From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2SCC1rZ030715 for ; Mon, 28 Mar 2011 14:12:01 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApQCADF6kE1RZ90wkWdsb2JhbACkbGAUAQEBAQkLCwcUAyKIa7olhWkEjHc X-IronPort-AV: E=Sophos;i="4.63,255,1299452400"; d="scan'208";a="103813240" Received: from mtaout02-winn.ispmail.ntl.com ([81.103.221.48]) by mail1-smtp-roc.national.inria.fr with ESMTP; 28 Mar 2011 14:11:56 +0200 Received: from aamtaout01-winn.ispmail.ntl.com ([81.103.221.35]) by mtaout02-winn.ispmail.ntl.com (InterMail vM.7.08.04.00 201-2186-134-20080326) with ESMTP id <20110328121155.PFSH6199.mtaout02-winn.ispmail.ntl.com@aamtaout01-winn.ispmail.ntl.com>; Mon, 28 Mar 2011 13:11:55 +0100 Received: from romulus.metastack.com ([81.102.132.77]) by aamtaout01-winn.ispmail.ntl.com (InterMail vG.3.00.04.00 201-2196-133-20080908) with ESMTP id <20110328121155.LFCN20122.aamtaout01-winn.ispmail.ntl.com@romulus.metastack.com>; Mon, 28 Mar 2011 13:11:55 +0100 Received: from remus.metastack.local ([172.16.0.1]) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id p2SCBnOB025002 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=FAIL); Mon, 28 Mar 2011 13:11:49 +0100 Received: from Remus.metastack.local ([fe80::547c:3c42:e1da:eda2]) by Remus.metastack.local ([fe80::547c:3c42:e1da:eda2%11]) with mapi; Mon, 28 Mar 2011 13:11:48 +0100 From: David Allsopp To: "'Guillaume Yziquel'" CC: "'Alain Frisch'" , "'caml-list'" Thread-Topic: [Caml-list] Re: module typing issue Thread-Index: AQHL6sjgGT8J0i0YbEKMp09xW6WxSJQ+GUyAgAAY1ICAAA+egIAABMCAgAAiCICAA+uzAIAALJSAgAAfAWD///jMAIAAEZ9A Date: Mon, 28 Mar 2011 12:11:47 +0000 Message-ID: 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> <20110328115831.GW20598@localhost> In-Reply-To: <20110328115831.GW20598@localhost> Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: Content-Type: text/plain; charset="iso-8859-1" MIME-Version: 1.0 Organization: MetaStack Solutions Ltd. X-Scanned-By: MIMEDefang 2.65 on 81.102.132.77 X-Cloudmark-Analysis: v=1.1 cv=JvdXmxIgLJv2/GthKqHpGJEEHukvLcvELVXUanXFreg= c=1 sm=0 a=GIoHEcz2c30A:10 a=8nJEP1OIZ-IA:10 a=xqWC_Br6kY4A:10 a=ZOzjf2MOAAAA:8 a=Ke0nvQG9exj_0nge_5sA:9 a=4vRYQjKpthoQgIoQ94sA:7 a=ud1GEXEzgdu0guuIL70TaGJlN-cA:4 a=wPNLvfGTeEIA:10 a=HpAAvcLHHh0Zw7uRqdWCyQ==:117 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p2SCC1rZ030715 Subject: RE: [Caml-list] Re: module typing issue 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. > 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) > 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). David