Re: [Caml-list] Existential types

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

From: Lukasz Stafiniak <lukstafi@gmail.com>

> I use an abstract type and a one-way typecast operator to implement
> existential quantification; e. g.
> 
> type 'a t
> type unknown_t
> let some (v : 'a t) = ((Obj.magic v) : unknown_t t)
> 
> Good?

This is a standard technique that is used in labltk for instance.
There should be no problem as long as your ['a t] type has a uniform
representation (i.e. this use of magic only encodes more refined type
distinctions.)
Note that if your values are implemented in ocaml, there is a
reasonable possibility that you could avoid the magic altogether.
And if this is not the case (i.e. implemented in ocaml but magic
required), there is a serious risk that this is actually unsound.
Remember that the function Obj.repr of type ['a -> Obj.t] is unsound,
contrary to the intuition.
Which leads to the rule of thumb: the only "safe" uses of  magic are
when dealing with "unsafe" values (implemented in C.)

By the way, I'm not sure I would call this existantial quantification,
as it is only one-way. This looks more like a simple form of
subtyping.

Jacques Garrigue