This reminds me of my quest to find the proper method to model what I've termed 'large types' in an ideal language. As is well known, algebraic data types as c

This reminds me of my quest to find the proper method to model what I've termed 'large types' in an ideal language. As is well known, algebraic data types as commonly found, consist of sums of products, yet a great deal of useful types are larger than that; some hopefully illustrative examples include: 1) the type of subsets of another type would be 2^X (hopefully demonstrating what I mean by 'large'ness); 2) in practical languages like TypeScript, the 'Partial' of a product type A x B x C would be (1 + A) x (1 + B) x (1 + C); 3) data structures in general, as a term amenable to some certain set of operations, when needing to be represented for performance reasons e.g. a) union-find structures (quotients?); b) a list of words and their inverted indexes for searching; c) a sorted list Reading more about type modelling, and learning of the disagreements in how even basic things like quotients ought to be represented as types, I've since resigned to an understanding of this as an unsolved problem, and relegated the modelling the kitchen sinks of types with the kitchen sink of types - i.e. the function type (curbed with suitable type constraints upon the signature - from an index type to a suitable base type) - after all, its power and province being the irreducible kernel of type polymorphism, shadow over Church's types, original sin against type decidability.