Re: [Caml-list] Recursive subtyping issue

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

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).

It does indeed reject them without the private keyword, even with the 
rectypes option. I'd appreciate a statement from someone of the OCaml 
team as to whether this is a bug or a feature. Because I intend to use 
this feature in my code.

> 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 inhabited. I'm using C code 
to populate these types.

Say you have what I would like to have, i.e.

> type 'a t = private obj and obj = private 'a t

then you could have an

> external get_value : string -> obj = "my_get_value"

you could then retrieve a value for a Python function and another as its 
argument. They are both obj, but you could subtype them respectively to 
a (string -> int) t and to a string t.

Suppose you also have defined an

> external eval : ('a -> 'b) t -> 'a t -> 'b t = "my_eval"

you then have an interesting way to type Python code that you want to 
bring to OCaml.

That's the purpose.

>> I've been looking all over at this issue, but simply cannot find a way 
>> out. While experimenting on this, I've stumbled on a number of quirky 
>> issues with the type system.
>>
>> First one: http://ocaml.janestreet.com/?q=node/26
> 
> That's indeed a slight oversight in the design of the module type 
> system. (FWIW, this is possible in SML.)

Very probably. It seems that the author, 'skweeks', comes from the SML 
world.

>> Second one:
>>
>>> # type 'a q = <m : 'a>;;
>>> type 'a q = < m : 'a >
>>> # let f : 'a q -> 'a q = fun x -> x;;
>>> val f : 'a q -> 'a q = <fun>
>>> # let o = object method m : 'a. 'a -> 'a = fun x -> x end;; val o : < 
>>> m : 'a. 'a -> 'a > = <obj>
>>> # f o;;
>>> Error: This expression has type < m : 'a. 'a -> 'a >
>>>       but an expression was expected of type 'b q
>>>       The universal variable 'a would escape its scope
> 
> This example would require full impredicative polymorphism, because you 
> would need to instantiate 'a q with a polymorphic type.

Yes.

> The ML type 
> system does not support that, because it generally makes type inference 
> undecidable.

Could you sum up, in a nutshell, the argument that concludes to 
undecidability of such a type system?

> But see e.g. Le Botlan & Remy's work on ML^F for a more 
> powerful approach than what we have today.

Thanks.

> /Andreas

Still looking for workarounds... I've still got a few ideas to develop, 
but I'va got a feeling that I'm running short on oil, here...

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