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.