Question about polymorphic variants

Question about polymorphic variants

[Xavier Clerc]

Hello,

I have a question concerning polymorphic variants and type inference.
Formulating my question from the example of section 4.2 in the ocaml  
manual (version 3.08), I define a function f:

let f = function
| `On -> 1
| `Off -> 0

which is inferred as: val f : [< `Off | `On ] -> int

Then, I use this function in the following expression :

List.map f

which is in turn inferred as: _[< `Off | `On ] list -> int list


My question is about the meaning of the leading underscore in the  
inferred type (given that I understand the meaning of the underscore  
in an expression such as "Stack.create ()" that is inferred as: '_a  
Stack.t).


Regards,

Xavier Clerc

Re: [Caml-list] Question about polymorphic variants

[Jacques Garrigue]

From: Xavier Clerc <xcforum@free.fr>
> Then, I use this function in the following expression :
> 
> List.map f
> 
> which is in turn inferred as: _[< `Off | `On ] list -> int list
> 
> My question is about the meaning of the leading underscore in the  
> inferred type (given that I understand the meaning of the underscore  
> in an expression such as "Stack.create ()" that is inferred as: '_a  
> Stack.t).

This is exactly the same meaning: [< `Off | `On] has some form of
flexibility left, which you might see as a type variable, and as such
it obeys the same rules as type variables.

An example close to the above one would be:

# List.map (fun (x,y) -> x+1);;
- : (int * '_a) list -> int list = <fun>

Now you might wonder why '_a cannot be polymorphic in the above
example. That is, could there really be a definition of List.map such
that the polymorphic type would be dangerous (causing a segmentation
fault for instance.) The answer is yes, with a counter-example using
the difference in representation between normal arrays and float
arrays.
Actually, since this counter-example wouldn't apply to the above case
of polymorphic variants, this would probably be safe to leave the
polymorphic variant type as polymorphic...

Jacques Garrigue

Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc]

Le 28 oct. 05 à 13:59, Jacques Garrigue a écrit :

