Re: [Caml-list] Coinductive semantics

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

William Lovas wrote:
>> 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.

Concepts X and Y are dual if X's in a category C are the same thing as
Y's in the opposite category C^op. There is no classical logic involved
when you ask "are products and coproducts dual"--it is apparent that
they are if you look at their definitions in terms of categorical limits
and colimits.

The type-theory training explains (to me) what you had in mind. In type
theory, types and propositions are the same thing, so it makes sense to
talk about deMorgan rules that involve types. Presumably one could do
that in categories as well: consider a category that is equipped with an
involution * such that

  X + Y = (X* x Y*)*

This would be an analogue of deMorgan rules and it would give you
coproducts out of products. But it's a rather special thing and I don't
know how to even express the above equation without first postulating
that coproducts exist. There are several other ways of getting
coproducts out of other things that exist in a category.

> Maybe what i mean when i say "product" and "sum" is something different
> from what you mean?

I mean categorical products and coproducts.

> 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)
> 
> Perhaps this afterthought subobject is similar to what i'm referring to
> above, but i don't know enough category theory to be certain.

Not quite, in terms of dependent type theory the aftertaught would be
something like defining a coproduct u+t as a setoid with underlying type
int * u * t and "equality" relation ~

    (a,x,y) ~ (b,x',y') <==>  (a=b=0 and x=x') or (a=b=1 and y=y')

I am not too well-versed in type theory, so you'll have to translate
that into "real" type-theoretic lingo.

As I said, there are many ways to get coproducts. Above you mention one
which uses dependent sums and the type of booleans, which is the
simplest instance of a sum, namely bool = unit + unit.

Another well known construction of coproducts comes from the polymorphic
lambda calculus, where the coproduct u + t is represented by the type

  (u -> 'a) -> (t -> 'a) -> 'a

To see this, use the exponential laws:

  (u -> 'a) -> (t -> 'a) -> 'a =
  (u -> 'a) * (t -> 'a) -> 'a =
  ((u + t) -> 'a) -> 'a .

Nevertheless, none of the above is an argument in favor of eliminating
coproducts from a programming language. In general, the argument "we may
eliminate concept X because it can be reconstructed using other concepts
already present" must be used with caution, lest one ends up programming
directly in assembler.

We are way off topic for this mailing list here, aren't we?

Andrej