Cobig Comma Pratt

Date: Tue, 21 Mar 89 13:32:11 -0100

I was fascinated by Vaughan Pratt's "Cobig, Coproduct and Comma".
Hagino's thesis on categorical datatypes uses comma categories
to give meaning to the concept of recursive sums and products.
The ideas presented also recall Freyd's structors.

I hope Vaughan Pratt did not think I was trying to say that values
of sums are finite and values of products are infinite; perhaps it is
my fault for being too imprecise. What I ought to have said is that
values of a recursive sum (initial algebra) A(T) are well-founded
over T (can be expressed as a term involving constructors and T-values)
whereas values of a recursive product (final coalgebra) B(T) are not
in general. Of course one can have isomorphisms e.g.

                (U+V)*W ~ (U*W)+(V*W)

in a category (or some other semantics). However, in a programming language
we have to deal with free expressions. We would expect quite different
representations for values of type (U+V)*W from representations of values
of type (U*W)+(V*W). The confusion arises because we are insufficiently
clear about the level of metalanguage.

We have "types" in a (hypothetical) programming language, that correspond
to certain tokens and patterns of usage of those tokens, e.g. list(int)
or whatever - the concrete syntax. Then we have "types" in an abstract
syntax e.g. mu x.(1+int*x) or !x.((!y.(y->y)->(y->y))->x->x)->x->x
or whatever, depending on the theory and on its presentation. Then we
have the interpretation of types, as objects, structors, ideals,
algebraic toposes, etc. I apologise if my musings have caused
confusion through lack of precision.

I am rather gratified to have had so much response to the kite I flew.
Perhaps I should summarise by saying that I think it would be
helpful to make a distinction between sum type declarations (algebraic
datatypes) and product type declarations (coalgebraic datatypes). The
latter have either not been recognised (in the recursive case) or
have been forced into bed with sum types. There are, of course, a lot of
ways of thinking about mathematical structures/constructions/types;
to a large extent it is a matter of fashion or taste. When it comes to
using these ideas in programming languages there are other constraints -
computability, efficiency etc. The general notions of sum type and product
type lead to natural ideas for implementation: a constructor for a sum simply
tags a value, the case statement corresponds to a branch table, with an entry
for each tag, a record corresponds to an array of pointers, a destructor
for a product type simply indirects through the relevant array pointer.
Recursive records are obtainable by knot-tying; recursive values for sum
types do not come in to the picture. I am envisaging systems where all
type-checking is done at compile time, so there is no computation
involved in having recursive type declarations, sum or product.

Gavin Wraith