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 910F2BC88 for ; Sun, 6 Feb 2005 01:48:37 +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 j160mavt010491 for ; Sun, 6 Feb 2005 01:48:37 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA02439 for ; Sun, 6 Feb 2005 01:48:36 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j160mYEm010482 for ; Sun, 6 Feb 2005 01:48:35 +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 j160mNc3018953; Sun, 6 Feb 2005 09:48:23 +0900 (JST) Date: Sun, 06 Feb 2005 09:48:49 +0900 (JST) Message-Id: <20050206.094849.93018777.garrigue@math.nagoya-u.ac.jp> To: markus.mottl@gmail.com Cc: yminsky@cs.cornell.edu, caml-list@inria.fr Subject: Re: [Caml-list] Phantom types and read-only variables From: Jacques Garrigue In-Reply-To: <20050205192113.GA26897@mobile> References: <891bd33905020508504e272acf@mail.gmail.com> <20050205192113.GA26897@mobile> X-Mailer: Mew version 4.1 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 42056964.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 42056962.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 read-only:01 markus:01 mottl:01 markus:01 mottl:01 compiler:01 mutable:01 mutable:01 inference:01 unify:01 val:01 compiler:01 trivial:01 unification: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: Markus Mottl > Hm, it seems to me that the compiler could do a better job here. > > Instead of writing: > > type 'a t = { mutable value: int } > > write: > > type v = { mutable value: int } > type 'a t = v > > This should make the code compile. Indeed, by doing that you make t extensible to a type that drops the type parameter, meaning that type inference will never try to unify the parameter. A more direct way would be to define type 'a t = int ref Alternatively, you could just slightly change the definition of freeze, to allow dropping the parameter # type 'a t = { mutable value: int } ;; # let freeze ({value=_} as v) = v ;; val freeze : 'a t -> 'b t = > I think the compiler should be able to infer automatically that 'a isn't > used on the right hand side of the record definition (i.e. that it is > just a phantom type) without using the hint of a separate monomorphic > record definition. I guess this feature should be trivial to add. > Maybe in the next release? :-) Actually, this is a bit problematic. Types defined as abbreviations are automatically expanded during unification, so that unused parameters disappear. But datatypes cannot be expanded, so their parameters are going to be unified. Avoiding it would mean checking whether the parameters appear in the real definition during unification. This is possible, but would change the semantics of unification, something you want to be careful about. Actually ocaml 3.09 will go in the somehow opposite direction: allowing private types to behave as phantom types. Currently private types have their variance automatically inferred from their definition, meaning you can use the above subtyping trick even after the type is made private, but considering the fact they are semi-abstract, it seems more natural to require their variance to be explicitly given, allowing one to disallow such subtyping. Jacques Garrigue