Coinductive semantics
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060121 (19:05) 
From:  Andrej Bauer <Andrej.Bauer@a...> 
Subject:  Re: [Camllist] Coinductive semantics 
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 typetheory 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 wellversed in type theory, so you'll have to translate that into "real" typetheoretic 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