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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Ross | Paterson | Sent: 29 September 2006 10:37 | To: haskell-cafe@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
