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

Simon Peyton-Jones simonpj at microsoft.com
Fri Sep 29 06:19:26 EDT 2006

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

I've lost track of this thread.  Can you re-state the question?  I'm
strongly influence by the question "can we translate this into System F
+ (existential) data types" because (a) that's what GHC does (b) it's an
excellent sanity check.  E.g. if you can, then we know the system is


| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Ross
| Paterson
| Sent: 29 September 2006 10:37
| To: haskell-cafe at haskell.org
| Subject: [Haskell-cafe] existential types (was Re: Optimization
| On Thu, Sep 28, 2006 at 03:22:25PM +0100, Simon Peyton-Jones wrote:
| > | Does anything go wrong with irrefutable patterns for existential
| >
| > Try giving the translation into System F.
| I'm a bit puzzled about this.  A declaration
| 	data Foo = forall a. MkFoo a (a -> Bool)
| is equivalent to
| 	newtype Foo = forall a. Foo (Foo' a)
| 	data Foo' a = MkFoo a (a -> Bool)
| except that you also don't allow existentials with newtypes, for
| similarly unclear reasons.  If you did allow them, you'd certainly
| allow this equivalent of the original irrefutable match:
| 	... case x of
| 		Foo y -> let MkFoo val fn = y in fn val
| So, is there some real issue with existentials and non-termination?
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list