Recursive subtyping issue

Recursive subtyping issue

[Guillaume Yziquel]

Hello.

I've been struggling to have a type system where I could do the 
following subtyping:

'a t1 :> t2  and  t2 :> 'a t1

So I've tried to do the following:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2
> 
> # #rectypes;;
> # module Q = struct
>     type -'a e
>     type 'a q = private w
>     and w = w e
>     and 'a r = 'a q e
>   end;;
> module Q :
>   sig type -'a e type 'a q = private w and w = w e and 'a r = 'a q e end

It almost seems to work:

> # let f x = (x : Q.w Q.e :> 'a Q.q Q.e);;
> val f : Q.w Q.e -> 'a Q.q Q.e = <fun>
> # let f' x = (x : Q.w :> 'a Q.r);;
> val f' : Q.w -> 'a Q.r = <fun>
> # let g x = (x : 'a Q.q :> Q.w);;
> val g : 'a Q.q -> Q.w = <fun>

We can subtype from 'a Q.q to Q.w and from Q.w to 'a Q.r. So I now only 
need to equate 'a Q.r with 'a Q.q in one way or another...

I therefore tried the following, unsuccessfully:

> # module W = struct
>     type -'a e = ('a -> unit) q
>     and 'a q = private w
>     and w = w e
>     and 'a r = 'a q e
>   end;;
> Error: The type abbreviation q is cyclic
> # 

What's going wrong? And how can one get to do the proposed recursive 
subtyping?

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

Re: [Caml-list] Recursive subtyping issue

[Andreas Rossberg]

On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>
> I've been struggling to have a type system where I could do the  
> following subtyping:
>
> 'a t1 :> t2  and  t2 :> 'a t1

Hm, what do you mean? Subtyping ought to be reflexive and  
antisymmetric (although the latter is rarely proved for most type  
systems), which means that your two inequations will hold if and only  
if 'a t1 = t2, regardless of recursive types.

/Andreas

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Andreas Rossberg a écrit :
> On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>>
>> I've been struggling to have a type system where I could do the 
>> following subtyping:
>>
>> 'a t1 :> t2  and  t2 :> 'a t1
> 
> Hm, what do you mean? Subtyping ought to be reflexive and antisymmetric 
> (although the latter is rarely proved for most type systems), which 
> means that your two inequations will hold if and only if 'a t1 = t2, 
> regardless of recursive types.
> 
> /Andreas

Antisymmetric?

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2
> 
> # 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
> # 

Not exactly, it seems.

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.

You can move around this specific problem by using contravariant 
polymorphism, as is done in my previous email, but somehow, you cannot 
have a recursive subtyping from 'a q to w and from w back to 'a q. There 
always seem to be something wrong, with a problematic more or less 
analoguous to adjoint functors in category theory.

Hence my last email.

All the best,

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

Re: [Caml-list] Recursive subtyping issue

[Goswin von Brederlow]

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

> Andreas Rossberg a écrit :
>> On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>>>
>>> I've been struggling to have a type system where I could do the
>>> following subtyping:
>>>
>>> 'a t1 :> t2  and  t2 :> 'a t1
>>
>> Hm, what do you mean? Subtyping ought to be reflexive and
>> antisymmetric (although the latter is rarely proved for most type
>> systems), which means that your two inequations will hold if and
>> only if 'a t1 = t2, regardless of recursive types.
>>
>> /Andreas
...
> Not exactly, it seems.
>
> 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.

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

module M : sig
  type w = Int of int | Float of float
  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
end = struct
  type w = Int of int | Float of float
  type 'a q = w
  let add x y = match (x, y) with
      (Int x, Int y) -> Int (x + y)
    | (Float x, Float y) -> Float (x +. y)
    | _ -> assert false(* typesystem failed us *)
  let print = function
      Int x -> print_int x
    | Float x -> print_float x
  let as_int x = match x with
      Int _ -> x
    | Float _ -> assert false
  let as_float x = match x with
      Int _ -> assert false
    | Float _ -> x
end

# let i = M.as_int (M.Int 1);;
val i : int M.q = M.Int 1

# let f = M.as_float (M.Float 1.);;
val f : float M.q = M.Float 1.

