[Haskell-cafe] Recommended reading on non-algebraic types.

[Ignat Insarov]

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-graphs.pdf