From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id B59D7BC8E for ; Wed, 16 Feb 2005 00:15:40 +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 j1FNFerb025823 for ; Wed, 16 Feb 2005 00:15:40 +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 AAA12989 for ; Wed, 16 Feb 2005 00:15:40 +0100 (MET) Received: from nutty.inf.ed.ac.uk (nutty.inf.ed.ac.uk [129.215.216.3]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j1FNFdpj025817 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 16 Feb 2005 00:15:39 +0100 Received: from [129.215.96.135] (dhcp-96-135.dcs.ed.ac.uk [129.215.96.135]) by nutty.inf.ed.ac.uk (8.12.8/8.12.8) with ESMTP id j1FNFdpH007997 for ; Tue, 15 Feb 2005 23:15:39 GMT Mime-Version: 1.0 (Apple Message framework v619.2) In-Reply-To: <421275ED.1060607@laposte.net> References: <7bf1f3b95c18eeda0ed169eb7f73d6f0@urbanet.ch> <421275ED.1060607@laposte.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Message-Id: <141c991e0f84781450c6f0948e9f6cb0@epfl.ch> Content-Transfer-Encoding: quoted-printable From: Gilles Dubochet Subject: Re: [Caml-list] Polymorphic variant typing Date: Tue, 15 Feb 2005 23:15:38 +0000 To: Caml-list X-Mailer: Apple Mail (2.619.2) X-Miltered: at nez-perce with ID 4212829C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 4212829B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; epfl:01 caml-list:01 ocaml:01 val:01 inference:01 variants:01 o'caml's:01 variants:01 inference:01 o'caml's:01 o'caml:01 notation:01 cheers:01 ...:98 polymorphic:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: >> let incr g x =3D match x with >> | `Int i -> `Int (i+1) >> | x -> (g x);; >> Receives type: >> (([> `Int of int ] as 'a) -> ([> `Int of int ] as 'b)) -> 'a -> 'b > > Now, how about this : > > let incr x g =3D match x with > | `Int i -> `Int (i+1) > | x -> g x;; > > Doesn't it look like your code ? OCaml 3.08.2 types it as follows : > val incr : ([> `Int of int ] as 'a) -> ('a -> ([> `Int of int ] as=20 > 'b)) -> 'b =3D > > This is more like it ! I am afraid I can't agree with you: As far as I can tell, this type=20 with the 'x g' version is exactly equivalent to the type I obtained=20 with the 'g x' version. If you remember that "... as 'a" is the binding=20= of a type variable, it is quite intuitive why. > incr (`Int 1) (fun (`Int i) -> (`Int (i+1)));; > - : [> `Int of int ] =3D `Int 2 > incr (`Float 1.0) (fun x -> match x with (`Float f) -> (`Float (f +.=20= > 1.0)) | x -> x);; > - : [> `Float of float | `Int of int ] =3D `Float 2. Yes, but in your case the g function you pass as a parameter has a last=20= generic case. This means it has type "([> `Float of float ] as 'a) ->=20 'a" which is an "at least" instead of a "at most" variant type. With=20 that function it works also with my original 'g x' version. The goal is=20= to be able to make this run: incr (`Float 1.0) (fun x -> match x with (`Float f) -> (`Float (f +.=20 1.0)));; And your solution doesn't more than mine. Just to make things clear, I am not looking for a workaround to this=20 problem. I am rather looking for an explanation about why the mentioned=20= type is inferred for this expression. I am developing a type inference=20= system for a language with similar variants to O'Caml's polymorphic=20 variants. My inference algorithm calculates a different type than=20 O'Caml's for a equivalent expression. I try to understand why O'Caml=20 does it that way to decide how I should do it. To make it even more=20 clear, the type I obtain with my algorithm is (in row variable=20 notation): (['a] -> [#int:int | 'b]) -> [#int:int | 'a] -> [#int:int |=20= 'b] Voil=E0, but thanks for the answer anyway, Cheers, Gilles.=