Re: [Caml-list] Recursive subtyping issue

[Andreas Rossberg <rossberg@mpi-sws.org>]

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.

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

> 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. The ML  
type system does not support that, because it generally makes type  
inference undecidable. But see e.g. Le Botlan & Remy's work on ML^F  
for a more powerful approach than what we have today.

/Andreas