From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 735A5BC8E for ; Wed, 16 Feb 2005 01:37:56 +0100 (CET) Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j1G0bsav029789 for ; Wed, 16 Feb 2005 01:37:55 +0100 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id j1G0bmef016913; Wed, 16 Feb 2005 09:37:48 +0900 (JST) Date: Wed, 16 Feb 2005 09:36:35 +0900 (JST) Message-Id: <20050216.093635.226803934.garrigue@math.nagoya-u.ac.jp> To: dubochet@urbanet.ch Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic variant typing From: Jacques Garrigue In-Reply-To: <7bf1f3b95c18eeda0ed169eb7f73d6f0@urbanet.ch> References: <7bf1f3b95c18eeda0ed169eb7f73d6f0@urbanet.ch> X-Mailer: Mew version 4.0.69 on Emacs 21.3.50 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Miltered: at concorde with ID 421295E2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 o'caml:01 wand:01 notation:01 notation:01 o'caml:01 variants:01 ocaml:01 remy's:01 inference:01 polymorphism:01 wwwfun:01 avoiding:01 algebra:01 ocaml: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: From: Gilles Dubochet > The following O'Caml expression: > 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 > = > Why? I am quite astonished. I would have expected a type more like: > ([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ] > = > or in Wand or R=E9my-like row variable notation with which I am a lit= tle = > more comfortable (I am not exactly sure the preceding type is correct= = > in the 'at leat - at most' notation of O'Caml): > ([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ] The reason is simple enough: variants in ocaml are not based on Remy's rows, but on a type system with kinded variables, more in Ohori's style= .= This is described in detail in "Simple type inference for structural polymorphism", which you can find at http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ The main reason for this choice is avoiding making rows explicit, i.e. having a multi-sorted type algebra. Note also that ocaml object types, while originally based on Remy's system, are hiding their row-variables, and can be described in the same formalism. > Could anyone be kind enough to give me some clues about where to look= = > at to find an explanation or even better, explain me what is going on= ? = > I am particularly puzzled by the fact that the g function's *argument= * = > type is 'at least `Int of int'. This rejects the following code which= = > seems intuitively correct: > incr (function `Float f -> `Float (f+.1.));; Pragmatic reasons for this choice are given in Section 3 of "Typing deep pattern-matching in presence of polymorphic variants" which you can find at the same place. Cheers, Jacques Garrigue