Re: [Caml-list] Recursive subtyping issue

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

Guillaume Yziquel a écrit :
> 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:

Here's a cleaner version, without the object type system:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2
> 
> # type untyped;;
> type untyped
> # type 'a typed = private untyped;;
> type 'a typed = private untyped
> # type -'typing tau = private obj
>   and 'a t = 'a typed tau
>   and obj = private untyped tau;;
> type 'a tau = private obj
> and 'a t = 'a typed tau
> and obj = private untyped tau
> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);;
> val f : 'a t -> obj = <fun>
> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);;
> val g : obj -> 'a t = <fun>
> # 

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