# M.add i i;;
- : int M.q = M.Int 2

# M.add i f;;
Error: This expression has type float M.q
       but an expression was expected of type int M.q

# M.print (i :> M.w);;
1- : unit = ()

MfG
        Goswin

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

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/

Re: [Caml-list] Recursive subtyping issue

[Andreas Rossberg]

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

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Andreas Rossberg a écrit :
> 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).

It does indeed reject them without the private keyword, even with the 
rectypes option. I'd appreciate a statement from someone of the OCaml 
team as to whether this is a bug or a feature. Because I intend to use 
this feature in my code.

> In any case, I don't quite 
> understand how this pathological behaviour is supposed to help, because 
> the types are uninhabited anyway.

 From OCaml world exclusively, yes, they are inhabited. I'm using C code 
to populate these types.

Say you have what I would like to have, i.e.

> type 'a t = private obj and obj = private 'a t

then you could have an

> external get_value : string -> obj = "my_get_value"

you could then retrieve a value for a Python function and another as its 
argument. They are both obj, but you could subtype them respectively to 
a (string -> int) t and to a string t.

Suppose you also have defined an

> external eval : ('a -> 'b) t -> 'a t -> 'b t = "my_eval"

you then have an interesting way to type Python code that you want to 
bring to OCaml.

That's the purpose.

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

Very probably. It seems that the author, 'skweeks', comes from the SML 
world.

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

Yes.

> The ML type 
> system does not support that, because it generally makes type inference 
> undecidable.

Could you sum up, in a nutshell, the argument that concludes to 
undecidability of such a type system?

> But see e.g. Le Botlan & Remy's work on ML^F for a more 
> powerful approach than what we have today.

Thanks.

> /Andreas

Still looking for workarounds... I've still got a few ideas to develop, 
but I'va got a feeling that I'm running short on oil, here...

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

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Guillaume Yziquel a écrit :
> Andreas Rossberg a écrit :
>> 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.
> 
> From OCaml world exclusively, yes, they are uninhabited. I'm using C code 
> to populate these types. [...]
> 
> you then have an interesting way to type Python code that you want to 
> bring to OCaml.
> 
> That's the purpose.

Got it!

Hope it may be useful for others:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2

The rectypes option is not necessary here.

> # type -'a tau = private q and 'a w = < m : 'a > tau and q = private < > tau;;
> type 'a tau = private q
> and 'a w = < m : 'a > tau
> and q = private <  > tau

We're using the < m : 'a > :> < > subtyping with contravariant 
polymorphism to get q :> < > tau :> < m : 'a > tau = 'a w.

The converse is rather easy: 'a w = < m : 'a > tau :> q.

> # let f : 'a w -> q = fun x -> (x : 'a w :> q);;
> val f : 'a w -> q = <fun>
> # let g : q -> 'a w = fun x -> (x : q :> 'a w);;
> val g : q -> 'a w = <fun>

So this subtyping type checks correctly.

> # let h : 'a w -> q = fun x -> x;;
> Error: This expression has type 'a w = < m : 'a > tau
>        but an expression was expected of type q
> #         

And the two types are not equivalent. As this opens the way to correctly 
typing dynamic languages bindings for OCaml (at least in my humble point 
of view), I'd like to know what the bug/feature

	type q = private w and w = private q with q != w

will become in the future.

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

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Guillaume Yziquel a écrit :
> Guillaume Yziquel a écrit :
>> Andreas Rossberg a écrit :
>>> 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.
>>
>> From OCaml world exclusively, yes, they are uninhabited. I'm using C 
>> code to populate these types. [...]
>>
>> you then have an interesting way to type Python code that you want to 
>> bring to OCaml.
>>
>> That's the purpose.
> 
> Got it!
> 
> Hope it may be useful for others:

Here's a cleaner version, without the object type system:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2
> 
> # type untyped;;
> type untyped
> # type 'a typed = private untyped;;
> type 'a typed = private untyped
> # type -'typing tau = private obj
>   and 'a t = 'a typed tau
>   and obj = private untyped tau;;
> type 'a tau = private obj
> and 'a t = 'a typed tau
> and obj = private untyped tau
> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);;
> val f : 'a t -> obj = <fun>
> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);;
> val g : obj -> 'a t = <fun>
> # 

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

