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/