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=2.0 required=5.0 tests=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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 007FCBB84 for ; Sat, 1 Nov 2008 09:20:07 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiIBAA+uC0lRZ90wkWdsb2JhbACKG4l2AQEBAQkLCgcRA7Zug1GDLQ X-IronPort-AV: E=Sophos;i="4.33,526,1220220000"; d="scan'208";a="19452719" Received: from mtaout02-winn.ispmail.ntl.com ([81.103.221.48]) by mail1-smtp-roc.national.inria.fr with ESMTP; 01 Nov 2008 09:20:07 +0100 Received: from aamtaout02-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 <20081101082007.XPAD13155.mtaout02-winn.ispmail.ntl.com@aamtaout02-winn.ispmail.ntl.com>; Sat, 1 Nov 2008 08:20:07 +0000 Received: from romulus.metastack.com ([81.102.132.77]) by aamtaout02-winn.ispmail.ntl.com (InterMail vG.2.02.00.01 201-2161-120-102-20060912) with ESMTP id <20081101082007.SLNF21638.aamtaout02-winn.ispmail.ntl.com@romulus.metastack.com>; Sat, 1 Nov 2008 08:20:07 +0000 Received: from countertenor (cust-62-62-110-94.dyn.versateladsl.be [94.110.62.62]) (authenticated bits=0) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id mA18K0Va028277 (version=TLSv1/SSLv3 cipher=RC4-MD5 bits=128 verify=NO); Sat, 1 Nov 2008 08:20:03 GMT From: "David Allsopp" To: "'Edgar Friendly'" , "'Jacques Garrigue'" Cc: References: <340C8DB35D244173AE527238DB359A19@countertenor> <04092D60-3BB6-49A6-8A04-0BFE3A2081BD@erratique.ch> <5687D906367C49F981398A97A5966E09@countertenor> <20081031.090842.254669920.garrigue@math.nagoya-u.ac.jp> <490BB657.5050301@gmail.com> Subject: RE: [Caml-list] Private types Date: Sat, 1 Nov 2008 09:19:56 +0100 Organization: MetaStack Solutions Ltd. Message-ID: <6788D960DAEA460EABA915DEA52D5CA2@countertenor> MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Mailer: Microsoft Office Outlook 11 In-Reply-To: <490BB657.5050301@gmail.com> Thread-Index: Ack7xH36UbTtRbCzS+KWjc5AkJXqZQAMYaCw X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 X-Scanned-By: MIMEDefang 2.64 on 81.102.132.74 X-Cloudmark-Analysis: v=1.0 c=1 a=7yTadfetKrCqFwz4viEA:9 a=kQd_YAAKE59OXqfBU8-vrJrXeHcA:4 a=tXPUrm4B3N8A:10 X-Spam: no; 0.00; subtyping:01 unification:01 compiler:01 variants:01 checker:01 infers:01 unify:01 coerced:01 compiler:01 variants:01 checker:01 unify:01 subtyping:01 inference:01 coercions:01 Edgar Friendly wrote: > Jacques Garrigue wrote: > > > 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), > > Does the compiler really get any information from an explicit cast that > it can't figure out already? I can't come up with any example. Polymorphic variants. Consider: type t = [ `A of int ] let f (x : t) = let `A n = x in if n mod 2 = 0 then (x : t :> [> t ]) else `B (2 * n) Without the full coercion for x you'll get a type error because the type checker infers that the type of the [if] expression is [t] from the [then] branch and then fails to unify [> `B of int ] with [t] unless the type of [x] is first coerced to [> t ]. If the compiler were to try (x : t : [> t ]) in all those instances I think that would render polymorphic variants pretty unusable ... the type checker needs to know that you meant to do that or everything will unify! > > So the current approach is to completely separate subtyping and type > > inference, and require coercions everywhere subtyping is needed. > > > Would it be particularly difficult to, in the cases where type [x] is > found but type [y] is expected, to try a (foo : x :> y) cast? +1! With reference my previous comment that "the type checker needs to know if you meant that", there's still the option of using fully abstract types if you wanted to avoid this kind of automatic coercion and have, say, positive integers totally distinct from all integers without an explicit cast. All said, I do see Jacques point of wanting to keep coercion and type inference totally separate... though perhaps if coercions were only tried during unification if at least one of the types in question is private that would maintain a certain level of predictability about when they're used automatically? David