Re: [Caml-list] Recursive subtyping issue

[Stéphane Glondu]

Guillaume Yziquel a écrit :
>> # type untyped;;
>> type untyped
>> # type 'a typed = private untyped;;
>> type 'a typed = private untyped
>> # type -'typing tau = private obj
>>   and 'a t = 'a typed tau
>>   and obj = private untyped tau;;
>> type 'a tau = private obj
>> and 'a t = 'a typed tau
>> and obj = private untyped tau
>> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);;
>> val f : 'a t -> obj = <fun>
>> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);;
>> val g : obj -> 'a t = <fun>
>> # 

Why don't you just declare 'a t to be synonym for obj in the
implementation of your module, declare them as abstract in its
interface, and export the specially typed identities f and g?


Cheers,

-- 
Stéphane

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Stéphane Glondu a écrit :
> Guillaume Yziquel a écrit :
>>> # type untyped;;
>>> type untyped
>>> # type 'a typed = private untyped;;
>>> type 'a typed = private untyped
>>> # type -'typing tau = private obj
>>>   and 'a t = 'a typed tau
>>>   and obj = private untyped tau;;
>>> type 'a tau = private obj
>>> and 'a t = 'a typed tau
>>> and obj = private untyped tau
>>> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);;
>>> val f : 'a t -> obj = <fun>
>>> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);;
>>> val g : obj -> 'a t = <fun>
>>> # 
> 
> Why don't you just declare 'a t to be synonym for obj in the
> implementation of your module, declare them as abstract in its
> interface, and export the specially typed identities f and g?

Because subtyping seems more efficient than applying a noop function. 
And this code might run really often, so I do not like very much the 
idea of having noop functions running really often.

Moreover, having conversion functions is not really handy, from a 
syntactic point of view: It's quite convenient to write something like

let f : string -> obj :> string -> float t = blah blah blah...

than doing the explicit, runtime, casting in the definition of f. 
Haven't tried the line above, so do not quote me on this, but using 
covariance and contravariance can make your code cleaner, with less 
parentheses.

What happened is that I was (am currently) doing only the 'a t :> obj 
subtyping in OCaml-R, and I also have a R.cast function to cast from obj 
to 'a t.

I thought this solution was cleaner than having two conversion functions.

I then tried to go the whole way, and get rid of conversion functions 
altogether.

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

Re: [Caml-list] Recursive subtyping issue

[Stéphane Glondu]

Guillaume Yziquel a écrit :
> Because subtyping seems more efficient than applying a noop function.
> And this code might run really often, so I do not like very much the
> idea of having noop functions running really often.

FWIW, I don't think you have any penalty if you declare your identities
as externals like Obj.{repr,obj,magic}. Yuk, some might say... but we
are in the context of bindings to other languages anyway.

> Moreover, having conversion functions is not really handy, from a
> syntactic point of view: It's quite convenient to write something like
> 
> let f : string -> obj :> string -> float t = blah blah blah...
> 
> than doing the explicit, runtime, casting in the definition of f.

It's more convenient for me write letters and parentheses than the
symbol ":>" :-)

IIUC, these conversion function are not to be used often, are they? What
you want is the equivalent of Obj.{repr,obj}, but for values of some
other language, right?

Are you planning to leak your "tau", "typed" and "untyped" types out of
the module? If so, inferred types are likely to refer to those, which
might be very confusing (unless you resort to a lot of type
annotations). If not, you'll have to use explicitly the coercion
functions outside of the module anyway.

-- 
Stéphane

RE: [Caml-list] Recursive subtyping issue

[David Allsopp]

