Re: [Caml-list] Coinductive semantics

[Andrej Bauer <Andrej.Bauer@andrej.com>]

William Lovas wrote:
> A thought: products and sums are duals, classically, but not
> intuitionistically.

This is false. Products and sums are dual concepts, both classically and
intuitionistically.

> Since O'Caml lacks classical control constructs like
> callcc, there's no redundancy having both products and sums: neither is
> representable solely using the other.

The above statement is rather vague and I am tempted to ignore it. If I
try to interpet it the best I can, it looks as if William is confusing
sums and products with unions and intersections (and is thus thinking
that complements might help in representing sums as products, using laws
of Boolean algebra).

Intersection of sets is a special case of products. Unions is a special
case of coproducts. In any Boolean algebra (hence also in the Boolean
algebra of subsets), unions and intersections may indeed be expressed in
terms of each other, using complements:

 A union B = complement (complement A intersection complement B)

where A, B are elements of a Boolean algebra. But in a general category
there is not such relationship between products and coproducts.

(By the way, unions and intersections are dual concepts even if there is
no complementation available, such as in intuitionistic set theory.)

> Also, O'Caml's datatypes are much more than just sums: they also include
> recursive types, polymorphism, pattern matching, and a degree of
> abstraction.

So? What is the point here?

In a programming language equipped with products and natural numbers,
and irrespective of what else is there, sums of (inhabited) types may be
encoded by products, as every programmer knows (at some level). For
example, to encode the following sum, which expresses the fact that
programmers are interesting characters and mathematicians may experience
instabilities,

  type person = Programmer of char | Mathematician of float

we assign constants

  let programmer = 0
  let mathematician = 1

pick two dummy values

  let dummy_c = '\0'
  let dummy_f = 0.0

and encode values of type person as values of the product type

  type person' = int * char * float

A value Programer(c) is represented by the triple (programmer, c,
dummy_f) and a Mathematician(x) is represented by (mathematician,
dummy_c, f). In a less strictly typed language (e.g. assembler), we may
avoid the redundancy and encode the sum with the product type

  type person'' = int * t

where t is a type large enough to hold both char and float. This is
precisely how people who use "lesser" languages work with sums, and
precisely how sums are represented in compiled ocaml code (modulo
optimizations). Of course, it does not provide a water-tight duality
between products and sums at the level of datatypes, but a certain
realizability construction gets you to a category (built on top of
datatypes) in which the above trick is precisely how sums are
constructed--all that is added as an aftertaught is the definition of
the subobject of person' consisting of those triples whcich represent
valid values of the corresponding sum type.

Andrej