This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Recursive subtyping issue
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2010-02-27 (10:25) From: Guillaume Yziquel Subject: Re: [Caml-list] 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/

```