In type theory, the existential quantifier, \(\exists\) is the dual to the more familiar universal quantifier, \(\forall\) (which expresses parametric polymorphism). Believe it or not, these existentially quantified types can be useful in day-to-day programming in languages like Haskell where you wish to perform some kind of "information hiding". As a simple example, consider this program:

data Showable = forall a. Show a => MkShowable a

We start off by declaring a datatype, `Showable`, with a single constructor, `MkShowable` that has type \(\forall \alpha. (\text{S}\text{how}~\alpha) \Rightarrow \alpha \rightarrow \text{S}\text{how}\text{able}\). This is to say, it injects any value with a `Show` instance into the `Showable` type.

This is really an existentially quantified datatype. However, many newbies are confused by this pronouncement, as it quite clearly uses the `forall` keyword, which introduces **universal** quantification - I'll come back to that at the end of this article.

instance Show Showable where
show (Showable x) = show x

This next chunk of code declares that *any* value of type `Showable` is itself a member of the `Show` type class. We implement it by unpacking the `Showable` value and applying `show` "recursively" to that value. We are able to do this precisely because of the constraint in the `MkShowable` constructor that specified that whatever type gets injected into `Showable` must have a `Show` instance somewhere.

An aside: this construction has something of the flavour of object orientation, as it implements a uniform interface using dynamic dispatch. I'll leave it up to the inimitable Oleg to expand on this point...

showable_stuff :: [Showable]
showable_stuff = [MkShowable 1337, MkShowable "I'm a string!", MkShowable 3.1415]

Here we make use of the marvellous information-hiding properties of the existential to create a list holding values of varying types. All we can know about the elements of the resulting list is that they certainly have a `Show` instance.

main = mapM_ print showable_stuff

This last declaration is just a bit of top-level gunk that outputs all the things in that list to the screen using the `Show` typeclass.

So, that's a pretty interesting technique. But in precisely what sense is it existential, given that we got all this going by using the universal quantifier (the `forall` keyword)? I think the easiest way to look at this problem is using the marvellously useful Curry-Howard correspondence between types and terms in a logic system.

First, remember than the function arrow at the type level (\(\tau_1 \rightarrow \tau_2\)) just corresponds to implication in proofs, and the quantifiers carry through unchanged. Secondly, remember that in the proof system corresponding to simple ML-style types (second-order intuionistic logic) \(\sigma_1 \rightarrow \sigma_2 \equiv \lnot \sigma_1 \lor \sigma_2\). Thirdly, recall that if \(\alpha\) is free in \(\sigma_2\) then \(\forall \alpha. \sigma_1 \lor \sigma_2 \equiv (\forall \alpha. \sigma_1) \lor \sigma_2\). Finally, you need to know that pushing a negation through an existiental or universal quantifier flips the kind of quantifier we have (the statement that an \(x\) does not exist satisfying \(P\) is equivalent to saying that all \(x\)s do not satisfy \(P\)). Now we can gradually manipulate the type of a simple data constructor function into a form that makes it obvious where the existiential comes from. Let's try this example (which doesn't have any typeclasses, since they don't really fit into the classical correspondence):

data K = forall a. MkK a

So `MkK` has type \(\forall \alpha. \alpha \rightarrow K\). Let's push that into the realm of logic and proof and see what we can do:

\[\begin{array}{ccc}\forall \alpha. \alpha \rightarrow K &=& \forall \alpha. \lnot \alpha \lor K\\ &=& (\forall \alpha. \lnot \alpha) \lor K\\ &=& \lnot (\exists \alpha. \alpha) \lor K\\ &=& (\exists \alpha. \alpha) \rightarrow K\end{array}\]

And we're done! We can extract this last proof term back out as a type in our source language without any fuss, and hence from only a few logical rules (which, if you didn't know them, are fairly easy to convince yourself of) we have derived why these constructs are known as "existential". In fact, some Haskell compilers once supported the `exists` keywoard to let you declare them directly, but due to precisely this correspondence between the two quantifiers GHC dropped the extra keyword in favour of just using the `forall` to do both jobs.