# 24 Days of GHC Extensions: Existential Quantification

I’m happy to announce that today Roman Cheplyaka is going to take over 24 Days of GHC Extensions, and guide us through the very interesting idea of existential quantification. Like yesterday, this extension is much more than mere syntax sugar - it changes the landscape as to how we can write programs. Roman, the stage is yours!

Today we are going to look at existential types, also known as the `ExistentialQuantification` extension. I won’t explain the theory of existential types here; it is admittedly somewhat complex, and good books exist on the subject, to which I’ll refer at the end of this post.

Instead, I want to show one small example of existential types, which hopefully will make you interested enough to go and read those books!

Our example will be a HashMap module similar to Data.HashMap. Specifically, what should an API for such a module look like?

We’ll piggyback on the idea that Ollie described earlier in the series, in the post about Record Wildcards, namely: representing modules as records. In that vein, let’s represent our HashMap module as a record:

``````data HashMap k v = ... -- actual implementation

data HashMapM = HashMapM
{ empty  :: forall k v . HashMap k v
, lookup :: Hashable k => k -> HashMap k v -> Maybe v
, insert :: Hashable k => k -> v -> HashMap k v -> HashMap k v
, union  :: Hashable k => HashMap k v -> HashMap k v -> HashMap k v
}``````

One advantage of doing so is the ability to parameterize this module on a (possibly random) salt, which is important for security reasons. Instead of having one static value of the `HashMapM` type, we’ll have a function that takes a salt and returns a record/module where each operation hashes keys based on that salt:

``mkHashMapM :: Int -> HashMapM``

Unfortunately, if we do that, bad things may happen. Here’s a recent example. Santa’s junior elf, who only recently got into programming, wanted to give Ollie a giraffe for Christmas, so he wrote this code:

``````addGift :: HashMap Name Gift -> HashMap Name Gift
addGift gifts =
let
-- locally bring HashMapM functions into scope
HashMapM{..} = mkHashMapM 42
in
insert "Ollie" giraffe gifts``````

The code compiled, and therefore it worked, or so the elf thought.

Later, when Santa looked up a gift for Ollie, he used his own instantiation of `HashMapM` with a different salt, and the lookup turned up Nothing. (Which maybe isn’t that bad — keeping a giraffe ain’t easy.)

Could we design the HashMap module to prevent such a rookie mistake? Yes, with existential types!

First, we replace the concrete type `HashMap` with a type variable `hm` in the record/module definition:

``````data HashMapM hm = HashMapM
{ empty  :: forall k v . hm k v
, lookup :: Hashable k => k -> hm k v -> Maybe v
, insert :: Hashable k => k -> v -> hm k v -> hm k v
, union  :: Hashable k => hm k v -> hm k v -> hm k v
}``````

Next, we existentially quantify that `hm` variable by creating a wrapper:

``````data HashMapE where
HashMapE :: HashMapM hm -> HashMapE``````

Here I used the GADTs syntax, since it makes it easier to see what’s going on. When we wrap a module in the `HashMapE` constructor, we erase, or forget, the `hm` type variable — notice how `hm` is not part of the result type. There’s also equivalent forall-syntax:

``data HashMapE = forall hm . HashMapE (HashMapM hm)``

The only way to create `HashMapM` should be through this existential wrapper:

``````-- public
mkHashMapE :: Int -> HashMapE
mkHashMapE = HashMapE . mkHashMapM

-- private
mkHashMapM :: Int -> HashMapM HashMap
mkHashMapM salt = HashMapM { {- implementation -} }``````

Now, the important thing about existential types is that every time we unpack `HashMapE`, we get a fresh `hm` type. Operationally, the implementation of `hm` is still `HashMap` (at least until we write another one, which we could also pack into `HashMapE`), but from the type system’s perspective, nothing about `hm` is known.

Let’s try again that elfin code (a variation of it, since we are not allowed to use an existential pattern inside `let`; we need to use `case` instead):

``````addGift :: HashMap Name Gift -> HashMap Name Gift
addGift gifts =
case mkHashMapE 42 of
HashMapE (HashMapM{..}) ->
insert "Ollie" giraffe gifts``````

We’ll get the following error:

``````    Couldn't match type ‘hm’ with ‘HashMap’
‘hm’ is a rigid type variable bound by
a pattern with constructor
HashMapE :: forall (hm :: * -> * -> *). HashMapM hm -> HashMapE,
in a case alternative
Expected type: HashMap Name Gift
Actual type: hm Name Gift``````

(In fact, we shouldn’t expose our implementation type `HashMap` at all; it’s now completely useless.)

But what if we replace `HashMap` with `hm`, just as the error message suggests?

``````addGift :: hm Name Gift -> hm Name Gift
addGift gifts =
case mkHashMapE 42 of
HashMapE (HashMapM{..}) ->
insert "Ollie" giraffe gifts``````

Still no luck:

``````    Couldn't match type ‘hm1’ with ‘hm’
‘hm1’ is a rigid type variable bound by
a pattern with constructor
HashMapE :: forall (hm :: * -> * -> *). HashMapM hm -> HashMapE,
in a case alternative
‘hm’ is a rigid type variable bound by
the type signature for addGift :: hm Name Gift -> hm Name Gift
Expected type: hm Name Gift
Actual type: hm1 Name Gift``````

The compiler is too clever to be tricked by our choice of names; it’ll always create a fresh type each time it unpacks `HashMapE`. So the elf has no choice but to write code the right way, which is of course to take a module as an argument:

``````addGift :: HashMapM hm -> hm Name Gift -> hm Name Gift
addGift mod gifts =
let
HashMapM{..} = mod
in
insert "Ollie" giraffe gifts``````

Notice how in the type signature `hm` of the record/module is the same as `hm` of the gift map. That makes the type checker happy.

And here’s how Santa might use the function his elf has just written:

``````sendGifts =
case mkHashMapE santa'sSecretSalt of
HashMapE (mod@HashMapM{..}) ->
let
gifts = addGift mod empty
in
traverse_ sendGiftToOllie \$ lookup "Ollie" gifts``````

Unlike some other extensions, `ExistentialQuantification` wasn’t introduced for some specific purpose. Existential quantification is a concept from logic and type theory which turned out to be quite useful in practice. Existential types help model and implement:

If you plan to use existential types, I advise you to gain a deeper understanding of them from a book on programming languages, such as Pierce’s Types and Programming Languages (recommended), Mitchell’s Foundations for Programming Languages, or Practical Foundations for Programming Languages (available online for free).

This post is part of 24 Days of GHC Extensions - for more posts like this, check out the calendar.