Re: [Caml-list] Recursive subtyping issue

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

Goswin von Brederlow a écrit :
>>
>> 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.

Yes and no.

In some sense, when you do bindings of C code, you do have to be 
careful. There's no reason that it should be different for binding 
Python code or R code.

I mean, having a slick binding without dynamic type checks is, from my 
point of view, a good thing.

But this subtyping is for the person binding R or Python code.

The user of the binded code should not see any subtyping. That's the 
goal: having a good framework to do the bindings. Not exposing low level 
R or Python details the the OCaml coder using the bindings.

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

Will have a look at that when I find the time.

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