[Haskell-cafe] existential types (was Re: Optimization problem)

[Ross Paterson]

On Fri, Sep 29, 2006 at 11:19:26AM +0100, Simon Peyton-Jones wrote:
> I must be missing your point.  Newtype is just type isomorphism; a new
> name for an existing type.  But there is not existing type "exists x.
> T(x)".  So it's not surprising that newtype doesn't support
> existentials.

And yet newtype does support recursion.

> I've lost track of this thread.

The story so far:
apfelmus: why are there no irrefutable patterns for GADTs?
Conor: because you could use them to write unsafeCoerce
Ross: how about irrefutable patterns (or newtypes) for existential types?
Simon: Try giving the translation into System F + (existential) data types

Copying a notion of datatype from Haskell to Core and then asking for
a translation to that seems to be begging the question.  If your target
really was System F, you could use the standard encoding of existentials
as nested foralls, but there's the problem that Haskell function spaces
differ from System F ones, System F is strongly normalizing, etc.