Yes, hbc had existential types around 1993.
I've used an encoding of existentials in O'Caml (well F#), and it
works, but I find it painful.
And when a very smart but non-CS person saw it his mind boggled,
whereas he understood the existential version just fine.
On Thu, Oct 16, 2008 at 8:26 AM,
Lennart Augustsson wrote:
We don't need them [existentials] from a theoretical perspective, but in practice I'd rather use existentials than encodinging them in some tricky way.
If the claim that we don't need existentials theoretically is obvious, I don't have the argument. Still, existentials are the recurrent topic on the OCaml list; quite a few people perceive them as a needed feature and their perceived absence as a drawback of OCaml.
The principle of encoding existentials is straightforward: represent the existential datatype by a set of its possible observations. Existentials demonstrate once again what I sloppily call initial-final dichotomy: initial encodings are easier to think of upfront, yet require fancier type systems (second-order types, dependent types, GADTs). Final encodings are elementary, yet take (far) longer to imagine. That difficulty may be just the matter of habit.
BTW, wasn't hbc the first Haskell compiler to introduce existentials?
The performance grounds for existentials are justified, for example, by the following paper
Yasuhiko Minamide, J. Gregory Morrisett and Robert Harper Typed Closure Conversion, POPL 1996, pp. 271--283. http://www.cs.cmu.edu/~rwh/papers/closures/popl96.ps
Many object encodings may be considered instances of the type closure conversion. On the other hand, existential elimination may be seen as an inverse process.