From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id D3EF9BC37 for ; Sun, 28 Feb 2010 10:54:16 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmgCAM3LiUvZSMDjimdsb2JhbACbHRUBAQEKCQwHEQUfuS6EewQ X-IronPort-AV: E=Sophos;i="4.49,554,1262559600"; d="scan'208";a="45625898" Received: from fmmailgate02.web.de ([217.72.192.227]) by mail2-smtp-roc.national.inria.fr with ESMTP; 28 Feb 2010 10:54:16 +0100 Received: from smtp08.web.de (fmsmtp08.dlan.cinetic.de [172.20.5.216]) by fmmailgate02.web.de (Postfix) with ESMTP id 121F315088E14; Sun, 28 Feb 2010 10:54:16 +0100 (CET) Received: from [85.216.85.71] (helo=frosties.localdomain) by smtp08.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #314) id 1Nlfqp-0002hm-00; Sun, 28 Feb 2010 10:54:15 +0100 Received: from mrvn by frosties.localdomain with local (Exim 4.71) (envelope-from ) id 1Nlfqp-0007Kk-8b; Sun, 28 Feb 2010 10:54:15 +0100 From: Goswin von Brederlow To: guillaume.yziquel@citycable.ch Cc: Goswin von Brederlow , Andreas Rossberg , OCaml List Subject: Re: [Caml-list] Recursive subtyping issue References: <4B887AED.3090005@citycable.ch> <4B88F32C.3050701@citycable.ch> <87k4tyoq3m.fsf@frosties.localdomain> <4B891A0C.604@citycable.ch> Date: Sun, 28 Feb 2010 10:54:15 +0100 In-Reply-To: <4B891A0C.604@citycable.ch> (Guillaume Yziquel's message of "Sat, 27 Feb 2010 14:11:40 +0100") Message-ID: <87tyt1r8hk.fsf@frosties.localdomain> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: goswin-v-b@web.de X-Sender: goswin-v-b@web.de X-Provags-ID: V01U2FsdGVkX18V/mx43u7o0meM5voOsEB4zTnBU3YznaQFD3m3 IYY+Hg0Z9kozRR7mzCSv7iGS5V4MiAoKp0VyswU1K2/8hv9Sj8 4nZLspXiI= X-Spam: no; 0.00; recursive:01 subtyping:01 guillaume:01 guillaume:01 inference:01 inference:01 subtype:01 ocaml:01 semantics:01 ocaml:01 low-level:01 type-checked:01 sig:01 val:01 val:01 Guillaume Yziquel writes: > Goswin von Brederlow a écrit : >> Guillaume Yziquel writes: >> >>> My goal is to implement a type inference barrier. >>> >>> You can do >>> >>>> type 'a q = private w >>> and from the type inference point of view, int q and float q are two >>> distinct types, that you can subtype to a common type. >>> >>> What I want is also to have the reverse, i.e. >>> >>>> type w = private 'a q >>> But that doesn't work out this way because of the fact that 'a is unbound. >> >> But then int q :> w :> float q and float q :> w :> int q. That would >> make the whole thing somewhat pointless. Everyone could convert the type >> to anything. I guess it would protect from accidentally passing the >> wrong 'a q while allowing purposefully to pass any 'a q. > > Exactly. It's the situation you have when you're trying to do OCaml > binding of libraries written in dynamic languages: You want to have > type inference on the side of semantics, hence a typing reflecting > this. Bt you also want to type lower-level details about objects. This > last sentence is not so true with Python, for instance, but with R, it > is (despite the argument I had with Simon Urbanek on the r-devel@ > mailing list). > > You want to have an 'a t type with 'a reflecting the corresponding > typing in OCaml. And an 'underlying' type representing the low-level > value. > > Doing 'a t = private underlying allows you to create a type inference > barrier. However, you also want to be able to cast from underlying to > 'a t, when you get the result of a function in R or Python, for > instance. > > So that's exactly the use case you mentionned above. > >> Why not supply conversion functions that do any additional checks to >> ensure the conversion is a valid one? Consider the following: > > Because that's exactly what I try to avoid. R and Python are already > slow enough and dynamically type-checked at every corner. I'm not > happy to add another type-checking layer. But if you do not check then someone can convert a float q into w and back into int q. That would hide the error in the conversion until such a time as the type is later used in some function that does check the type. I would rather have those checks than go hunting for the real error for hours. >> module M : sig >> type w = Int of int | Float of float > > Ugly. (IMHO) > >> type 'a q = private w >> val add : 'a q -> 'a q -> 'a q >> val print : w -> unit >> val as_int : w -> int q >> val as_float : w -> float q > > Ugly. (IMHO) > >> end = struct > > I've been looking all over at this issue, but simply cannot find a way > out. While experimenting on this, I've stumbled on a number of quirky > issues with the type system. > > First one: http://ocaml.janestreet.com/?q=node/26 > > Second one: > >> # type 'a q = ;; >> type 'a q = < m : 'a > >> # let f : 'a q -> 'a q = fun x -> x;; >> val f : 'a q -> 'a q = >> # let o = object method m : 'a. 'a -> 'a = fun x -> x end;; val o : >> < m : 'a. 'a -> 'a > = >> # f o;; >> Error: This expression has type < m : 'a. 'a -> 'a > >> but an expression was expected of type 'b q >> The universal variable 'a would escape its scope >> # > > All these issues seem to be somehow related, in a way I'm not yet able > to articulate clearly. # class ['a] foo = object method map (f : 'a -> 'b) = ((Obj.magic 0) : 'b foo) end;; class ['a] foo : object method map : ('a -> 'a) -> 'a foo end As I recently learned there seems to be no way to make that actualy produce a 'b foo. I think that hits the same problem. MfG Goswin