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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id D36FABBAF for ; Sat, 27 Feb 2010 20:52:03 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlgDADcGiUtV2gB5h2dsb2JhbACDBJgtAQEBCgsIBxUiqUaPf4E0gl1qBIly X-IronPort-AV: E=Sophos;i="4.49,551,1262559600"; d="scan'208";a="45681773" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail3-smtp-sop.national.inria.fr with SMTP; 27 Feb 2010 20:52: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 8294A834466; Sat, 27 Feb 2010 20:51:59 +0100 (CET) Message-ID: <4B89780E.5080305@citycable.ch> Date: Sat, 27 Feb 2010 20:52: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 , Goswin von Brederlow 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> <4B896026.2070805@citycable.ch> In-Reply-To: <4B896026.2070805@citycable.ch> 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 ocaml:01 -'a:01 subtyping:01 polymorphism:01 val:01 bindings:01 Guillaume Yziquel a =C3=A9crit : > 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 >>>> # >> >> 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). >>=20 >> In any case, I don't quite understand how this pathological behaviour=20 >> is supposed to help, because the types are uninhabited anyway. >=20 > From OCaml world exclusively, yes, they are uninhabited. I'm using C co= de=20 > to populate these types. [...] >=20 > you then have an interesting way to type Python code that you want to=20 > bring to OCaml. >=20 > That's the purpose. Got it! Hope it may be useful for others: > yziquel@seldon:~$ ocaml > Objective Caml version 3.11.2 The rectypes option is not necessary here. > # type -'a tau =3D private q and 'a w =3D < m : 'a > tau and q =3D priv= ate < > tau;; > type 'a tau =3D private q > and 'a w =3D < m : 'a > tau > and q =3D private < > tau We're using the < m : 'a > :> < > subtyping with contravariant=20 polymorphism to get q :> < > tau :> < m : 'a > tau =3D 'a w. The converse is rather easy: 'a w =3D < m : 'a > tau :> q. > # let f : 'a w -> q =3D fun x -> (x : 'a w :> q);; > val f : 'a w -> q =3D > # let g : q -> 'a w =3D fun x -> (x : q :> 'a w);; > val g : q -> 'a w =3D So this subtyping type checks correctly. > # let h : 'a w -> q =3D fun x -> x;; > Error: This expression has type 'a w =3D < m : 'a > tau > but an expression was expected of type q > # =20 And the two types are not equivalent. As this opens the way to correctly=20 typing dynamic languages bindings for OCaml (at least in my humble point=20 of view), I'd like to know what the bug/feature type q =3D private w and w =3D private q with q !=3D w will become in the future. --=20 Guillaume Yziquel http://yziquel.homelinux.org/