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 01AB3BBAF for ; Sat, 27 Feb 2010 21:32:14 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYGAEsQiUtV2gB5h2dsb2JhbACDBIwrixByAQEBCgsIBxUiqRuPe4E0gl1qBIly X-IronPort-AV: E=Sophos;i="4.49,551,1262559600"; d="scan'208";a="45611216" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail2-smtp-roc.national.inria.fr with SMTP; 27 Feb 2010 21:32:14 +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 18BDDB10574; Sat, 27 Feb 2010 21:32:11 +0100 (CET) Message-ID: <4B898179.1000600@citycable.ch> Date: Sat, 27 Feb 2010 21:32:57 +0100 From: Guillaume Yziquel Reply-To: guillaume.yziquel@citycable.ch User-Agent: Mozilla-Thunderbird 2.0.0.22 (X11/20090707) MIME-Version: 1.0 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> <4B891A0C.604@citycable.ch> <76EDF2F2-8B02-4C97-B083-EC74630D8ECA@mpi-sws.org> <4B896026.2070805@citycable.ch> <4B89780E.5080305@citycable.ch> In-Reply-To: <4B89780E.5080305@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 untyped:01 untyped:01 val:01 pathological:98 wrote:01 Guillaume Yziquel a =C3=A9crit : > 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=20 >>> you remove at least one of the "private"s). >>> >>> In any case, I don't quite understand how this pathological behaviour= =20 >>> is supposed to help, because the types are uninhabited anyway. >> >> From OCaml world exclusively, yes, they are uninhabited. I'm using C=20 >> code to populate these types. [...] >> >> you then have an interesting way to type Python code that you want to=20 >> bring to OCaml. >> >> That's the purpose. >=20 > Got it! >=20 > Hope it may be useful for others: Here's a cleaner version, without the object type system: > yziquel@seldon:~$ ocaml > Objective Caml version 3.11.2 >=20 > # type untyped;; > type untyped > # type 'a typed =3D private untyped;; > type 'a typed =3D private untyped > # type -'typing tau =3D private obj > and 'a t =3D 'a typed tau > and obj =3D private untyped tau;; > type 'a tau =3D private obj > and 'a t =3D 'a typed tau > and obj =3D private untyped tau > # let f : 'a t -> obj =3D fun x -> (x : 'a t :> obj);; > val f : 'a t -> obj =3D > # let g : obj -> 'a t =3D fun x -> (x : obj :> 'a t);; > val g : obj -> 'a t =3D > #=20 --=20 Guillaume Yziquel http://yziquel.homelinux.org/