Re: [Caml-list] Recursive subtyping issue

[Goswin von Brederlow <goswin-v-b@web.de>]

Guillaume Yziquel <guillaume.yziquel@citycable.ch> writes:

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

But if you do not check then someone can convert a float q into w and
back into int q. That would hide the error in the conversion until such
a time as the type is later used in some function that does check the
type. I would rather have those checks than go hunting for the real
error for hours.

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

# class ['a] foo = object method map (f : 'a -> 'b) = ((Obj.magic 0) : 'b foo) end;;
class ['a] foo : object method map : ('a -> 'a) -> 'a foo end

As I recently learned there seems to be no way to make that actualy
produce a 'b foo. I think that hits the same problem.

MfG
        Goswin