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

[Olaf Klinke]

Dear Ignat, 

In the paper you linked to one should state more clearly that the two
graph operations overlay and connect use an implicit equivalence
relation between vertices of the two graphs involved. So these
operations can be thought of as a traditional algebraic operation
followed by a quotient. 

You might want to learn about domain semantics in general and domain
environments in particular. Big names are Dana Scott and Gordon
Plotkin, to name just two. Domain theory is the science of assigning
(via  a functor) an object of a category of partially ordered sets to
each type of a (typed) lambda calculus and to each term of the calculus
an arrow of that category. 
It turns out that algebraic domains are suitable for representing
programs on algebraic data types. And if the category is just right and
the lambda calculus is rich enough, then one can go the other way: Then
you can prove that for each arrow in the category of domains there is a
program that has that arrow as semantics. Algebraic domains match very
nicely the way we build up complex data types via tuples, sums,
function types and type recursion and how we build up functions via
pattern matching and recursion. And every finite algebraic domain is a
directed cycle-free graph. The little (free online) book by Thomas
Streicher [1] might be a good start on domain semantics. A
comprehensive mathematical theory of domains (not only algebraic ones)
can be found in [2] but that book is expensive and hard to obtain. 
Sadly, with vanilla type systems such as Haskell's you can specify only
algebraic domains. Anything beyond that is via "soft" definitions,
meaning it can not be expressed in the type system, as you already
observed. And domain theory provides mathematical proofs for this fact.

Representing types like the prime numbers is possible with dependently-
typed languages, but as far as I know these languages can also not go
beyond algebraic domains, anyone please correct me if I'm wrong. 

Of course people have thought about representing other structures that
are not algebraic domains. There are at least two ways I can think of:

(1) What you call a sub-type: A subset of an algebraic domain. If the
sub-type in question somehow sits "at the top" of the domain, then the
surrounding algebraic domain is called a domain environment of the type
in question. For example, the infinite binary tree is a domain
environment of the type of infinite binary sequences. The important
question to ask youself here is whether the sub-type is a computable
one or not [*]. So if A is an algebraic data type, can you write a
program that, given x :: A decides whether x is a member of the sub-
type? For example, the sub-type of total functions A -> B is not a
computable sub-type of the type of all functions A -> B for general A
and B.  

(2) Quotients of algebraic domains. That means each element of your
target type has several (maybe infinitely many) representations in an
algebraic domain. This is fairly common. The Double data type has two
representations for zero, because each Double value has a sign bit. If
you want a set functor, take any container like [] or Seq and disregard
multiplicities, so [x,y] and [x,y,y] represent the same set {x,y}. The
art is then to write functions f that respect these quotients. Meaning
if the values x and y both represent the same element in the quotient,
then f(x) and f(y) represent the same element again. See section 4.2 in
your linked paper on the problem of whether equivalence classes are
computable. 

A stronger notion is a retract, that is a quotient map q :: A -> D
together with a function e :: D -> A that embeds the type D back into
the algebraic domain A such that q.e = id and q and e are adjoints. It
is known that the retracts of algebraic domains are precisely the so-
called continuous domains, a wide class that encompasses for example a
real numbers object. 

Now you may also want to combine (1) and (2) and represent your data
type as a quotient of a sub-set of an algebraic domain. As I see it
your paper describes just that. 

It is still an open question whether certain continuous domains can be
represented via expanding systems of finite domains, as is the case
with algebraic domains [**]. My gut feeling is that such a description
involves a description of quotients, but on another level: Since any
quotient of a finite domain is algebraic, limits of such quotients will
not take you beyond algebraic domains. Instead, one must describe what
the quotient q :: A -> D does to the finite parts of A. 

Regards,
Olaf


[1] https://b-ok.org/book/768876/241ddb
[2] Continuous lattices and domains, ISBN 0-521-80338-1
[*] One can prove that while there are uncountably many subsets of
natural numbers, there are only countably many computable subsets in
the sense that there exists a program that decides membership. 
[**] Give me any Haskell type and I show you the system of retractions
of finite types whose limit is this type.