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.5 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, DNS_FROM_SECURITYSAGE,MAILTO_TO_SPAM_ADDR autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 3A303BB84 for ; Sat, 1 Nov 2008 11:00:55 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAPfFC0mCNhAB/2dsb2JhbADKL4NR X-IronPort-AV: E=Sophos;i="4.33,526,1220220000"; d="scan'208";a="18744332" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail3-smtp-sop.national.inria.fr with ESMTP; 01 Nov 2008 11:00:53 +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 mA1A0fj4022075; Sat, 1 Nov 2008 19:00:41 +0900 (JST) Date: Sat, 01 Nov 2008 19:00:36 +0900 (JST) Message-Id: <20081101.190036.135520839.garrigue@math.nagoya-u.ac.jp> To: thelema314@gmail.com Cc: dra-news@metastack.com, caml-list@yquem.inria.fr Subject: Re: [Caml-list] Private types From: Jacques Garrigue In-Reply-To: <490BB657.5050301@gmail.com> References: <5687D906367C49F981398A97A5966E09@countertenor> <20081031.090842.254669920.garrigue@math.nagoya-u.ac.jp> <490BB657.5050301@gmail.com> 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; subtyping:01 inference:01 coercions:01 subtyping:01 foo:01 inference:01 subtype:01 ocaml:01 edgar:98 typing:01 caml-list:01 functions:01 differs:01 coercion:01 coercion:01 From: Edgar Friendly > > 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? If we limit ourselves to the case where both [x] and [y] contrain no type variables, this si not particularly difficult. However whether they will contain type variables or not depends heavily on how the type inference algorithm proceeds. If they contain type variables, then the situation becomes much more muddled, as these type variables may get instantiated by the subtyping check, and not necessarily as expected. So typing becomes rather unpredictable... > > 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. > > > Code isn't produced by a :> cast. As the internal representation of int > and float differs, a coercion function isn't required. The internal > representation of [private int] and [int] is the same, not to mention > one is exactly the [private] of the other. This was not intended as a complete comparison :-) However, since the coercion function is canonical, I don't think that this difference matters much here. Jacques Garrigue