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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id A94B1BBAF for ; Sat, 27 Feb 2010 02:52:12 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoDAI8JiEtV2gB4Zmdsb2JhbACDBZgvDQsICBQiqx6QI4E0glxpBIly X-IronPort-AV: E=Sophos;i="4.49,549,1262559600"; d="scan'208";a="53696237" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail1-smtp-roc.national.inria.fr with SMTP; 27 Feb 2010 02:52:12 +0100 Received: from [192.168.0.12] (unknown [85.218.92.99]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal1.citycable.ch (Postfix) with ESMTPA id C546C12C19C; Sat, 27 Feb 2010 02:52:10 +0100 (CET) Message-ID: <4B887AED.3090005@citycable.ch> Date: Sat, 27 Feb 2010 02:52:45 +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: OCaml List Subject: Recursive subtyping issue Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; guillaume:01 guillaume:01 recursive:01 subtyping:01 subtyping:01 ocaml:01 struct:01 -'a:01 sig:01 -'a:01 val:01 val:01 subtype:01 struct:01 abbreviation:01 Hello. I've been struggling to have a type system where I could do the following subtyping: 'a t1 :> t2 and t2 :> 'a t1 So I've tried to do the following: > yziquel@seldon:~$ ocaml > Objective Caml version 3.11.2 > > # #rectypes;; > # module Q = struct > type -'a e > type 'a q = private w > and w = w e > and 'a r = 'a q e > end;; > module Q : > sig type -'a e type 'a q = private w and w = w e and 'a r = 'a q e end It almost seems to work: > # let f x = (x : Q.w Q.e :> 'a Q.q Q.e);; > val f : Q.w Q.e -> 'a Q.q Q.e = > # let f' x = (x : Q.w :> 'a Q.r);; > val f' : Q.w -> 'a Q.r = > # let g x = (x : 'a Q.q :> Q.w);; > val g : 'a Q.q -> Q.w = We can subtype from 'a Q.q to Q.w and from Q.w to 'a Q.r. So I now only need to equate 'a Q.r with 'a Q.q in one way or another... I therefore tried the following, unsuccessfully: > # module W = struct > type -'a e = ('a -> unit) q > and 'a q = private w > and w = w e > and 'a r = 'a q e > end;; > Error: The type abbreviation q is cyclic > # What's going wrong? And how can one get to do the proposed recursive subtyping? -- Guillaume Yziquel http://yziquel.homelinux.org/