From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2SCV95I031808 for ; Mon, 28 Mar 2011 14:31:09 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuIAAN9+kE1V2gB4mWdsb2JhbAClUwEBAQEBCAsLBxQliGu6Aw2FXASQZQ X-IronPort-AV: E=Sophos;i="4.63,255,1299452400"; d="scan'208";a="95148181" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail2-smtp-roc.national.inria.fr with SMTP; 28 Mar 2011 14:31:04 +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 7E41F12CCFA; Mon, 28 Mar 2011 14:31:02 +0200 (CEST) Received: from yziquel by seldon with local (Exim 4.72) (envelope-from ) id 1Q4BZt-0002yR-1A; Mon, 28 Mar 2011 14:29:49 +0200 Date: Mon, 28 Mar 2011 14:29:48 +0200 From: Guillaume Yziquel To: David Allsopp Cc: "'Alain Frisch'" , "'caml-list'" Message-ID: <20110328122948.GB20598@localhost> References: <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> <20110328115831.GW20598@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 p2SCV95I031808 Subject: Re: [Caml-list] Re: module typing issue Le Monday 28 Mar 2011 à 12:11:47 (+0000), David Allsopp a écrit : > Guillaume Yziquel wrote: > > Le Monday 28 Mar 2011 à 11:29:51 (+0000), David Allsopp a écrit : > > > Guillaume Yziquel wrote: > > > > 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. > > There's nothing special needed to do this - the type of `A is [> `A ] so that unifies with type X.t without any special handling at all. OK, there's no special handling. Type of `A is [> `A] and type of X.x is t = private [< `A ]. But that's hardly different from: Type of 1 is int and type of X.x is t = private int. What I meant is that the fact that 'function `A -> ()' gets properly unified with X.x which is of type 't = private [< `A]' is a solved type inference issue. Because of what private row types mean: you can feed a private row type to a function accepting the correct polymorphic variant types. It isn't the case for private ints. It's not a private row type, but while I understand why type inference is screened by the private keyword, I do not really understand why we couldn't pattern-match it as an int. Except for the fact that you cannot feed a private int to a function accepting an int for type inference reasons (opposite behaviour than for private row types). > > 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. > > There's no extra work been done here - it's just normal type inference (i.e. there are no special cases that have been added for this to work). I'm not completely convinced by the argument against inferring coercions in the type checker, but arguing with Jacques is usually a route to being proven comprehensively wrong :o) I wouldn't complain about that. I like the type hackery flexibility this distinction brings. > > 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. > > There's nothing special going on for private row types - it's simply that the constants (variant or polymorphic variants) can only have only one type where integer constants can have more than one type (sort of - it's the wrong terminology really but from the type inference perspective, it's what's happening). I do not understand the 'integer constants can have more than one type' part of your sentence. > David -- Guillaume Yziquel