> From: Xavier Clerc <xcforum@free.fr>
>
>> Then, I use this function in the following expression :
>>
>> List.map f
>>
>> which is in turn inferred as: _[< `Off | `On ] list -> int list
>>
>> My question is about the meaning of the leading underscore in the
>> inferred type (given that I understand the meaning of the underscore
>> in an expression such as "Stack.create ()" that is inferred as: '_a
>> Stack.t).
>>
>
> This is exactly the same meaning: [< `Off | `On] has some form of
> flexibility left, which you might see as a type variable, and as such
> it obeys the same rules as type variables.
>
> An example close to the above one would be:
>
> # List.map (fun (x,y) -> x+1);;
> - : (int * '_a) list -> int list = <fun>
>
> Now you might wonder why '_a cannot be polymorphic in the above
> example. That is, could there really be a definition of List.map such
> that the polymorphic type would be dangerous (causing a segmentation
> fault for instance.)

This is indeed the question I was asking to myself ...


> The answer is yes, with a counter-example using
> the difference in representation between normal arrays and float
> arrays.

In this counter-example, it is not clear to me whether the possible  
problem is type-related or runtime-related. I mean, would this  
counter-example still hold if arrays were both boxed or both unboxed ?


> Actually, since this counter-example wouldn't apply to the above case
> of polymorphic variants, this would probably be safe to leave the
> polymorphic variant type as polymorphic...

Does this mean that inferring "[< `Off | `On] list -> int list" would  
be perfectly safe in the example above ?
(by saying so, I am not pleading for any compiler change, I am just  
trying to organize my thoughts)



Thanks for you clear (and fast) answer.

Regards

Re: [Caml-list] Question about polymorphic variants

[Jacques Garrigue]

From: Xavier Clerc <xcforum@free.fr>

> > An example close to the above one would be:
> >
> > # List.map (fun (x,y) -> x+1);;
> > - : (int * '_a) list -> int list = <fun>
> >
> > Now you might wonder why '_a cannot be polymorphic in the above
> > example. That is, could there really be a definition of List.map such
> > that the polymorphic type would be dangerous (causing a segmentation
> > fault for instance.)
> 
> This is indeed the question I was asking to myself ...
> 
> 
> > The answer is yes, with a counter-example using
> > the difference in representation between normal arrays and float
> > arrays.
> 
> In this counter-example, it is not clear to me whether the possible  
> problem is type-related or runtime-related. I mean, would this  
> counter-example still hold if arrays were both boxed or both unboxed ?

No, the difference in representation is essential here.

But at the type level, this problem can be expressed a bit
differently: whether it is safe to add a "top" to the type system,
allowing any type to be coerced to it. While some languages might
allow that, there is no fundamental reason it should be so (an this is
indeed not the case in ocaml.)
If we cannot assume the existence of such a type, then we cannot prove
that polymorphism in this case would be safe.

Note that the property used by the relaxed value restriction, that
one can always add safely a "bottom" to the type system, is much more
reasonable, as it's only assumption is that the representation of
values depend only on (typed) values, not on types alone. This is
valid in ocaml, but some other language might still break it.
> 
> > Actually, since this counter-example wouldn't apply to the above case
> > of polymorphic variants, this would probably be safe to leave the
> > polymorphic variant type as polymorphic...
> 
> Does this mean that inferring "[< `Off | `On] list -> int list" would  
> be perfectly safe in the example above ?
> (by saying so, I am not pleading for any compiler change, I am just  
> trying to organize my thoughts)

I believe so, but I don't have a proof ready for that.
One way to do it would be to prove that any instance of [< `Off | `On]
is a subtype of [ `Off | `On ], which sounds trivial in this case.
So I would say this should apply to both [< ... ] types (closed
polymorphic variants, including the [< ... > ...] case) and <...; ..>
types (extensible object types.) But not to [> ...] types (open
polymorphic variants.)

Jacques Garrigue

Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc]

Le 29 oct. 05 à 02:26, Jacques Garrigue a écrit :

[...]

>> In this counter-example, it is not clear to me whether the possible
>> problem is type-related or runtime-related. I mean, would this
>> counter-example still hold if arrays were both boxed or both  
>> unboxed ?
>>
>
> No, the difference in representation is essential here.
>
> But at the type level, this problem can be expressed a bit
> differently: whether it is safe to add a "top" to the type system,
> allowing any type to be coerced to it. While some languages might
> allow that, there is no fundamental reason it should be so (an this is
> indeed not the case in ocaml.)
> If we cannot assume the existence of such a type, then we cannot prove
> that polymorphism in this case would be safe.

I must admit that I don't grasp the link between the existence of a  
"top" type and the inference of a polymorphic type in the given  
examples. I would expect inference of 'a array in arrays example and  
'a in "List.map (fun (x, y) -> x + 1)" and don't see in what  
circumstances such types would not be safe (modulo the array  
representation issue discussed above).
Could you exhibit an example where such inference would be false/ 
unsafe ?


>>> Actually, since this counter-example wouldn't apply to the above  
>>> case
>>> of polymorphic variants, this would probably be safe to leave the
>>> polymorphic variant type as polymorphic...
>>>
>>
>> Does this mean that inferring "[< `Off | `On] list -> int list" would
>> be perfectly safe in the example above ?
>> (by saying so, I am not pleading for any compiler change, I am just
>> trying to organize my thoughts)
>>
>
> I believe so, but I don't have a proof ready for that.
> One way to do it would be to prove that any instance of [< `Off | `On]
> is a subtype of [ `Off | `On ], which sounds trivial in this case.
> So I would say this should apply to both [< ... ] types (closed
> polymorphic variants, including the [< ... > ...] case) and <...; ..>
> types (extensible object types.) But not to [> ...] types (open
> polymorphic variants.)


Well, the only way to get rid of the leading underscore in inferred  
type is to "use" all the tags of the type (that is "converge" toward  
the upper bound of the variant), as in the following toplevel session :

# let f = function
   | `Off -> 0
   | `On -> 1;;
val f : [< `Off | `On ] -> int = <fun>
# let mf = List.map f;;
val mf : _[< `Off | `On ] list -> int list = <fun>
# mf [`On];;
- : int list = [1]
# mf;;
- : _[< `Off | `On > `On ] list -> int list = <fun>
# mf [`Off];;
- : int list = [0]
# mf;;
- : [ `Off | `On ] list -> int list = <fun>

Does this mean that [`Off | `On] list -> int list could be inferred  
for mf as one can pass [`Off | `On] where [< `Off | `On] is waited  
(as [`tag1 | `tag2 ... | `tagn] is shorthand for [< tag1 | `tag2 ...  
| `tagn > tag1 | `tag2 ... | `tagn]).




I apologize for my questions if they are trivial but I must confess  
that I am having a hard time understanding the subtleties of  
polymorphic variants.


Xavier Clerc

Re: [Caml-list] Question about polymorphic variants

[Jacques Garrigue]

From: Xavier Clerc <xcforum@free.fr>

> I must admit that I don't grasp the link between the existence of a  
> "top" type and the inference of a polymorphic type in the given  
> examples. I would expect inference of 'a array in arrays example and  
> 'a in "List.map (fun (x, y) -> x + 1)" and don't see in what  
> circumstances such types would not be safe (modulo the array  
> representation issue discussed above).
> Could you exhibit an example where such inference would be false/ 
> unsafe ?

Here is the concrete counter-example for top. It uses the (unsafe) Obj
module to produce a segmentation fault, but through an operation that
most people would suppose to be safe.

# let l = [| Obj.repr 1.0 |];;
val l : Obj.t array = [|<abstr>|]
# l.(0) <- Obj.repr 1;;
Segmentation fault

How does it relate to top? Essentially, every ocaml value is
represented by a fixed-size word, either an integer or a
pointer to a boxed representation. All Obj.repr does is return its
argument with type Obj.t, the type of all ocaml values, which we can
see as another name for top. So one could assume that Obj.repr is a 
coercion to top. The trouble, as you can see here, is that Obj.t
itself appears to be unsafe. Here l is created as an array, initialized
with a float. This means that internally it will get a float array
representation. Now when we try to put an integer into it, it will try
to use the float array assignment operation, which attempts to
dereference the argument to get its float representation. This
naturally results in a segmentation fault.
As a result we can see here that one assumption in the above must be
false. Since the definition of Obj.repr is exactly that of a coercion
to top, this must mean that adding top to the type system is unsound.

Now, how can I use it to find a problem in the following typing?

  # let g = map (fun x -> 1) ;;
  val g : 'a list -> int list

I first need a "bad" implementation of map, which uses arrays behind the
scene.
  let map f =
    let arr = ref [||] in
    fun l ->
      List.iter
        (fun x -> if !arr = [||] then arr := [|x|] else !arr.(0) <- x) l;
      List.map f l
  val map : ('a -> 'b) -> 'a list -> 'b list

This function just keeps the last list element in a one-element array,
but does nothing with it, so it is exactly equivalent to List.map.
Actually, it cannot do anything bad, as the type system protects me:

  # let g = map (fun x -> 1) ;;
  val g : '_a list -> int list

But now let's assume that Obj.t is really top, and Obj.repr a safe
operation.

  # let g' l = g (List.map Obj.repr l) ;;
  val g' : 'a list -> int list

This time we've got the right type.
Let's use it:

  # g' [1.0];;
  - : int list = [1]
  # g' [1];;
  Segmentation fault


> Well, the only way to get rid of the leading underscore in inferred  
> type is to "use" all the tags of the type (that is "converge" toward  
> the upper bound of the variant), as in the following toplevel session :
> 
> # let f = function
>    | `Off -> 0
>    | `On -> 1;;
> val f : [< `Off | `On ] -> int = <fun>
> # let mf = List.map f;;
> val mf : _[< `Off | `On ] list -> int list = <fun>
> # mf [`On];;
> - : int list = [1]
> # mf;;
> - : _[< `Off | `On > `On ] list -> int list = <fun>
> # mf [`Off];;
> - : int list = [0]
> # mf;;
> - : [ `Off | `On ] list -> int list = <fun>
> 
> Does this mean that [`Off | `On] list -> int list could be inferred  
> for mf as one can pass [`Off | `On] where [< `Off | `On] is waited  
> (as [`tag1 | `tag2 ... | `tagn] is shorthand for [< tag1 | `tag2 ...  
> | `tagn > tag1 | `tag2 ... | `tagn]).

Certainly, as [`Off|`On] is an instance of [< `Off|`On].
But [`Off] or [`On] are other possible instances of [< `Off|`On], so
the latter is more general.
By the way, you can get your intended type directly with a type
annotation.
  # let mf = List.map (f : [`Off|`On] -> _);;
  val mf : [ `Off | `On ] list -> int list = <fun>

Jacques Garrigue

Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc]

Le 1 nov. 05 à 01:27, Jacques Garrigue a écrit :

> From: Xavier Clerc <xcforum@free.fr>
>
>> I must admit that I don't grasp the link between the existence of a
>> "top" type and the inference of a polymorphic type in the given
>> examples. I would expect inference of 'a array in arrays example and
>> 'a in "List.map (fun (x, y) -> x + 1)" and don't see in what
>> circumstances such types would not be safe (modulo the array
>> representation issue discussed above).
>> Could you exhibit an example where such inference would be false/
>> unsafe ?
>
> Here is the concrete counter-example for top. It uses the (unsafe) Obj
> module to produce a segmentation fault, but through an operation that
> most people would suppose to be safe.
>
> # let l = [| Obj.repr 1.0 |];;
> val l : Obj.t array = [|<abstr>|]
> # l.(0) <- Obj.repr 1;;
> Segmentation fault
>
> How does it relate to top? Essentially, every ocaml value is
> represented by a fixed-size word, either an integer or a
> pointer to a boxed representation. All Obj.repr does is return its
> argument with type Obj.t, the type of all ocaml values, which we can
> see as another name for top. So one could assume that Obj.repr is a
> coercion to top. The trouble, as you can see here, is that Obj.t
> itself appears to be unsafe. Here l is created as an array,  
> initialized
> with a float. This means that internally it will get a float array
> representation. Now when we try to put an integer into it, it will try
> to use the float array assignment operation, which attempts to
> dereference the argument to get its float representation. This
> naturally results in a segmentation fault.
> As a result we can see here that one assumption in the above must be
> false. Since the definition of Obj.repr is exactly that of a coercion
> to top, this must mean that adding top to the type system is unsound.

Thanks for your answer, I start to grasp how existence of "top" can  
be related to related to my question.
However, I must confess that I am still puzzled by the fact that your  
example heavily rely on the actual representations of elements and  
not only on their types.
A question is still pending in my mind (in fact, always the same  
question, reformulated to sound like I am making some progress) : if  
the compiler(s) where patched to treat all arrays either as boxed or  
as unboxed, would it be safe to get rid of the leading underscore in  
the inferred type ?
Equivalently, is the use of "top" (using Obj.repr and relatives)  
unsafe only because of concrete representation or for theoretical  
reason ?


>
>> Well, the only way to get rid of the leading underscore in inferred
>> type is to "use" all the tags of the type (that is "converge" toward
>> the upper bound of the variant), as in the following toplevel  
>> session :
>>
>> # let f = function
>>    | `Off -> 0
>>    | `On -> 1;;
>> val f : [< `Off | `On ] -> int = <fun>
>> # let mf = List.map f;;
>> val mf : _[< `Off | `On ] list -> int list = <fun>
>> # mf [`On];;
>> - : int list = [1]
>> # mf;;
>> - : _[< `Off | `On > `On ] list -> int list = <fun>
>> # mf [`Off];;
>> - : int list = [0]
>> # mf;;
>> - : [ `Off | `On ] list -> int list = <fun>
>>
>> Does this mean that [`Off | `On] list -> int list could be inferred
>> for mf as one can pass [`Off | `On] where [< `Off | `On] is waited
>> (as [`tag1 | `tag2 ... | `tagn] is shorthand for [< tag1 | `tag2 ...
>> | `tagn > tag1 | `tag2 ... | `tagn]).
>
> Certainly, as [`Off|`On] is an instance of [< `Off|`On].
> But [`Off] or [`On] are other possible instances of [< `Off|`On], so
> the latter is more general.
> By the way, you can get your intended type directly with a type
> annotation.
>   # let mf = List.map (f : [`Off|`On] -> _);;
>   val mf : [ `Off | `On ] list -> int list = <fun>

Of course.
I am ashamed of my error.

Xavier Clerc

Re: [Caml-list] Question about polymorphic variants

[Jacques Garrigue]

From: Xavier Clerc <xcforum@free.fr>

> Thanks for your answer, I start to grasp how existence of "top" can  
> be related to related to my question.
> However, I must confess that I am still puzzled by the fact that your  
> example heavily rely on the actual representations of elements and  
> not only on their types.
> A question is still pending in my mind (in fact, always the same  
> question, reformulated to sound like I am making some progress) : if  
> the compiler(s) where patched to treat all arrays either as boxed or  
> as unboxed, would it be safe to get rid of the leading underscore in  
> the inferred type ?

Possibly. That is, only if there is nothing else in the representation
of values that makes impossible to assume the existence of top.
This counter-example is simple enough, but to check that top is sound
one would have to check the whole compiler and libraries.
The point is that, if you do not require the existence of top from the
beginning, you may end up doing lots of things that make it impossible
to add it later.

> Equivalently, is the use of "top" (using Obj.repr and relatives)  
> unsafe only because of concrete representation or for theoretical  
> reason ?

Theory is only a way to prove that practice is correct.
There is no theoretical reason not to have top (one can design a
sound theory with top), but if practice does not allow to add top,
then theory does not allow us to generalize contravariant type
variables.

Put differently, it had been known that the existence of top would
matter, implementation might have been different.  Or the conclusion
might have been that assuming top would be too much of a burden in
practice, and it might have been intentionally dropped anyway. Not
allowing a compiler to change representation according to types can be
seen as rather drastic, even if Objective Caml doesn't do it a lot.

Jacques Garrigue

Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc]

Le 7 nov. 05 à 04:11, Jacques Garrigue a écrit :

> From: Xavier Clerc <xcforum@free.fr>
>
>> Thanks for your answer, I start to grasp how existence of "top" can
>> be related to related to my question.
>> However, I must confess that I am still puzzled by the fact that your
>> example heavily rely on the actual representations of elements and
>> not only on their types.
>> A question is still pending in my mind (in fact, always the same
>> question, reformulated to sound like I am making some progress) : if
>> the compiler(s) where patched to treat all arrays either as boxed or
>> as unboxed, would it be safe to get rid of the leading underscore in
>> the inferred type ?
>
> Possibly. That is, only if there is nothing else in the representation
> of values that makes impossible to assume the existence of top.
> This counter-example is simple enough, but to check that top is sound
> one would have to check the whole compiler and libraries.
> The point is that, if you do not require the existence of top from the
> beginning, you may end up doing lots of things that make it impossible
> to add it later.
>
>> Equivalently, is the use of "top" (using Obj.repr and relatives)
>> unsafe only because of concrete representation or for theoretical
>> reason ?
>
> Theory is only a way to prove that practice is correct.
> There is no theoretical reason not to have top (one can design a
> sound theory with top), but if practice does not allow to add top,
> then theory does not allow us to generalize contravariant type
> variables.
>
> Put differently, it had been known that the existence of top would
> matter, implementation might have been different.  Or the conclusion
> might have been that assuming top would be too much of a burden in
> practice, and it might have been intentionally dropped anyway. Not
> allowing a compiler to change representation according to types can be
> seen as rather drastic, even if Objective Caml doesn't do it a lot.
>
> Jacques Garrigue
>

Thanks again for your thorough and precious explanations.

Best regards,

Xavier Clerc