re: the importance of existential-cleansing On the one hand, it's easy to concur that existentials are simpler than the alternatives, the tortuous elimination of CC Shan's "translucent" existential being a case in point. And it's also easy to dismiss such caprice as a penchant for Houdinian escape perversities. Then again, why not? There may never be a real need for anything particular at all, existentials notwithstanding. Affirming that by cracking open the shackles of icons and diabolical shibboleths is arguably the only "real need." Lennart Augustsson wrote:

What do you mean by need? From a theoretical or practical perspective? We don't need them from a theoretical perspective, but in practice I'd rather use existentials than encodinging them in some tricky way.

On Wed, Oct 15, 2008 at 11:05 AM, wrote:

...

The web page begs a question if there is ever any real need for existentials.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- View this message in context: http://www.nabble.com/Object-oriented-programming%2C-Haskell-and-existential... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

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, wrote:

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.