Hello Café. This is a request for reading. There is a huge literature on mathematics of program construction, but those are algebraic types therein considered; abstract types are hardly mentioned. At the same time, reality presents us with a range of compact mathematical constructions that are, however, not readily expressible via tagged unions, tuples and fixed points. A few examples: * The most usual `"containers" Data.Set (Set) ` is an abstract type that is not even lawful enough to be a functor. * It has been discovered that graphs can be represented by algebraic types _(see `alga` [1][1])_, but edge labels are, to my knowledge, not available. The types for graphs that have edge labels are all abstract. Coincidentally or not, the usual representations for the examples above are trees, refined with the use of smart constructors — so they are subtypes of algebraic types. There are less computationally accessible subtypes, say the type of prime numbers as a refinement of ℕ. So, my home baked theory is that abstract types represent subtyping in Haskell, so that every abstract type is a subtype of an algebraic type, matching a defining condition and equipped with a collection of constructors — functions whose range respects that condition. This means, for example, that: * Any projection of an algebraic type can be restricted to an abstract subtype for free. * There is a canonical partial one to one function from an algebraic type to its abstract subtype. Of course, we do not get anything like that in Haskell. Rather, we have _«abstract»_ abstract types, divorced from the underlying algebraic representation. As a consequence, we have only a handful abstract types in use, as each must be carefully crafted, verified and bundled with the totality of the interface — in a word, a bubble. By this point in my line of reasoning, I have to question if this fashion is justifiable. By now, the kind reader may concede that the matter is not without attraction. However, I am not aware of any prior art. For example, I wonder if there is a methodology for deciding if a given mathematical construction can be represented as an algebraic data type, and so far I have not seen this question being put forward. Please let me know if you have in mind some writing even faintly related to the line of inquiry presented above. [1]: https://github.com/snowleopard/alga-paper/releases/download/final/algebraic-...