Re: [Caml-list] Existential types

[Lukasz Stafiniak <lukstafi@gmail.com>]

Nice to know, that this is a standard technique.

2005/9/5, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>:
> [...]
> 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.)

Yes, they are custom values wrapping pointers to C++ objects related
by inheritance.
> 
> 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.
> 
I agree, it is by no means a constructive existential quantification,
and it is a simple form of subtyping based on polymorphism. The
similarity to <exists 'a. 'a t> may be misleading here.

Thank You,
Lukasz