From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 0B0F7BC2F for ; Fri, 26 Nov 2004 04:58:32 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iAQ3wUfS009658 for ; Fri, 26 Nov 2004 04:58:31 +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 EAA11628 for ; Fri, 26 Nov 2004 04:58:30 +0100 (MET) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iAQ3wSl2011614 for ; Fri, 26 Nov 2004 04:58:29 +0100 Received: from [192.168.1.200] (ppp217-171.lns1.syd3.internode.on.net [203.122.217.171]) by smtp1.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id iAQ3wJ4Y038662; Fri, 26 Nov 2004 14:28:22 +1030 (CST) Subject: Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement? From: skaller Reply-To: skaller@users.sourceforge.net To: Jacques Garrigue Cc: warplayer@free.fr, caml-list In-Reply-To: <20041126.094412.30442729.garrigue@math.nagoya-u.ac.jp> References: <20041125204628.GA24215@annexia.org> <005701c4d333$c3bc31e0$19b0e152@warp> <1101427906.9291.107.camel@pelican.wigram> <20041126.094412.30442729.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain Message-Id: <1101441498.9291.182.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 26 Nov 2004 14:58:19 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41A6A9E6.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41A6A9E4.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 ocamlopt:01 failwith:01 sourceforge:01 wrote:01 unification:01 polymorphism:01 afaik:01 polymorphism:01 pointer:01 heap:01 'a-:01 improper:01 categorical:01 ocaml:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Fri, 2004-11-26 at 11:44, Jacques Garrigue wrote: > But by definition 'a unifies with everything, including your void > type, or you get a noncommutative notion of unification... BTW: I still don't have a clear understanding of exactly how problems arise with void with intensional polymorphism. The typing with a distributive category is clearly sound. AFAIK this extends to a cartesion closed category. One might think that extra checks would be needed which would have to be done at run time with intensional polymorphism. For example: let snd (x,y) = y Here, 'a * 'b is isomorphic to void if 'a or 'b is void. The definition of snd then doesn't make sense. The actual problem, however, isn't void, but the incorrect assumption that a pair can represent a polymorphic tuple: it isn't the typing that is unsound, but the choice of canonical representation of product. The problem would go away if the pointer to the heap block was NULL for void, but this would require extra NULL checks at run time. However, this particular example cannot ever lead to a problem, since you can't actually create a variable of void type (there's no value to put in it) so no possible instantiation of 'snd' can fail. [There is a clearly related issue with unit: the types 'a and 1 * 'a are isomorphic, but the definition of numbered projections prevents the useless unit being optimised away -- the language guarrantees not to apply this isormorphism simply because it would break the run time representation.] However I don't know if this argument can be extended in the presence of function types. It would seem that without a primitive function returning void, there's no way to encode one that returns void either. However if you have a primitive f:'a-> void you can obviously create new functions returning void, for example: let g f x = f x let h x = g f x However I still don't see how you can ever call such a function in a way that actually tries to pass a value of type void. That value has to come from somewhere and there is no way to make one: a call f x is manifestly of type void, and so, for example, (f x, 99) is manifestly of type void. My thinking is that if you can't catch an improper use of void at compile time, then there can't be one at run time either (in other words its quite sound). I would like to see an example where this is not the case. I'm suspicious, because void is the categorical initial, and a fundamental part of many of the models for computing I've seen based on category theory -- and my understanding is that the CT approach is just an alternative to lambda calculus (i.e. they're equivalent). So it looks to me that not providing an algebraic void is a way to simplify the representation -- not a matter of unsoundness. BTW: Ocaml unification must already handle void: it supports intersection types internally, and int & float is void. How is it that this also doesn't lead to non-commutative unification? -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net