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:   (:) 
From:  Andrej Bauer <Andrej.Bauer@a...> 
Subject:  Re: [Camllist] Coinductive semantics 
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 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. Andrej