Stéphane Glondu wrote:
> Guillaume Yziquel a écrit :
> > Because subtyping seems more efficient than applying a noop function.
> > And this code might run really often, so I do not like very much the
> > idea of having noop functions running really often.
> 
> FWIW, I don't think you have any penalty if you declare your identities
> as externals like Obj.{repr,obj,magic}. Yuk, some might say... but we
> are in the context of bindings to other languages anyway.
> 
> > Moreover, having conversion functions is not really handy, from a
> > syntactic point of view: It's quite convenient to write something like
> >
> > let f : string -> obj :> string -> float t = blah blah blah...
> >
> > than doing the explicit, runtime, casting in the definition of f.
> 
> It's more convenient for me write letters and parentheses than the
> symbol ":>" :-)

Then you can write a camlp4 syntax extension to convert the casts to x_of_y function calls :o)

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

Stéphane Glondu a écrit :
> Guillaume Yziquel a écrit :
>> Because subtyping seems more efficient than applying a noop function.
>> And this code might run really often, so I do not like very much the
>> idea of having noop functions running really often.
> 
> FWIW, I don't think you have any penalty if you declare your identities
> as externals like Obj.{repr,obj,magic}. Yuk, some might say... but we
> are in the context of bindings to other languages anyway.

Yuk indeed. The subtyping was also a way to avoid Obj.magic in the first 
place and keep doing things cleanly.

I'm not so sure about runtime penalty in this context.

>> Moreover, having conversion functions is not really handy, from a
>> syntactic point of view: It's quite convenient to write something like
>>
>> let f : string -> obj :> string -> float t = blah blah blah...
>>
>> than doing the explicit, runtime, casting in the definition of f.
> 
> It's more convenient for me write letters and parentheses than the
> symbol ":>" :-)

That's a matter of taste, I guess :-)

> IIUC, these conversion function are not to be used often, are they? What
> you want is the equivalent of Obj.{repr,obj}, but for values of some
> other language, right?

Yes, for the values of some other language.

It depends: they are to be used often for people wanting to make 
bindings of R / Python code. (Even tough I plan to use syntax extensions 
to ease the pain, something like 'module Nltk = python module nltk'. But 
that's a long term perspective.

For people using the binded code, subtyping shouldn't be necessary.

> Are you planning to leak your "tau", "typed" and "untyped" types out of
> the module? If so, inferred types are likely to refer to those, which
> might be very confusing (unless you resort to a lot of type
> annotations). If not, you'll have to use explicitly the coercion
> functions outside of the module anyway.

Yes.

I'm not satisfied with this. (Renaming 'tau' to 'wrapped' would be 
better, I guess).

But somehow, I believe that it's an OCaml issue rather than an issue 
with my approach. I mean, why should it be impossible to *express* in 
the .mli file something like type 'a t = private obj and obj = private 
'a t without resorting to extra intermediary types and contravariant 
phantom types? Couldn't we just dump the type inequations and 
co/contra-variance information (which would require another syntax for 
types, I guess)?

But there's another problem for weirder typings that would need 3 
different categories of types (R ?). 2 conversion functions is OK. 6 
conversion functions is clearly a pain... And concerning R's quirky type 
system, I'm probably optimistic with the number 3.

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

RE: [Caml-list] Recursive subtyping issue

[David Allsopp]

Guillaume Yziquel wrote:
> Stéphane Glondu a écrit :
> > Guillaume Yziquel a écrit :
> >>> # type untyped;;
> >>> type untyped
> >>> # type 'a typed = private untyped;;
> >>> type 'a typed = private untyped
> >>> # type -'typing tau = private obj
> >>>   and 'a t = 'a typed tau
> >>>   and obj = private untyped tau;;
> >>> type 'a tau = private obj
> >>> and 'a t = 'a typed tau
> >>> and obj = private untyped tau
> >>> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);; val f : 'a t ->
> >>> obj = <fun> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);; val
> >>> g : obj -> 'a t = <fun> #
> >
> > Why don't you just declare 'a t to be synonym for obj in the
> > implementation of your module, declare them as abstract in its
> > interface, and export the specially typed identities f and g?
> 
> Because subtyping seems more efficient than applying a noop function.

I wholeheartedly agree that doing this in the type system is much cleaner than using noop/coercion functions but I don't think that there's any difference in terms of efficiency. If the noop/coercion functions are correctly coded then they will be of the form:

external foo_of_bar : bar -> foo = "%identity"

in *both* the .ml and .mli file for the module in question. I'm virtually certain that ocamlopt eliminates calls to the %identity primitive.

