The idea of using existential quantification in data type declarations
was suggested by Laufer (I believe, thought doubtless someone will
correct me), and implemented in Hope+. It's been in Lennart
Augustsson's **hbc** Haskell compiler for several years, and
proved very useful. Here's the idea. Consider the declaration:

data Foo = forall a. MkFoo a (a -> Bool) | Nil |

The data type `Foo` has two constructors with types:

MkFoo :: forall a. a -> (a -> Bool) -> Foo Nil :: Foo |

Notice that the type variable `a` in the type of `MkFoo`
does not appear in the data type itself, which is plain `Foo`.
For example, the following expression is fine:

[MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] |

Here, `(MkFoo 3 even)` packages an integer with a function
`even` that maps an integer to `Bool`; and `MkFoo 'c'
isUpper` packages a character with a compatible function. These
two things are each of type `Foo` and can be put in a list.

What can we do with a value of type `Foo`?. In particular,
what happens when we pattern-match on `MkFoo`?

f (MkFoo val fn) = ??? |

Since all we know about `val` and `fn` is that they
are compatible, the only (useful) thing we can do with them is to
apply `fn` to `val` to get a boolean. For example:

f :: Foo -> Bool f (MkFoo val fn) = fn val |

What this allows us to do is to package heterogenous values together with a bunch of functions that manipulate them, and then treat that collection of packages in a uniform manner. You can express quite a bit of object-oriented-like programming this way.

What has this to do with *existential* quantification?
Simply that `MkFoo` has the (nearly) isomorphic type

MkFoo :: (exists a . (a, a -> Bool)) -> Foo |

But Haskell programmers can safely think of the ordinary
*universally* quantified type given above, thereby avoiding
adding a new existential quantification construct.

An easy extension (implemented in **hbc**) is to allow
arbitrary contexts before the constructor. For example:

data Baz = forall a. Eq a => Baz1 a a | forall b. Show b => Baz2 b (b -> b) |

The two constructors have the types you'd expect:

Baz1 :: forall a. Eq a => a -> a -> Baz Baz2 :: forall b. Show b => b -> (b -> b) -> Baz |

But when pattern matching on `Baz1` the matched values can be compared
for equality, and when pattern matching on `Baz2` the first matched
value can be converted to a string (as well as applying the function to it).
So this program is legal:

f :: Baz -> String f (Baz1 p q) | p == q = "Yes" | otherwise = "No" f (Baz1 v fn) = show (fn v) |

Operationally, in a dictionary-passing implementation, the
constructors `Baz1` and `Baz2` must store the
dictionaries for `Eq` and `Show` respectively, and
extract it on pattern matching.

Notice the way that the syntax fits smoothly with that used for universal quantification earlier.

There are several restrictions on the ways in which existentially-quantified constructors can be use.

When pattern matching, each pattern match introduces a new, distinct, type for each existential type variable. These types cannot be unified with any other type, nor can they escape from the scope of the pattern match. For example, these fragments are incorrect:

Here, the type bound byf1 (MkFoo a f) = a

`MkFoo`"escapes", because`a`is the result of`f1`. One way to see why this is wrong is to ask what type`f1`has:

What is this "f1 :: Foo -> a -- Weird!

`a`" in the result type? Clearly we don't mean this:

The original program is just plain wrong. Here's another sort of errorf1 :: forall a. Foo -> a -- Wrong!

It's ok to sayf2 (Baz1 a b) (Baz1 p q) = a==q

`a==b`or`p==q`, but`a==q`is wrong because it equates the two distinct types arising from the two`Baz1`constructors.You can't pattern-match on an existentially quantified constructor in a

`let`or`where`group of bindings. So this is illegal:

You can only pattern-match on an existentially-quantified constructor in af3 x = a==b where { Baz1 a b = x }

`case`expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is.You can't use existential quantification for

`newtype`declarations. So this is illegal:

Reason: a value of typenewtype T = forall a. Ord a => MkT a

`T`must be represented as a pair of a dictionary for`Ord t`and a value of type`t`. That contradicts the idea that`newtype`should have no concrete representation. You can get just the same efficiency and effect by using`data`instead of`newtype`. If there is no overloading involved, then there is more of a case for allowing an existentially-quantified`newtype`, because the`data`because the`data`version does carry an implementation cost, but single-field existentially quantified constructors aren't much use. So the simple restriction (no existential stuff on`newtype`) stands, unless there are convincing reasons to change it.You can't use

`deriving`to define instances of a data type with existentially quantified data constructors. Reason: in most cases it would not make sense. For example:#

To derivedata T = forall a. MkT [a] deriving( Eq )

`Eq`in the standard way we would need to have equality between the single component of two`MkT`constructors:

Butinstance Eq T where (MkT a) == (MkT b) = ???

`a`and`b`have distinct types, and so can't be compared. It's just about possible to imagine examples in which the derived instance would make sense, but it seems altogether simpler simply to prohibit such declarations. Define your own instances!