Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc <xcforum@free.fr>]

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