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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 6DD82BBAF for ; Sat, 27 Feb 2010 14:11:00 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkUCAO+oiEtV2gB5h2dsb2JhbACDBZgsAQEBCgsIBxUiqSKQGIE0gl1qBIly X-IronPort-AV: E=Sophos;i="4.49,550,1262559600"; d="scan'208";a="57888984" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail4-smtp-sop.national.inria.fr with SMTP; 27 Feb 2010 14:10:59 +0100 Received: from [192.168.0.12] (unknown [85.218.92.99]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal2.citycable.ch (Postfix) with ESMTPA id C759CB1059A; Sat, 27 Feb 2010 14:10:53 +0100 (CET) Message-ID: <4B891A0C.604@citycable.ch> Date: Sat, 27 Feb 2010 14:11:40 +0100 From: Guillaume Yziquel Reply-To: guillaume.yziquel@citycable.ch User-Agent: Mozilla-Thunderbird 2.0.0.22 (X11/20090707) MIME-Version: 1.0 To: Goswin von Brederlow Cc: Andreas Rossberg , OCaml List Subject: Re: [Caml-list] Recursive subtyping issue References: <4B887AED.3090005@citycable.ch> <4B88F32C.3050701@citycable.ch> <87k4tyoq3m.fsf@frosties.localdomain> In-Reply-To: <87k4tyoq3m.fsf@frosties.localdomain> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; guillaume:01 guillaume:01 recursive:01 subtyping: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 Goswin von Brederlow a =C3=A9crit : > Guillaume Yziquel writes: >=20 >> My goal is to implement a type inference barrier. >> >> You can do >> >>> type 'a q =3D 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 =3D private 'a q >> But that doesn't work out this way because of the fact that 'a is unbo= und. >=20 > 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 typ= e > 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=20 binding of libraries written in dynamic languages: You want to have type=20 inference on the side of semantics, hence a typing reflecting this. Bt=20 you also want to type lower-level details about objects. This last=20 sentence is not so true with Python, for instance, but with R, it is=20 (despite the argument I had with Simon Urbanek on the r-devel@ mailing=20 list). You want to have an 'a t type with 'a reflecting the corresponding=20 typing in OCaml. And an 'underlying' type representing the low-level valu= e. Doing 'a t =3D private underlying allows you to create a type inference=20 barrier. However, you also want to be able to cast from underlying to 'a=20 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=20 slow enough and dynamically type-checked at every corner. I'm not happy=20 to add another type-checking layer. > module M : sig > type w =3D Int of int | Float of float Ugly. (IMHO) > type 'a q =3D 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 =3D struct I've been looking all over at this issue, but simply cannot find a way=20 out. While experimenting on this, I've stumbled on a number of quirky=20 issues with the type system. First one: http://ocaml.janestreet.com/?q=3Dnode/26 Second one: > # type 'a q =3D ;; > type 'a q =3D < m : 'a > > # let f : 'a q -> 'a q =3D fun x -> x;; > val f : 'a q -> 'a q =3D > # let o =3D object method m : 'a. 'a -> 'a =3D fun x -> x end;;=20 > val o : < m : 'a. 'a -> 'a > =3D > # 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 > #=20 All these issues seem to be somehow related, in a way I'm not yet able=20 to articulate clearly. --=20 Guillaume Yziquel http://yziquel.homelinux.org/