Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Recursive subtyping issue
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2010-02-28 (11:07)
From: Guillaume Yziquel <guillaume.yziquel@c...>
Subject: Re: [Caml-list] Recursive subtyping issue
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:
>> 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