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.
In this article, we’ll cover both types of quantification.
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
username <- getUsername
log username
userCount <- getUserCount
log userCount
getUsername :: IO String
getUsername = undefined
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:
-
func
’s type variablea
is universally quantified, therefore it can only be instantiated at the use site. - We’re trying to instantiate it at
func
’s definition site (log username
is trying to instantiate the type variablea
withString
andlog userCount
is trying to instantiate the type variableb
withInt
).
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
username <- getUsername
log @String username
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.
For more Haskell tutorials, you can check out our Haskell section or follow us on Twitter.
If you see any issues with the text of the blog or need some help understanding it, you’re welcome to submit an issue in blog’s GitHub repo.
Top comments (0)