On Fri, 14 Oct 2005, Simon Peyton-Jones wrote:

| In that context, how well-understood is the combination of impredicative | types via boxy types and a proper existential quantifier at the moment? | It's certainly something that has many uses in an industrial context.

Stephanie Weirich, Dimitrios Vytiniotis, and I are currently re-writing our paper about type inference for impredicative polymorphism. I don't think there's any difficulty with existentials, at least when they are wrapped in a data constructor (which is the way GHC deals with existentials at the moment). We'll have a draft done in a couple of weeks. (Until then the paper on my home page is still approximately right.) http://research.microsoft.com/%7Esimonpj/papers/boxy

Can you elaborate on what you had in mind in your last sentence above?

If you manage to avoid explicit boxing as required currently, you can swap out an existing type for an existential type covering a typeclass with minimal code modifications - which is wonderful for refactoring. More generally, they work rather nicely with typeclasses and avoid the need to keep track of whether you're dealing with the boxed existential type or a type that's an instance of the relevant class. -- flippa@flippac.org Performance anxiety leads to premature optimisation