Re: [Caml-list] Question about polymorphic variants

[Xavier Clerc <xcforum@free.fr>]

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