From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2SC0j1d030016 for ; Mon, 28 Mar 2011 14:00:46 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuIAADx3kE1V2gB4mWdsb2JhbAClYAEBAQEBCAsLBxQliGu6Ag2FXASQZQ X-IronPort-AV: E=Sophos;i="4.63,255,1299452400"; d="scan'208";a="91347017" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail4-smtp-sop.national.inria.fr with SMTP; 28 Mar 2011 14:00:44 +0200 X-Alinto-smtpauth-localdomain: Yes Received: from seldon (unknown [85.218.93.111]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal1.citycable.ch (Postfix) with ESMTPA id 5F37012CCD2; Mon, 28 Mar 2011 14:00:42 +0200 (CEST) Received: from yziquel by seldon with local (Exim 4.72) (envelope-from ) id 1Q4B5h-0001Ze-Gd; Mon, 28 Mar 2011 13:58:37 +0200 Date: Mon, 28 Mar 2011 13:58:36 +0200 From: Guillaume Yziquel To: David Allsopp Cc: Alain Frisch , caml-list Message-ID: <20110328115831.GW20598@localhost> References: <89643D7F-B0F9-4452-BBAF-0445D9D3CA4E@gmail.com> <639CCD2C-402F-4754-B942-B460FD908A95@gmail.com> <63968844-AD95-4359-80F0-E9E071CF6518@mpi-sws.org> <20110325164240.GT10028@localhost> <46B666E2-4575-4E79-ACF1-FE0789C0C76B@mpi-sws.org> <20110325190129.GU10028@localhost> <4D903E90.4080907@frisch.fr> <20110328103325.GH20598@localhost> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.20 (2009-06-14) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p2SC0j1d030016 Subject: Re: [Caml-list] Re: module typing issue Le Monday 28 Mar 2011 à 11:29:51 (+0000), David Allsopp a écrit : > Guillaume Yziquel wrote: > > Le Monday 28 Mar 2011 à 09:53:52 (+0200), Alain Frisch a écrit : > > > On 03/25/2011 08:01 PM, Guillaume Yziquel wrote: > > > >type error = private int > > > > > > > >external get_error : unit -> error = "zzz" > > > > > > > >You get some error level that you can pattern match as an int, and > > > >this also enforces that all values of type error come from a call to > > > >get_error. > > > > > > You need to coerce explicitly from type error to type int (... :> > > > int), so this is not really different from defining error as an > > > abstract type and exposing a function error->int. > > > > > > -- Alain > > > > Yes, doesn't work for private ints. However, it works for stuff like that, > > though it's not exactly the same thing as a 'private int': > > > > # type t = private A | B;; > > type t = private A | B > > # let x : t = Obj.magic 0;; > > val x : t = A > > # match x with A -> true | _ -> false;; > > - : bool = true > > # A;; > > Error: Cannot create values of the private type t > > > > I thought it also worked on for ints, and in a sense, I'm surprised that > > you cannot pattern match private ints as ints without a coercion. > > I asked a similar question when private ints were introduced in OCaml 3.11 - full explanation from Jacques as to why in: https://sympa-roc.inria.fr/wws/arc/caml-list/2008-10/msg00375.html Yes an no. From a type inference perspective, that's right. However, you can already do such pattern matching on private row types for variant types. module X : sig type t = private [< `A ] val x : t end = struct type t = [ `A ] let x = `A end match X.x with `A -> () and the X.x is correctly unified with `A. So the type inference issue is solved in this case. What I'm wondering is why, when there is a known way to pattern match on a given base type (like ints or strings), could this behaviour not be extended. The work seems to have already been done for variant types. While making type inference implicitly cross the border of type coercion (as in your post) seems excessive, pattern-matching private ints as you would for private row types seems OK to me. Moreover, I somehow disagree with Jacques when he says: >> 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. There is a point: The first 'private int' would simply be a way to forbid construction, while allowing type-inference to go beyond the :> barrier. The second 'very_private int' would be a way to block type inference. Both would have their use cases. -- Guillaume Yziquel