From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 15E59BB9C for ; Fri, 20 Jan 2006 10:56:48 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0K9ulP9008922 for ; Fri, 20 Jan 2006 10:56:47 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA23698 for ; Fri, 20 Jan 2006 10:56:46 +0100 (MET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0K9ujOX008911 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Fri, 20 Jan 2006 10:56:46 +0100 Received: from katapult.fmf.uni-lj.si ([193.2.67.50] helo=[10.10.4.74]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1Ezt0Y-0000bj-3L; Fri, 20 Jan 2006 10:56:45 +0100 Message-ID: <43D0B413.1060806@andrej.com> Date: Fri, 20 Jan 2006 10:57:39 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Debian Thunderbird 1.0.7 (X11/20051017) X-Accept-Language: en-us, en MIME-Version: 1.0 To: William Lovas Cc: caml-list@inria.fr References: <1136981974.8962.100.camel@rosella> <43C51C33.2000206@andrej.com> <1137031853.3681.138.camel@rosella> <43C661AF.2080404@andrej.com> <1137102848.3681.268.camel@rosella> <1137163342.3681.533.camel@rosella> <1137594157.8943.106.camel@rosella> <20060120004948.GA2490@coruscant.stwing.upenn.edu> In-Reply-To: <20060120004948.GA2490@coruscant.stwing.upenn.edu> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 193.2.67.50 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Coinductive semantics X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on haka.fmf.uni-lj.si) X-Miltered: at concorde with ID 43D0B3DF.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43D0B3DD.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 coinductive:01 semantics:01 lovas:01 o'caml:01 lacks:01 unions:01 algebra:01 intersection:01 unions:01 algebra:01 intersection:01 o'caml's:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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 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. Andrej