## DEV Community Serokell

Posted on • Originally published at serokell.io on

# Universal and Existential Quantification in Haskell

In logic, there are two common quantifiers: the universal quantifier and the existential quantifier. You might recognize them as ∀ (for all) and ∃ (there exists).

They are relevant to Haskellers as well, since both universal and existential quantification are possible in Haskell.

You’ll learn how to:

• Make universal quantification explicit with `ExplicitForAll`.
• Create a heterogeneous list with existential data types.
• Use existentially quantified type variables to make instantiation happen at the definition site.

## Universal quantification

In Haskell, all type variables are universally quantified by default. It just happens implicitly.

As an example, look at the `id` function.

``````id :: a -> a

``````

We can think of it as “for all types aaa, this function takes a value of that type and returns a value of the same type”.

With the `ExplicitForAll` extension, we can write that down explicitly.

``````{-# LANGUAGE ExplicitForAll #-}

id :: forall a. a -> a

``````

The syntax is simple – at the beginning of a function or instance declaration, before any constraints or arguments are used, we use the `forall` quantifier to introduce all type variables that we’ll use later.

Here, we introduce four variables: `a`, `b`, `c`, and `m`:

``````func :: forall a b c m. a -> b -> m c -- OK, it compiles

``````

All type variables that you introduce in your type signature should belong to exactly one `forall`. No more, no less.

``````func :: forall a b c. a -> b -> m c -- Error, type variable `m` is not introduced

``````

Of course, we can also add constraints. For example, we might want to specify that the `m` variable needs an instance of the `Monad` typeclass.

``````func :: forall a b c m. Monad m => a -> b -> m c

``````

So far, it might not seem very useful. Nothing changes when we add the quantifier because it’s already there (although implicit). On its own, `ExplicitForAll` doesn’t do a lot.

However, making the quantification explicit allows us to do some new things. You frequently need it to work with other extensions. Some of them will work better, and some of them just won’t work at all without the `forall` quantifier. :)

### Practical use cases of universal quantification

#### Reordering type variables

With `ExplicitForAll`, you can change the order that type variables appear in the `forall` quantifier.

Why is that useful? Let’s imagine you want to define a function with 10 type variables.

``````veryLongFunction :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

``````

(Yes, there are real-life examples of such functions.)

And when you use it, you want to instantiate the last type variable explicitly.

Instantiation

Before we proceed, a quick note on the instantiation of type variables – the process of plugging in a type to replace a type variable.

You can either let GHC do instantiation implicitly:

``````fst :: forall a b. (a, b) -> a
fst (x, _) = x

pair :: (Int, String)
pair = (1, "a")

-- The argument of `fst` is of type `(Int, String)`,
-- so GHC infers how to instantiate its type variables:
-- a=Int, b=String.
x = fst pair

``````

Or you can do it explicitly with the `TypeApplications` extension:

