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 9E11BBB91 for ; Thu, 27 Jan 2005 01:19:19 +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 j0R0JJ7E023852 for ; Thu, 27 Jan 2005 01:19:19 +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 BAA30918 for ; Thu, 27 Jan 2005 01:19:18 +0100 (MET) Received: from us19.unix.fas.harvard.edu (us19.unix.fas.harvard.edu [140.247.35.199]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0R0JINJ011044 for ; Thu, 27 Jan 2005 01:19:18 +0100 Received: from [140.247.161.153] (roam161-153.student.harvard.edu [140.247.161.153]) by us19.unix.fas.harvard.edu (8.12.11/8.12.11) with ESMTP id j0R0JHCK029918 for ; Wed, 26 Jan 2005 19:19:17 -0500 Mime-Version: 1.0 (Apple Message framework v619) Content-Transfer-Encoding: 7bit Message-Id: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> Content-Type: text/plain; charset=US-ASCII; format=flowed To: caml-list@inria.fr From: Mike Hamburg Subject: '_a Date: Wed, 26 Jan 2005 19:19:16 -0500 X-Mailer: Apple Mail (2.619) X-Miltered: at concorde with ID 41F83387.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41F83386.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; beginners:01 o'caml:01 arrays:01 val:01 val:01 o'caml:01 mutable:01 subtype:01 subtype:01 mutable:01 stack:01 memoize:01 hash:01 pointer:01 type-safe: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: 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). The cause of the problem is that programs may create a closure with a mutable variable of type 'a, which if we were to let 'a generalize could be replaced with a subtype 'b of 'a, and then used as another subtype 'c of 'a, which would be unsafe. As a fix, I propose the following: the type system should keep track of where a mutable or immutable reference to a polymorphic variable with type parameter 'a is created on the stack. Call these places [m'a] and [i'a]. For example, ref should have type 'a -> [m'a] 'a, and ref [] should have type [m'a] 'a (which is equivalent to the current '_a). I don't propose that the printing should show this complexity, just as it hides whatever heuristic O'Caml is using now, except in the case where there is a mutable reference at top level, in which case it should convert 'a to '_a. Of course, module interfaces shouldn't have to show when they keep references to things, so we probably can't do much about applying List.map to the identity without modifying List (for instance, what if List.map decided to memoize the function fed into it using a hash table?). Is this a reasonable idea? If so, can someone give me a pointer on how to go about implementing it (or proving that it is type-safe with appropriate unification rules?)? Mike