Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel <guillaume.yziquel@citycable.ch>]

Guillaume Yziquel a écrit :
> Andreas Rossberg a écrit :
>> On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote:
>>>> # 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
>>>> #
>>
>> Interesting, but these are vacuous type definitions. In fact, I would 
>> call it a bug that the compiler does not reject them (it does when you 
>> remove at least one of the "private"s).
>> 
>> In any case, I don't quite understand how this pathological behaviour 
>> is supposed to help, because the types are uninhabited anyway.
> 
> From OCaml world exclusively, yes, they are uninhabited. I'm using C code 
> to populate these types. [...]
> 
> you then have an interesting way to type Python code that you want to 
> bring to OCaml.
> 
> That's the purpose.

Got it!

Hope it may be useful for others:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2

The rectypes option is not necessary here.

> # type -'a tau = private q and 'a w = < m : 'a > tau and q = private < > tau;;
> type 'a tau = private q
> and 'a w = < m : 'a > tau
> and q = private <  > tau

We're using the < m : 'a > :> < > subtyping with contravariant 
polymorphism to get q :> < > tau :> < m : 'a > tau = 'a w.

The converse is rather easy: 'a w = < m : 'a > tau :> q.

> # let f : 'a w -> q = fun x -> (x : 'a w :> q);;
> val f : 'a w -> q = <fun>
> # let g : q -> 'a w = fun x -> (x : q :> 'a w);;
> val g : q -> 'a w = <fun>

So this subtyping type checks correctly.

> # let h : 'a w -> q = fun x -> x;;
> Error: This expression has type 'a w = < m : 'a > tau
>        but an expression was expected of type q
> #         

And the two types are not equivalent. As this opens the way to correctly 
typing dynamic languages bindings for OCaml (at least in my humble point 
of view), I'd like to know what the bug/feature

	type q = private w and w = private q with q != w

will become in the future.

-- 
      Guillaume Yziquel
http://yziquel.homelinux.org/