From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 18E4ABB91 for ; Thu, 27 Jan 2005 01:51:57 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j0R0pudH027105 for ; Thu, 27 Jan 2005 01:51:56 +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 BAA31233 for ; Thu, 27 Jan 2005 01:51:55 +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 j0R0prCc013943 for ; Thu, 27 Jan 2005 01:51:55 +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 j0R0pgZ5014144; Thu, 27 Jan 2005 09:51:42 +0900 (JST) Date: Thu, 27 Jan 2005 09:51:19 +0900 (JST) Message-Id: <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> To: hamburg@fas.harvard.edu Cc: caml-list@inria.fr Subject: Re: [Caml-list] '_a From: Jacques Garrigue In-Reply-To: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> References: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> X-Mailer: Mew version 4.1.53 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 concorde with ID 41F83B2C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41F83B29.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 caml-list:01 beginners:01 o'caml:01 arrays:01 val:01 val:01 o'caml:01 runtime:01 wwwfun:01 ocaml:01 syntactical:01 polymorphic:01 functions:01 jacques: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: Mike Hamburg Subject: [Caml-list] '_a Date: Wed, 26 Jan 2005 19:19:16 -0500 > The appearance of '_a in places where it shouldn't appear causes some > annoyance, and a good deal of confusion among beginners to O'Caml. In > particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a > list, whereas it instead has type '_a list -> '_a list. > > Some types are treated specially for creation of '_a, such as refs and > arrays. For instance, if you have the following two declarations: > > # let a = let f x () = [x] in f [];; > val a : unit -> 'a list list = > # let b = let f x () = [|x|] in f [];; > val b : unit -> '_a list array = > > Although I haven't read the code for O'Caml, I deduce from this that > there is deep magic in place to determine when to turn 'a into '_a, and > in many cases, the heuristic is wrong (in the conservative direction: > in this case, 'a should not be turned into '_a until b is applied). There is no deep magic, no heuristics. There is just a type system which guarantees type soundness (i.e. "well typed programs cannot produce runtime type errors"). If you want the type system and all the historical details, read my paper "Relaxing the value restriction" at http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ In a nutshell, ocaml uses an improvement of the value restriction. With the value restriction, only definitions which are syntactical values (i.e. that do not call functions, etc when defined) are allowed to contain polymorphic type variables. This is improved by allowing covariant type variables to be generalized in all cases. Your first example is ok, because list is a covariant type, but your second fails, because array is not (you may assign to an array, and you would have to look at the code to see that each call to b creates a different array) Of course, one could think of many clever tricks by looking at what the code actually does. The above paper describes some of the "crazy" things Xavier Leroy and others tried in the past, which actually subsume your ideas, before they all decided this was too complicated. The main reason is that, if something is going to break at module boundaries, then it is not really useful. Good reading, Jacques Garrigue