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

[Simon Peyton-Jones]

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.

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
sound.

Simon

| -----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
problem)
| 
| On Thu, Sep 28, 2006 at 03:22:25PM +0100, Simon Peyton-Jones wrote:
| > | Does anything go wrong with irrefutable patterns for existential
types?
| >
| > 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