Re: [Caml-list] Question about polymorphic variants

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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