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 25D7FBBAF for ; Sat, 27 Feb 2010 11:25:19 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ak4DAGKBiEtV2gB5h2dsb2JhbACDBZgrAQEBCgsIBxUiqgyQJoE0gl1qBIly X-IronPort-AV: E=Sophos;i="4.49,549,1262559600"; d="scan'208";a="45596105" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail2-smtp-roc.national.inria.fr with SMTP; 27 Feb 2010 11:25:18 +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 0C59EB10569; Sat, 27 Feb 2010 11:25:02 +0100 (CET) Message-ID: <4B88F32C.3050701@citycable.ch> Date: Sat, 27 Feb 2010 11:25:48 +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> In-Reply-To: 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 subtyping:01 recursive:01 ocaml:01 val:01 inference:01 inference:01 subtype:01 polymorphism:01 functors:01 unbound:01 Andreas Rossberg a =C3=A9crit : > On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote: >> >> I've been struggling to have a type system where I could do the=20 >> following subtyping: >> >> 'a t1 :> t2 and t2 :> 'a t1 >=20 > Hm, what do you mean? Subtyping ought to be reflexive and antisymmetric= =20 > (although the latter is rarely proved for most type systems), which=20 > means that your two inequations will hold if and only if 'a t1 =3D t2,=20 > regardless of recursive types. >=20 > /Andreas Antisymmetric? > yziquel@seldon:~$ ocaml > Objective Caml version 3.11.2 >=20 > # 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 typ= e w > #=20 Not exactly, it seems. 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=20 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 unbound= . You can move around this specific problem by using contravariant=20 polymorphism, as is done in my previous email, but somehow, you cannot=20 have a recursive subtyping from 'a q to w and from w back to 'a q. There=20 always seem to be something wrong, with a problematic more or less=20 analoguous to adjoint functors in category theory. Hence my last email. All the best, --=20 Guillaume Yziquel http://yziquel.homelinux.org/