Recursive subtyping issue

Guillaume Yziquel

Andreas Rossberg
 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:  20100227 (10:25) 
From:  Guillaume Yziquel <guillaume.yziquel@c...> 
Subject:  Re: [Camllist] Recursive subtyping issue 
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 Antisymmetric? > yziquel@seldon:~$ ocaml > Objective Caml version 3.11.2 > > # type q = private w and w = private q;; > type q = private w > and w = private q > # let f (x : q) = (x : q :> w);; > val f : q > w = <fun> > # let f (x : q) = (x : w);; > Error: This expression has type q but an expression was expected of type w > # 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. You can move around this specific problem by using contravariant polymorphism, as is done in my previous email, but somehow, you cannot have a recursive subtyping from 'a q to w and from w back to 'a q. There always seem to be something wrong, with a problematic more or less analoguous to adjoint functors in category theory. Hence my last email. All the best,  Guillaume Yziquel http://yziquel.homelinux.org/