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 DA100BBAF for ; Sat, 27 Feb 2010 12:49:51 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArMBALeViEvZSMDjimdsb2JhbACbHBUBAQEKCQwHEQUfuVSEewQ X-IronPort-AV: E=Sophos;i="4.49,550,1262559600"; d="scan'208";a="45670720" Received: from fmmailgate02.web.de ([217.72.192.227]) by mail3-smtp-sop.national.inria.fr with ESMTP; 27 Feb 2010 12:49:51 +0100 Received: from smtp07.web.de (fmsmtp07.dlan.cinetic.de [172.20.5.215]) by fmmailgate02.web.de (Postfix) with ESMTP id C78EA15054B6F; Sat, 27 Feb 2010 12:49:50 +0100 (CET) Received: from [85.216.85.71] (helo=frosties.localdomain) by smtp07.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #314) id 1NlLB8-0007SD-00; Sat, 27 Feb 2010 12:49:50 +0100 Received: from mrvn by frosties.localdomain with local (Exim 4.71) (envelope-from ) id 1NlLB7-0001uZ-M3; Sat, 27 Feb 2010 12:49:49 +0100 From: Goswin von Brederlow To: guillaume.yziquel@citycable.ch Cc: Andreas Rossberg , OCaml List Subject: Re: [Caml-list] Recursive subtyping issue References: <4B887AED.3090005@citycable.ch> <4B88F32C.3050701@citycable.ch> Date: Sat, 27 Feb 2010 12:49:49 +0100 In-Reply-To: <4B88F32C.3050701@citycable.ch> (Guillaume Yziquel's message of "Sat, 27 Feb 2010 11:25:48 +0100") Message-ID: <87k4tyoq3m.fsf@frosties.localdomain> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: goswin-v-b@web.de X-Sender: goswin-v-b@web.de X-Provags-ID: V01U2FsdGVkX18fosBOPDr6c3rxIVPkn7ObSsRa80zBxCp2vBjk 8zoN1/fhV42A1mwO1hBqSHucMt6k6M+4rdNOIM2C2ZrjRmEdz3 sesPz2wOk= X-Spam: no; 0.00; recursive:01 subtyping:01 guillaume:01 guillaume:01 rossberg:01 subtyping:01 recursive:01 inference:01 inference:01 subtype:01 sig:01 val:01 val:01 struct:01 mfg:98 Guillaume Yziquel writes: > Andreas Rossberg a écrit : >> On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote: >>> >>> I've been struggling to have a type system where I could do the >>> following subtyping: >>> >>> 'a t1 :> t2 and t2 :> 'a t1 >> >> Hm, what do you mean? Subtyping ought to be reflexive and >> antisymmetric (although the latter is rarely proved for most type >> systems), which means that your two inequations will hold if and >> only if 'a t1 = t2, regardless of recursive types. >> >> /Andreas ... > Not exactly, it seems. > > My goal is to implement a type inference barrier. > > You can do > >> type 'a q = private w > > and from the type inference point of view, int q and float q are two > distinct types, that you can subtype to a common type. > > What I want is also to have the reverse, i.e. > >> type w = private 'a q > > But that doesn't work out this way because of the fact that 'a is unbound. But then int q :> w :> float q and float q :> w :> int q. That would make the whole thing somewhat pointless. Everyone could convert the type to anything. I guess it would protect from accidentally passing the wrong 'a q while allowing purposefully to pass any 'a q. Why not supply conversion functions that do any additional checks to ensure the conversion is a valid one? Consider the following: module M : sig type w = Int of int | Float of float type 'a q = private w val add : 'a q -> 'a q -> 'a q val print : w -> unit val as_int : w -> int q val as_float : w -> float q end = struct type w = Int of int | Float of float type 'a q = w let add x y = match (x, y) with (Int x, Int y) -> Int (x + y) | (Float x, Float y) -> Float (x +. y) | _ -> assert false(* typesystem failed us *) let print = function Int x -> print_int x | Float x -> print_float x let as_int x = match x with Int _ -> x | Float _ -> assert false let as_float x = match x with Int _ -> assert false | Float _ -> x end # let i = M.as_int (M.Int 1);; val i : int M.q = M.Int 1 # let f = M.as_float (M.Float 1.);; val f : float M.q = M.Float 1. # M.add i i;; - : int M.q = M.Int 2 # M.add i f;; Error: This expression has type float M.q but an expression was expected of type int M.q # M.print (i :> M.w);; 1- : unit = () MfG Goswin