From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr 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 5FA50BB83 for ; Fri, 1 Sep 2006 21:00:49 +0200 (CEST) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k81J0laa031375 for ; Fri, 1 Sep 2006 21:00:48 +0200 Received: from rosella (ppp14-47.lns2.syd7.internode.on.net [59.167.14.47]) by smtp1.adl2.internode.on.net (8.13.6/8.13.5) with ESMTP id k81J0SXa053212; Sat, 2 Sep 2006 04:30:29 +0930 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] Re: Polymorphic variants question From: skaller To: Chris King Cc: David Allsopp , OCaml List In-Reply-To: <875c7e070609011133udd506c7v223d8ece952b95ae@mail.gmail.com> References: <012901c6cdec$64edf490$6a7ba8c0@treble> <875c7e070609011133udd506c7v223d8ece952b95ae@mail.gmail.com> Content-Type: text/plain Date: Sat, 02 Sep 2006 05:00:28 +1000 Message-Id: <1157137228.22787.13.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.6.1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 44F8835F.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; variants:01 bool:01 compiler:01 val:01 bool:01 compiler:01 2006:98 sourceforge:01 wrote:01 wrote:01 polymorphic:01 typing:01 caml-list:01 expression:01 coercion:01 On Fri, 2006-09-01 at 14:33 -0400, Chris King wrote: > On 9/1/06, David Allsopp wrote: > > Now, if I try to constrain it to what I'm after with > > > > let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ... > > > > then I get a type error unless I change > > (false, x) > > to > > (false, id x) > > with > > let id = function `A -> `A | `C -> `C > > > > Is there a better way of writing this? > > Yes, you can use the coercion operator to tell the compiler to expand the type of x to include `B: > > # let f (x: [`A | `C]) = if x = `A then (true, `B) else (false, (x :> [`A | `B | `C])) > val f : [ `A | `C ] -> bool * [ `A | `B | `C ] = > > Perhaps someone else can clarify how this accomplishes the same thing as > your id function, as my understanding of type theory is somewhat rudimentary. The problem is `C not `B. Looking at this expression: if x = `A then (true, `B) else (false, x) we know the result is a bool followed by: 1. `B in the true case 2. x in the false case But we know x might be `A from the comparison x = `A so now we know the result is bool followed by `A, `B, or something else, we know not what, which x might be. Note that the type of x must include the case `A, since if this were not so the comparison: x = `A could not be between the same types .. even though x is only returned when it is *not* `A -- that's a flow of control issue not a typing issue. By using: let id = function `A -> `A | `C -> `C the compiler knows (id x) can include `A and it can include `C, the case (true, `B) being returned says the return type can also be `B. So the return type can be bool followed by `A, `B, or `C. Hope that makes sense :) -- John Skaller Felix, successor to C++: http://felix.sf.net