Re: [Caml-list] Coinductive semantics

[William Lovas <wlovas@stwing.upenn.edu>]

On Fri, Jan 20, 2006 at 10:57:39AM +0100, Andrej Bauer wrote:
> 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.

Perhaps you can explain this in more detail; my training is in type theory,
not category theory, and i had deMorgan duals in mind.

> > 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).

It is well-known that control constructs like callcc correspond via
Curry-Howard to classical axioms like Peirce's law.  I was referring to
the fact that in the presence of such control operators, one can devise a
sound and complete encoding of products in terms of sums or sums in terms
of products.  For example, section 7 of Tom Murphy's 2005 CSL paper
"Distributed Control Flow with Classical Modal Logic" showed how to define
sums in terms of products using deMorgan duality and letcc.

Maybe what i mean when i say "product" and "sum" is something different
from what you mean?  I *have* been thinking about deMorgan duality using
negation as you mentioned, but it's unrelated to union and intersection
types.

> > 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?

The point is that even if sums were encodable using products, the inclusion
of datatypes in O'Caml would not be redundant as skaller suggests, since
they bring with them access to several other important features whose
behavior would not otherwise be expressible.

>   type person = Programmer of char | Mathematician of float
> [...]
>   type person' = int * char * float
> [...]
>   type person'' = int * t

These encodings do not have the same force as the original type; they are
complete, but unsound -- every value of person has a corresponding value in
person', but not every value of person' has a corresponding person value
(like (3, 'c', 0.0), for example).  To do this sort of encoding correctly,
wouldn't you need dependent types in the language?  So you could write
something like:

    type person''' = Sigma x:bool. if x then char else float

with

    Programmer(c) =def= (true, c)
    Mathematician(x) =def= (false, x)

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

Perhaps this afterthought subobject is similar to what i'm referring to
above, but i don't know enough category theory to be certain.

cheers,
William