> And this code might run really often, so I do not like very much the
> idea of having noop functions running really often.

See previous; I don't think it makes a difference (to runtime performance, anyway).

> Moreover, having conversion functions is not really handy, from a
> syntactic point of view: It's quite convenient to write something like
> 
> let f : string -> obj :> string -> float t = blah blah blah...
> 
> than doing the explicit, runtime, casting in the definition of f.

Agreed - this is where your approach is really neat!

<snip>

> I then tried to go the whole way, and get rid of conversion functions
> altogether.

Being pedantic, what you mean is getting rid of *coercion* functions; *conversion* functions could never eliminated because by their nature they are "doing" something (for example, int_of_string constructs a new integer value based on the string value given to it - you could never just trick the type system into using the same value for both in a meaningful way).

This is tremendously clean - as long as the types are clearly documented! The problem is that ocamldoc doesn't let you "document" coercions (by which I mean that having a conversion function provides means for the documentation of that particular usage).


David

Re: [Caml-list] Recursive subtyping issue

[Goswin von Brederlow]

"David Allsopp" <dra-news@metastack.com> writes:

> external foo_of_bar : bar -> foo = "%identity"
>
> in *both* the .ml and .mli file for the module in question. I'm virtually certain that ocamlopt eliminates calls to the %identity primitive.

Where is that documented? I would have written

let foo_of_bar (x : bar) = (x :> foo)

and hoped the inlining would eliminate it.

MfG
        Goswin

RE: [Caml-list] Recursive subtyping issue

[David Allsopp]

Goswin von Brederlow wrote:
> "David Allsopp" <dra-news@metastack.com> writes:
> 
> > external foo_of_bar : bar -> foo = "%identity"
> >
> > in *both* the .ml and .mli file for the module in question. I'm
> virtually certain that ocamlopt eliminates calls to the %identity
> primitive.
> 
> Where is that documented?

The use of external and its benefit in exported signatures is documented in
Chapter 18 of the manual.

I believe I became aware of the %identity special handling as a side-effect
of the discussion in
http://caml.inria.fr/pub/ml-archives/caml-list/2007/04/200afc54d9796dbb7a8d7
5bef70f2496.en.html.

If you look in asmcomp/cmmgen.ml you'll see what I think is the elimination
of Pidentity calls in the code generator.

> I would have written
> 
> let foo_of_bar (x : bar) = (x :> foo)

We're solving two different problems, I think (as you're assuming that bar
can be constrained to type foo) - I'm assuming that all type constraining is
done in the signature of the interface so, without %identity I would simply
have put [let foo_of_bar x = x] of type 'a -> 'a in my module... and then
constrained it as [val foo_of_bar : bar -> foo] in the signature.

It is possible that ocamlopt can recognise (obvious) identity functions as
well, but that's just speculation on my part as I haven't looked.


David

Re: [Caml-list] Recursive subtyping issue

[Goswin von Brederlow]

"David Allsopp" <dra-news@metastack.com> writes:

> Goswin von Brederlow wrote:
>> "David Allsopp" <dra-news@metastack.com> writes:
>> 
>> > external foo_of_bar : bar -> foo = "%identity"
>> >
>> > in *both* the .ml and .mli file for the module in question. I'm
>> virtually certain that ocamlopt eliminates calls to the %identity
>> primitive.
>> 
>> Where is that documented?
>
> The use of external and its benefit in exported signatures is documented in
> Chapter 18 of the manual.
>
> I believe I became aware of the %identity special handling as a side-effect
> of the discussion in
> http://caml.inria.fr/pub/ml-archives/caml-list/2007/04/200afc54d9796dbb7a8d7
> 5bef70f2496.en.html.
>
> If you look in asmcomp/cmmgen.ml you'll see what I think is the elimination
> of Pidentity calls in the code generator.