``````{-# LANGUAGE TypeApplications #-}

-- Explicitly instantiate fst's first type variable to Int
-- and the second type variable to String.
x = fst @Int @String pair

``````

`TypeApplications` assigns types to type variables in the order they appear in the (implicit or explicit) `forall`.

Explicit instantiation with `TypeApplications` is often used to give GHC a hand when it’s having trouble inferring a type or simply to make code more readable.

Now, without an explicit `forall`, you would write something like this:

``````veryLongFunction :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

func = veryLongFunction @_ @_ @_ @_ @_ @_ @_ @_ @_ @Integer ...

``````

Quite long, right? However, this can be simplified with an explicit `forall`:

``````veryLongFunction :: forall j a b c d e f g h i. a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

func = veryLongFunction @Integer ...

``````

Since `j` is the first type variable in the declaration of `veryLongFunction`, you can explicitly instantiate only `j` and omit the others.

### Supporting `ScopedTypeVariables`

A common extension that needs `ExplicitForAll` is `ScopedTypeVariables`.

The code below may seem reasonable, but it will not compile.

``````example :: a -> [a] -> [a]
example x rest = pair ++ rest
where
pair :: [a]
pair = [x, x]

``````

It seems reasonable because it looks like both functions are referring to the same type variable `a`. However, GHC is actually inserting an implicit `forall` in both functions. In other words, each function has its own type variable `a`.

``````example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
where
pair :: forall a. [a]
pair = [x, x]

``````

We can rename one of those type variables to make the issue even more obvious:

``````example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
where
pair :: forall b. [b]
pair = [x, x]

``````

Now it’s clear that `pair` is a polymorphic function that promises to return a list of any type `b`, but its implementation actually returns a list of type `a`.

What we meant to say was that `pair` should be a monomorphic function that return a list of the type `a` declared in `example`.

To fix this, we can enable the `ScopedTypeVariables` extension. With this, the type variables declared in an explicit `forall` will be scoped over any accompanying definitions, like `pair`.

``````{-# LANGUAGE ScopedTypeVariables #-}

example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
where
pair :: [a]
pair = [x, x]

``````

The above are just two of many examples where `ExplicitForAll` is useful. Other extensions that benefit from the usage of `ExplicitForAll` are `LiberalTypeSynonyms`, `RankNTypes`, and many more.

## Existential quantification

As said earlier, besides universal quantification, Haskell also supports existential quantification. This too can be done with the `forall` keyword.

You can do it this way because these two constructions – `(exists x. p x) -> q` and `forall x. (p x -> q)` – are equivalent in terms of first-order predicate logic. For a theoretical proof of this statement, you can check this thread.

In this section, we’ll look at existential quantification in data types and function signatures.

### Existential quantification in data types

First, to declare existentially quantified data types, you need to enable either the `ExistentialQuantification` or the `GADTs` extension.

A classic motivating example are heterogeneous lists. Haskell’s `[]` type represents a homogeneous list: a list whose elements are all of the same type. You can’t have a list where the first element is an `Int` and the second is a `String`.

However, you can emulate a heterogeneous list by wrapping all the elements in an existential type.

You can define an existential type by using `forall` on the left side of the constructor name.

``````data Elem = forall a. MkElem a

``````

This effectively “hides” the element’s type `a` inside the `MkElem` constructor.

``````multitypedList :: [Elem]
multitypedList = [MkElem "a", MkElem 1, MkElem (Just 5)]

``````

This is not very useful, though. When we pattern match on `MkElem`, the type of the inner value is not known at compile time.

``````useElem :: Elem -> Int
useElem (MkElem (x :: Int)) = x + 1
^^^^^^^^
-- • Couldn't match expected type ‘a’ with actual type ‘Int’

``````

There’s nothing we can do with it, not even print it to stdout.

``````printElem :: Elem -> IO ()
printElem (MkElem x) =
print x
^^^^^^^
-- • No instance for (Show a) arising from a use of ‘print’
-- Possible fix:
-- add (Show a) to the context of the data constructor ‘MkElem’

``````

GHC kindly suggests adding a `Show` constraint to the `MkElem` constructor. Now, when we match on `MkElem`, the `Show` instance is brought into scope, and we can print our values.

``````data Elem = forall a. (Show a) => MkElem a

multitypedList :: [Elem]
multitypedList = [MkElem "a", MkElem 1, MkElem (Just 5)]

printElem :: Elem -> IO ()
printElem (MkElem x) =
-- We can use `print` here because we have a `Show a` instance in scope.
print x

main :: IO ()
main = forM_ multitypedList printElem

λ> "a"
λ> 1
λ> Just 5

``````

Note that, since the type variable `a` is “hidden” inside the `MkElem` constructor, you can only use the constraints declared in the constructor. You can’t constrain it any further.

``````allEqual :: Eq ??? => [Elem] -> Bool -- There is no type variable that you can add a constraint to.
allEqual = ...

``````

Another useful example of hiding type variables is the `SomeException` wrapper.

``````data SomeException = forall e. Exception e => SomeException e

``````

All exceptions, upon being thrown, are wrapped in `SomeException`. If you want to catch all thrown exceptions, you can use `catchAll` to catch a `SomeException`.

When you pattern match on the `SomeException` constructor, its `Exception` instance is brought into scope.`Exception` implies `Typeable` and `Show`, so those instances are also brought into scope.

``````exceptionHandler :: SomeException -> IO ()
exceptionHandler (SomeException (ex :: e)) =
-- The following instances are in scope here:
-- `Exception e`, `Typeable e`, `Show e`
...

``````

These three instances are all the information we have about `ex` at compile time. Luckily, the `Typeable` instance we have in scope lets us perform aruntime cast, and that’s exactly what functions like `catch` and `fromException` do under the hood.

### Existential quantification in function signatures

Type variables of a function can also be existentially quantified.

Before proceeding further, let’s first have a look at higher-rank types.

Higher-rank types

By default, Haskell98 supports rank-0 and rank-1 types.

Rank-0 types are just monomorphic types (also called monotypes), i.e. they don’t have any type variables:

``````f :: Int -> Int

``````

Rank-1 types have a `forall` that does not appear to the left of any arrow. The type variables bound by that `forall` are universally quantified.

``````f :: forall a. a -> a

-- Keep in mind that the `->` operator has precedence over `.`
-- so this is equivalent to:
f :: forall a. (a -> a)

``````

By enabling the `RankNTypes` extension, we unlock higher-rank types. Just like higher-order functions take other functions as arguments, higher-rank types take lower-rank types as arguments.

Rank-2 types take a type of rank 1 (but no higher) as an argument. In other words, they may have a `forall` that appears to the left of one arrow. The type variables bound by that `forall` are existentially quantified.

``````f :: (forall a. (a -> a)) -> Int

``````

Similarly, rank-3 types take a type of rank 2 (but no higher) as an argument. The `forall` appears to the left of two arrows.

Here, `a` is universally quantified.

``````f :: ((forall a. (a -> a)) -> Int) -> Int

``````

In general:

• A rank-n type is a function whose highest rank argument is n-1.
• A type variable is universally quantified if it’s bound by a forall appearing to the left of an even number of arrows.
• A type variable is existentially quantified if it’s bound by a forall appearing to the left of an odd number of arrows.

Here’s another example for good measure:

``````f :: forall a. a -> (forall b. Show b => b -> IO ()) -> IO ()

``````

Here, `f` is a rank-2 type with two type variables: a universal type variable `a` and an existential type variable `b`.

But what does it mean for a type variable to be existentially quantified?

In short: whereas universally quantified type variables are instantiated at the “use site” (i.e. the user of the function has to choose which type they want that type variable to be), existentially quantified type variables are instantiated at the “definition site” (where the function is defined). In other words, the function’s definition is free to choose how to instantiate the type variable; but the user of the function is not.

Let’s look at a real-life example. Imagine a function that prints logs while calculating some result. You may want to write logs to the console or to some file. In order to abstract over where the logs are written to, you pass a logging function as an argument.

``````func :: _ -> IO ()
func log = do

userCount <- getUserCount
log userCount

getUserCount :: IO Int
getUserCount = undefined

main :: IO ()
main = do
-- log to the console
func print

-- log to a logfile
func (appendFile "logfile.log" . show)

``````

What type should the `log` function have? Since it logs both `String` and `Int`, one might think that adding a function with signature `a -> IO` and a constraint `Show a` would be enough to implement it.

``````log :: Show a => a -> IO ()

``````

However, if we try this:

``````func :: Show a => (a -> IO ()) -> IO ()
func log = ...

``````

We will see this compiler error:

``````  log username
^^^^^^^^
Couldn't match expected type `a` with actual type `String`...

``````

We get this error because:

1. `func`’s type variable `a` is universally quantified, therefore it can only be instantiated at the use site.
2. We’re trying to instantiate it at `func`’s definition site (`log username` is trying to instantiate the type variable `a` with `String` and `log userCount` is trying to instantiate the type variable `b` with `Int`).

Because we want `a` to be instantiated at `func`’s definition site (rather than its use site), we need `a` to be existentially quantified instead.

``````{-# LANGUAGE RankNTypes #-}

func :: (forall a. Show a => a -> IO ()) -> IO ()

``````

Now the compiler knows that no matter which function we pass to `func`, it must work for any type `a`, and `func`’s definition will be responsible for instantiating it.

``````func :: (forall a. Show a => a -> IO ()) -> IO ()
func log = do

userCount <- getUserCount
log @Int userCount

``````

Note that type applications aren’t strictly necessary here, the compiler is smart enough to infer the right types, but they do help with readability.

### Connection between existential types and existentially quantified variables

Lastly, we should point out that existential types are isomorphic to functions with existentially quantified variables (i.e. they’re equivalent), hence their name.

For example, the `Elem` type we saw earlier is equivalent to the following CPS function:

``````data Elem = forall a. Show a => MkElem a

type Elem' = forall r. (forall a. Show a => a -> r) -> r

``````

And we can prove this isomorphism:

``````elemToElem' :: Elem -> Elem'
elemToElem' (MkElem a) f = f a

elem'ToElem :: Elem' -> Elem
elem'ToElem f = f (\a -> MkElem a)

``````

## Summary

We have taken a look at universal and existential quantification in Haskell. With a few extensions and the `forall` keyword, quantification allows you to further expand the rich type system of the language and to express ideas that were previously impossible.