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:  20060120 (18:59) 
From:  William Lovas <wlovas@s...> 
Subject:  Re: [Camllist] Coinductive semantics 
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 wellknown that control constructs like callcc correspond via CurryHoward 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 watertight 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 > constructedall 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