From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.1 required=5.0 tests=AWL,DNS_FROM_SECURITYSAGE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id D688ABB84 for ; Fri, 31 Oct 2008 01:09:02 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAPPpCUmCNhAB/2dsb2JhbADLSoNR X-IronPort-AV: E=Sophos;i="4.33,519,1220220000"; d="scan'208";a="30954874" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail4-smtp-sop.national.inria.fr with ESMTP; 31 Oct 2008 01:09:01 +0100 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m9V08mfe016408; Fri, 31 Oct 2008 09:08:49 +0900 (JST) Date: Fri, 31 Oct 2008 09:08:42 +0900 (JST) Message-Id: <20081031.090842.254669920.garrigue@math.nagoya-u.ac.jp> To: dra-news@metastack.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Private types From: Jacques Garrigue In-Reply-To: <5687D906367C49F981398A97A5966E09@countertenor> References: <340C8DB35D244173AE527238DB359A19@countertenor> <04092D60-3BB6-49A6-8A04-0BFE3A2081BD@erratique.ch> <5687D906367C49F981398A97A5966E09@countertenor> X-Mailer: Mew version 4.2 on Emacs 22.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; ocaml:01 ocaml:01 integers:01 abbreviation:01 coercions:01 casts:01 upcast:01 supertype:01 inference:01 inference:01 subtyping:01 coercions:01 checker:01 unify:01 unification:01 From: "David Allsopp" > Thanks for this - although it's a link to an OCaml 3.10 manual so not > applicable here it did point me to the correct chapter in the OCaml 3.11 > manual (I'd been looking in Part I of the manual and given up). What I > should have written is > > string_of_int (x :> int) > > Though that does make me wonder why the coercion is mandatory. What happens > if I *want* to allow the use of M.t values as though they were ints and only > want to guarantee that they come from a specific sub-set of the integers > (I'm thinking of database row IDs which is what I want to use them for)? > Assuming that the type abbreviation doesn't contain type-variables, would > there be anything theoretically preventing the inclusion of two keywords: > > type t = private int (* can be used as though it were an int *) > type t = very_private int (* requires a coercion to be used an int *) Explicit coercions in ocaml are completely unrelated to casts in C or Java, in that they only allow upcast (cast to a supertype). They are also completely erasable: they do not produce any code after type checking. So they are not there for any soundness reason, but just for type inference purposes. There would be no point at all in having two constructs: if the 1st one were possible, we wouldn't need the second. As for type inference, (x :> int) is already an abbreviated form of (x : t :> int), that only works if x is "known" to be of type t. Since ocaml type inference does not include subtyping, there is no way to do without coercions. To explain this, you should just see how the type checker handles string_of_int x It fetches the type of the string_of_int, int -> string, fetches the type of x, which is t, and tries to unify int and t. Since there is no direction in unification, this can only fail, as int and t are not equivalent, just related through subtyping. Your intuition is correct that it would theoretically be possible to try subtyping in place of unification in some cases. The trouble is that thoses cases are not easy to specify (so that it would be hard for the programmer to known when he can remove a coercion), and that subtyping is potentially very costly (structural subtyping is much harder to check than the nominal subtyping you have in Java.) So the current approach is to completely separate subtyping and type inference, and require coercions everywhere subtyping is needed. You can also compare that to the situation between int and float. For most uses, int can be viewed as a subtype of float. However ocaml separates the two, and requires coercion functions whenever you want to use an int as a float. Cheers, Jacques Garrigue