[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2005-09-05 (12:26) |
From: | Lukasz Stafiniak <lukstafi@g...> |
Subject: | Re: [Caml-list] Existential types |
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