From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id DFE5ABBC4 for ; Sat, 21 Jan 2006 20:05:07 +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 k0LJ571L004458 for ; Sat, 21 Jan 2006 20:05:07 +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 UAA18837 for ; Sat, 21 Jan 2006 20:05:05 +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 k0LJ539r004442 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Sat, 21 Jan 2006 20:05:04 +0100 Received: from bsn-77-186-71.dsl.siol.net ([193.77.186.71] helo=[192.168.1.101]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1F0O2j-0005yS-RC; Sat, 21 Jan 2006 20:05:03 +0100 Message-ID: <43D2861A.7070906@andrej.com> Date: Sat, 21 Jan 2006 20:06:02 +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: caml-list@inria.fr Cc: William Lovas 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> <20060120185911.GA22920@coruscant.stwing.upenn.edu> In-Reply-To: <20060120185911.GA22920@coruscant.stwing.upenn.edu> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 193.77.186.71 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 43D285E3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43D285E0.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 categorical:01 categorical:01 encodings:01 bool:01 char:01 def:01 def:01 booleans:01 bool: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: >> 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 type-theory 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 well-versed in type theory, so you'll have to translate that into "real" type-theoretic 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