Recommended reading on non-algebraic types.

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: 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.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.