Meaning it is not documented. :(

>> I would have written
>> 
>> let foo_of_bar (x : bar) = (x :> foo)
>
> We're solving two different problems, I think (as you're assuming that bar
> can be constrained to type foo) - I'm assuming that all type constraining is
> done in the signature of the interface so, without %identity I would simply
> have put [let foo_of_bar x = x] of type 'a -> 'a in my module... and then
> constrained it as [val foo_of_bar : bar -> foo] in the signature.
>
> It is possible that ocamlopt can recognise (obvious) identity functions as
> well, but that's just speculation on my part as I haven't looked.

It probably won't detect it as identity function but it probably always
inlines it and thereby eliminates it. I hope.

MfG
        Goswin

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

David Allsopp a écrit :
> Guillaume Yziquel wrote:
>> Stéphane Glondu a écrit :
>>
>>> Why don't you just declare 'a t to be synonym for obj in the
>>> implementation of your module, declare them as abstract in its
>>> interface, and export the specially typed identities f and g?
>>
>> Because subtyping seems more efficient than applying a noop function.
> 
> I wholeheartedly agree that doing this in the type system is much cleaner than using noop/coercion functions but I don't think that there's any difference in terms of efficiency. If the noop/coercion functions are correctly coded then they will be of the form:
> 
> external foo_of_bar : bar -> foo = "%identity"
> 
> in *both* the .ml and .mli file for the module in question. I'm virtually certain that ocamlopt eliminates calls to the %identity primitive.

yziquel@seldon:~$ grep magic /usr/lib/ocaml/obj.mli
external magic : 'a -> 'b = "%identity"

So far so good.

>> Moreover, having conversion functions is not really handy, from a
>> syntactic point of view: It's quite convenient to write something like
>>
>> let f : string -> obj :> string -> float t = blah blah blah...
>>
>> than doing the explicit, runtime, casting in the definition of f.
> 
> Agreed - this is where your approach is really neat!

I'm not so sure how far we can push the idea. You can, in one ':>', do 
subtyping at every type in the type 'a -> 'b -> 'c. This is quite handy. 
But I'll have to check in which way this can be integrated in the 
calling conventions of, say, Python.

>> I then tried to go the whole way, and get rid of conversion functions
>> altogether.
> 
> Being pedantic, what you mean is getting rid of *coercion* functions; *conversion* functions could never eliminated

OK.

> This is tremendously clean - as long as the types are clearly documented! The problem is that ocamldoc doesn't let you "document" coercions (by which I mean that having a conversion function provides means for the documentation of that particular usage).

Thank you. The ocamldoc problem isn't really a problem, I believe. You 
just have to write it cleanly in bold letters.

What is more a problem is the fact that inferred .mli files tend to 
leave out the contravariance on tau:

	http://caml.inria.fr/mantis/view.php?id=4988

And hence drops part of the subtyping facility.

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

RE: [Caml-list] Recursive subtyping issue

[David Allsopp]

Guillaume Yziquel wrote:
> David Allsopp a écrit :
<snip>
> >
> > external foo_of_bar : bar -> foo = "%identity"
> >
> > in *both* the .ml and .mli file for the module in question. I'm
> virtually certain that ocamlopt eliminates calls to the %identity
> primitive.
> 
> yziquel@seldon:~$ grep magic /usr/lib/ocaml/obj.mli external magic : 'a
> -> 'b = "%identity"
> 
> So far so good.

I don't follow...?

<snip>

> > This is tremendously clean - as long as the types are clearly
> documented! The problem is that ocamldoc doesn't let you "document"
> coercions (by which I mean that having a conversion function provides
> means for the documentation of that particular usage).
> 
> Thank you. The ocamldoc problem isn't really a problem, I believe. You
> just have to write it cleanly in bold letters.
> 
> What is more a problem is the fact that inferred .mli files tend to
> leave out the contravariance on tau:
> 
> 	http://caml.inria.fr/mantis/view.php?id=4988
> 
> And hence drops part of the subtyping facility.

Though that's another good reason for never, ever, ever, ever using inferred .mli files - the signature is part of your code! ocamlc -i is useful only for generating the first cut of the file so that you can double-check (and probably constrain) the inferred type annotations and add ocamldoc comments...


David

Re: [Caml-list] Recursive subtyping issue

[Goswin von Brederlow]

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

Re: [Caml-list] Recursive subtyping issue

[Guillaume Yziquel]

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/