[Haskell-cafe] existential types (was Re: Optimization problem)
ross at soi.city.ac.uk
Fri Sep 29 05:36:57 EDT 2006
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?
More information about the Haskell-Cafe