Existential types

Existential types

[Lukasz Stafiniak]

Hi!

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?

Best Regards,
Lukasz

Re: [Caml-list] Existential types

[Jacques Garrigue]

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

Re: [Caml-list] Existential types

[Lukasz Stafiniak]

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