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 2ECDCBCAE for ; Fri, 1 Jul 2005 01:57:41 +0200 (CEST) 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 j5UNvdLn017988 for ; Fri, 1 Jul 2005 01:57:40 +0200 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id j5UNvXkc025976; Fri, 1 Jul 2005 08:57:34 +0900 (JST) Date: Fri, 01 Jul 2005 08:57:27 +0900 (JST) Message-Id: <20050701.085727.25912785.garrigue@math.nagoya-u.ac.jp> To: Julien.Verlaguet@pps.jussieu.fr Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] bizarre type From: Jacques Garrigue In-Reply-To: References: <000d01c57dab$21871e30$14b2a8c0@wiko> X-Mailer: Mew version 4.2 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 42C486F3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 compiler:01 bool:01 compiler:01 semantics:01 avoiding:01 implicitly:01 coerced:01 ocaml:01 subtyping:01 inference:01 non-trivial:01 disturbs:01 unification:01 ...:98 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: Julien Verlaguet > > > Well, since '_a t = int t the compiler can freely choose either for > > printing. Or bool t, for that matter. > > agreed. Nice to see that everybody agrees that the current behaviour is reasonable :-) And thanks to Andreas for explaining things so well. Yet, these useless parameters are a rather weak part of the compiler, so there may be some bugs left there. I.e. it is hard to guarantee that "a t" will alway be equivalent to "b t" for any use, while they should be so in the intended semantics. Bugs report are welcome. In general, I would suggest avoiding non-abstract phantom types, as they are useless... except when you're going to abstract them at the next module boundary. > In fact it prevents me from writting this : > > type 'a marshalled=string > > let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);; > > And then do all type of operations in a type safe way on strings. What you want seems to be the Graal: a type that is more than a string, but can be implicitly coerced to one. Of course the opposite direction would not be allowed. A standard way to do that is to make [marshalled] abstract, and provide a function [to_string] when you need to recover the string. In ocaml 3.09, you will have another possibility: using a private type for that, with the extra advantage of having pattern-matching (this doesn't work with private types in 3.08, as they are not handled as abstract.) But not yet the Graal, which requires to combine implicit subtyping with type inference in a non-trivial way... > The only tiny thing that disturbs me is that in my previous example : > > let g (x : 'a t) (y : 'a) > > the type of y depends on the 'a present in 'a t. > It is odd. But I have to admit it's correct. The point here is that ['a t] is not the type of [x] itself, but a type that can be unified with it. And useless parameters are discarded during unification. At a more theoretical level, ['a t] is only required to be equivalent to the type of [x], not identical. Jacques Garrigue