Bitesize Functional Programming: Universals As Existentials
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.
