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 3C1C1BBC4 for ; Fri, 20 Jan 2006 19:59:23 +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 k0KIxMC5025128 for ; Fri, 20 Jan 2006 19:59:22 +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 TAA02162 for ; Fri, 20 Jan 2006 19:59:22 +0100 (MET) Received: from singularity.stwing.upenn.edu (YAVIN.STWING.upenn.edu [165.123.132.64]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0KIxK8Q025123 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 20 Jan 2006 19:59:21 +0100 Received: from localhost (localhost [127.0.0.1]) by singularity.stwing.upenn.edu (Postfix) with ESMTP id 64ED1BD4 for ; Fri, 20 Jan 2006 13:59:20 -0500 (EST) Received: from singularity.stwing.upenn.edu ([127.0.0.1]) by localhost (yavin.stwing.upenn.edu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 23233-06 for ; Fri, 20 Jan 2006 13:59:20 -0500 (EST) Received: from coruscant.stwing.upenn.edu (coruscant.stwing.upenn.edu [165.123.132.62]) by singularity.stwing.upenn.edu (Postfix) with ESMTP id 1CF9BA56 for ; Fri, 20 Jan 2006 13:59:20 -0500 (EST) Received: by coruscant.stwing.upenn.edu (Postfix, from userid 5302) id B1872E51E; Fri, 20 Jan 2006 13:59:19 -0500 (EST) Date: Fri, 20 Jan 2006 13:59:15 -0500 From: William Lovas To: caml-list@inria.fr Subject: Re: [Caml-list] Coinductive semantics Message-ID: <20060120185911.GA22920@coruscant.stwing.upenn.edu> Mail-Followup-To: caml-list@inria.fr References: <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> <43D0B413.1060806@andrej.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <43D0B413.1060806@andrej.com> User-Agent: Mutt/1.5.6i X-Virus-Scanned: amavisd-new at stwing.upenn.edu X-Miltered: at concorde with ID 43D1330A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43D13308.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; lovas:01 wlovas:01 stwing:01 upenn:01 caml-list:01 coinductive:01 semantics:01 andrej:01 lovas:01 o'caml:01 lacks:01 unions:01 algebra:01 axioms:01 negation: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 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 well-known that control constructs like callcc correspond via Curry-Howard 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 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. 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