Browse thread
Recursive subtyping issue
-
Guillaume Yziquel
-
Andreas Rossberg
-
Guillaume Yziquel
- Goswin von Brederlow
-
Guillaume Yziquel
-
Andreas Rossberg
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-02-27 (11:49) |
From: | Goswin von Brederlow <goswin-v-b@w...> |
Subject: | Re: [Caml-list] Recursive subtyping issue |
Guillaume Yziquel <guillaume.yziquel@citycable.ch> 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