Re: [Caml-list] Recursive subtyping issue

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

Goswin von Brederlow a écrit :
> Guillaume Yziquel <guillaume.yziquel@citycable.ch> writes:
> 
>> 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.
> 
> But then int q :> w :> float q and float q :> w :> int q. That would
> make the whole thing somewhat pointless. Everyone could convert the type
> to anything. I guess it would protect from accidentally passing the
> wrong 'a q while allowing purposefully to pass any 'a q.

Exactly. It's the situation you have when you're trying to do OCaml 
binding of libraries written in dynamic languages: You want to have type 
inference on the side of semantics, hence a typing reflecting this. Bt 
you also want to type lower-level details about objects. This last 
sentence is not so true with Python, for instance, but with R, it is 
(despite the argument I had with Simon Urbanek on the r-devel@ mailing 
list).

You want to have an 'a t type with 'a reflecting the corresponding 
typing in OCaml. And an 'underlying' type representing the low-level value.

Doing 'a t = private underlying allows you to create a type inference 
barrier. However, you also want to be able to cast from underlying to 'a 
t, when you get the result of a function in R or Python, for instance.

So that's exactly the use case you mentionned above.

> Why not supply conversion functions that do any additional checks to
> ensure the conversion is a valid one? Consider the following:

Because that's exactly what I try to avoid. R and Python are already 
slow enough and dynamically type-checked at every corner. I'm not happy 
to add another type-checking layer.

> module M : sig
>   type w = Int of int | Float of float

Ugly. (IMHO)

>   type 'a q = private w
>   val add : 'a q -> 'a q -> 'a q
>   val print : w -> unit
>   val as_int : w -> int q
>   val as_float : w -> float q

Ugly. (IMHO)

> end = struct

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

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
> # 

All these issues seem to be somehow related, in a way I'm not yet able 
to articulate clearly.

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