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 E9B65BC2F for ; Fri, 26 Nov 2004 06:25:46 +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 iAQ5PkVJ016844 for ; Fri, 26 Nov 2004 06:25:46 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id GAA16656 for ; Fri, 26 Nov 2004 06:25:44 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iAQ5Pgn1016837 for ; Fri, 26 Nov 2004 06:25:43 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id iAQ5PbWG000022; Fri, 26 Nov 2004 14:25:38 +0900 (JST) Date: Fri, 26 Nov 2004 14:25:25 +0900 (JST) Message-Id: <20041126.142525.93385094.garrigue@math.nagoya-u.ac.jp> To: skaller@users.sourceforge.net Cc: warplayer@free.fr, caml-list@inria.fr Subject: Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement? From: Jacques Garrigue In-Reply-To: <1101438486.9291.138.camel@pelican.wigram> References: <1101427906.9291.107.camel@pelican.wigram> <20041126.094412.30442729.garrigue@math.nagoya-u.ac.jp> <1101438486.9291.138.camel@pelican.wigram> X-Mailer: Mew version 4.0.64 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41A6BE5A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41A6BE56.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 unification:01 unification:01 pointers:01 pointer:01 existential:01 intersection:01 ocaml:01 bool:01 conjunctive:01 bool:01 failwith: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: From: skaller > > But by definition 'a unifies with everything, including your void > > type, or you get a noncommutative notion of unification... > > Can you give an example? I presume you mean that > the invariant U(t1,t2) == U(t2,t1) would break? Not exactly, I rather meant that unification steps would not commute. This happens sometimes when you allow unification between specialized forms, but not with type variables. However, I do not understand completely what you mean by void type, and how they would relate to type variables, so it is not clear whether this is the problem. For instance, you say that (void * t) should be void, which suggests that void is really the type with 0 elements (i.e. not unit.) However, from a logical point of view (i.e. intuitionistic logic), no function can be allowed to return such a type. It may accept it as input, but this just means it is unusable. Note that void in C is definitely not zero. You cannot have variables of type void, but you can have non-null pointers to void. If void were really zero, then a void pointer would necessarily be NULL. It looks more like an existential type, (\exists a.a), which is actually equivalent to unit, with special rules to deal with the fact its physical representation is unknown. Concerning intersection types in ocaml, int&bool is not a type by itself. It may only appear as a variant argument. In that case this just means that this variant case cannot be used. In the past, [ ] was a valid variant type, and would have been zero, but I removed it as it does not make sense, and may delay some type errors. Types with only one variant may not be conjunctive either. So the closest you can get to zero now is a polymorphic type like [< `A of int&bool | `B of int&bool]. Even with [ ] there was no problem of commutation, because unification with 'a was allowed, i.e. ([ ] * int) and [ ] were different types; which was why it was clumsy to have zero in the language: there is nothing as stupid as moving provably non-existing data around, as it means that the code will never be used anyway. Jacques Garrigue P.S. I believe the problem with failwith is solvable, albeit rather complicated. The idea is that you want to be warned when you apply a function of type (\forall 'a. 'a) to something, because no such function may exist, so that this application will never actually take place. This could be done attempting to generalize the type of the function, once we now it is a type variable. I'll have a try.