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 351FFBBAF for ; Sat, 27 Feb 2010 19:10:04 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkUCAE/uiEtV2gB5h2dsb2JhbACDBJgsAQEBCgsIBxUiqSiQAoE0gl1qBIly X-IronPort-AV: E=Sophos;i="4.49,551,1262559600"; d="scan'208";a="45608076" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail2-smtp-roc.national.inria.fr with SMTP; 27 Feb 2010 19:10:03 +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 BEE09B103E5; Sat, 27 Feb 2010 19:09:59 +0100 (CET) Message-ID: <4B896026.2070805@citycable.ch> Date: Sat, 27 Feb 2010 19:10:46 +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: Andreas Rossberg Cc: 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> <76EDF2F2-8B02-4C97-B083-EC74630D8ECA@mpi-sws.org> In-Reply-To: <76EDF2F2-8B02-4C97-B083-EC74630D8ECA@mpi-sws.org> 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 rossberg:01 val:01 bug:01 compiler:01 ocaml:01 bug:01 ocaml:01 subtype:01 node:01 oversight:01 fwiw:01 Andreas Rossberg a =C3=A9crit : > On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote: >>> # type q =3D private w and w =3D private q;; >>> type q =3D private w >>> and w =3D private q >>> # let f (x : q) =3D (x : q :> w);; >>> val f : q -> w =3D >>> # let f (x : q) =3D (x : w);; >>> Error: This expression has type q but an expression was expected of=20 >>> type w >>> # >=20 > Interesting, but these are vacuous type definitions. In fact, I would=20 > call it a bug that the compiler does not reject them (it does when you=20 > remove at least one of the "private"s). It does indeed reject them without the private keyword, even with the=20 rectypes option. I'd appreciate a statement from someone of the OCaml=20 team as to whether this is a bug or a feature. Because I intend to use=20 this feature in my code. > In any case, I don't quite=20 > understand how this pathological behaviour is supposed to help, because= =20 > the types are uninhabited anyway. From OCaml world exclusively, yes, they are inhabited. I'm using C code=20 to populate these types. Say you have what I would like to have, i.e. > type 'a t =3D private obj and obj =3D private 'a t then you could have an > external get_value : string -> obj =3D "my_get_value" you could then retrieve a value for a Python function and another as its=20 argument. They are both obj, but you could subtype them respectively to=20 a (string -> int) t and to a string t. Suppose you also have defined an > external eval : ('a -> 'b) t -> 'a t -> 'b t =3D "my_eval" you then have an interesting way to type Python code that you want to=20 bring to OCaml. That's the purpose. >> 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 >=20 > That's indeed a slight oversight in the design of the module type=20 > system. (FWIW, this is possible in SML.) Very probably. It seems that the author, 'skweeks', comes from the SML=20 world. >> 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;; val o= : <=20 >>> 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 > This example would require full impredicative polymorphism, because you= =20 > would need to instantiate 'a q with a polymorphic type. Yes. > The ML type=20 > system does not support that, because it generally makes type inference= =20 > undecidable. Could you sum up, in a nutshell, the argument that concludes to=20 undecidability of such a type system? > But see e.g. Le Botlan & Remy's work on ML^F for a more=20 > powerful approach than what we have today. Thanks. > /Andreas Still looking for workarounds... I've still got a few ideas to develop,=20 but I'va got a feeling that I'm running short on oil, here... --=20 Guillaume Yziquel http://yziquel.homelinux.org/