Published on November 11, 2018
In this post I’m going to give an idea of how existentials can be useful in Haskell. For some time I wanted to write such a post to explain the topic in a way that an older version of me could find helpful, because I still remember the confusion that I felt when I first ran into rank-N types and the terms universal and existential quantification.
I’d like to start from the beginning to make the post useful to as many readers as possible, but I’ll be presenting the basics in a concise form lest make more experienced readers bored.
Type variables and the
Type variables in Haskell are always introduced with the keyword
id :: forall a. a -> a
forall a means exactly what it suggests:
id works for all
will unify with (or will be fixed to) any type that consumer of
Fixing or unifying a variable doesn’t necessarily mean that we’re putting a concrete type in its place. It might as well unify with another variable:
idInt :: Int -> Int idInt = id -- 'a' unifies with 'Int' id' :: forall b. b -> b id' = id -- 'a' unifies with 'b'
What matters is that choice of type for such a variable is made.
By default Haskell type signatures allow us to omit
forall, but it’s still
useful to remember that those
foralls are there. In the post I’ll be
foralls for clarity even when they could have been omitted.
Only variables introduced with
foralls at the beginning of type signature
will be fixed when we use the corresponding function. Other
with independent type variables:
myPrettyPrinter :: forall a. Show a -- 'a' will be fixed when we use 'myPrettyPrinter' => (forall b. Show b => b -> String) -- but not 'b' -> Int -> Bool -> a -> String
When we have two levels of
foralls it’s called rank-2 type. And in general
such constructions are called rank-N types.
Universal and existential quantification
Here are the key things:
- A variable is universally quantified when the consumer of the expression it appears in can choose what it will be.
- A variable is existentially quantified when the consumer of the expression it appears in have to deal with the fact that the choice was made for him.
Both universally and existentially quantified variables are introduced with
forall. There is no
exists in Haskell. In fact, it’s not necessary.
A few examples should help:
In the function
myPrettyPrinterabove, for consumers of
ais universally quantified (we can choose what the type will be)
bis existentially quantified (we have to be prepared to deal with any
bthat will be given to the callback).
Inside the body of
ais existentially quantified because the caller of
myPrettyPrinteralready has chosen the type for us.
When we apply the function with
bin its type signature (the first argument of
myPrettyPrinter), we will be able to choose its concrete type. In the body of
bis universally quantified.
Apart from the cases I have mentioned above there is a way to have existentials by putting values in wrappers that “hide” type variables from signatures.
data Something where Something :: forall a. a -> Something
The constructor accepts any
a we like, but after construction we lose the
type information and pattern matching afterwards only reveals that there is
a, but nothing regarding what it is. Compare this to passing a value
id: we can pass anything to it but we lack any information about the
argument inside of the body of
One thing you can do with existential wrappers that is impossible without them is returning existentially quantified data from a function. The wrapper allows us to avoid unification of existentials with outer context and “escaping” of type variables.
Existentials are always about throwing type information away. Why would we want to do that? The answer is: sometimes we want to work with types that we don’t know at compile time. The types typically depend on the state of external world: they could depend on user’s input, on contents of a file we’re trying to parse, etc. Fortunately Haskell’s type system is powerful enough to allow us to do interesting things even in that case.
How to make use of existentials
We want to work with values of types that we don’t know at compile time, but at run time there are no types at all: they have been erased!
We have to preserve some information about existentially quantified type to
make use of it, otherwise we’ll be in the same position as implementers of
id having a value and only being able to pass it around never doing
anything meaningful with it.
There are various degrees of how much we might want to preserve:
We could have
ain the type
[a]existentially quantified. There are still some things we could do with a value of this type. For example, we could compute length of the list. So knowing nothing about a type is also an option sometimes when it parametrizes another type and we have parametrically-polymorphic functions that work on that type. In this case the set of possible types for
ais open i.e. it can grow.
We could assume that the existentially quantified type has certain properties (instances):
data Showable where Showable :: forall a. Show a => Showable
Showablewill give us the corresponding dictionary back. This allows us to do as much as the knowledge from the attached constraint permits. Again, the set of possible types for
ais open (new instances of
Showcan be defined).
We could use GADTs to restore exact types of existentially quantified variables later:
data EType a where ETypeWord8 :: EType Word8 ETypeInt :: EType Int ETypeFloat :: EType Float ETypeDouble :: EType Double ETypeString :: EType String data Something where Something :: EType a -> a -> Something
Matching on one of the data constructors of
aand after that we are free to do anything with the value of corresponding type because we know it.
With this approach the set of possible types for
ais limited and closed. It can be expanded by changing the definition of
Let’s take a closer look at the last method.
Constraints vs GADTs
How did the approach with GADTs come into existence? Usually we start with the second approach—the one with constraints. Well, let’s see…
- The approach with constraints is good, except as you develop an application you’ll want to know more and more about existential types, so the list of constraints will grow and grow.
It’s even worse though: at some point there will be parts of code that
require incompatible instances, so there won’t be any type
athat satisfies all of them. That’s a problem.
One solution is to add more constructors to the wrapper:
data Something where SomethingIntegral :: forall a. (Show a, Integral a) => a -> Something SomethingFloating :: forall a. (Show a, Floating a) => a -> Something SomethingStringy :: forall a. (Show a, IsString a) => a -> Something
But we haven’t solved the problem properly because now we classify the
existential value by a single pre-chosen criteria: it’s either
IsString. After a short while we are likely to find
ourselves in a situation when we want to use a different criteria that is
completely unrelated to the previously chosen one:
We could want to do something with instances of
Num. In that case we add
Num ato constraints of both data constructors
SomethingFloatingand then we have to pattern match on both and do the same thing in each branch.
We could be interested in an instance that only
Word8has, or only
Stringhave… you see the point.
GADT-driven approach allows us to recover any dictionaries of interest if the actual value is an instance of right type classes. This is as fine-grained as it can be:
reifyIntegralDict :: EType a -> Maybe (Dict (Integral a)) reifyIntegralDict = \case ETypeWord8 -> Just Dict ETypeInt -> Just Dict _ -> Nothing reifyFloatingDict :: EType a -> Maybe (Dict (Floating a)) reifyFloatingDict = \case ETypeFloat -> Just Dict ETypeDouble -> Just Dict _ -> Nothing reifyFooDict :: EType a -> Maybe (Dict (Foo a)) reifyFooDict = \case ETypeWord8 -> Just Dict ETypeString -> Just Dict _ -> Nothing
Example: vector indexed by existential length
You might be thinking that this approach actually amounts to having a sum data type like this:
data EType = ETypeWord8 Word8 | ETypeInt Int | ETypeFloat Float | ETypeDouble Double | ETypeString String
And that is correct in this case, but there also can be:
- Several existentially quantified type variables in a wrapper which leads to combinatorial explosion if we try to enumerate all the combinations.
- Types that are recursively defined and there is no way to enumerate all their variants at all. It could be a vector indexed by existential length or something indexed by a list of type-level.
Here is an example of that—a vector indexed by existential length:
data Vector (n :: Nat) a where Nil :: Vector 0 a Cons :: a -> Vector n a -> Vector (n + 1) a data SomeVector where SomeVector :: KnownNat n => EType a -> Vector n a -> SomeVector
This is a sort of combination of all the three approaches I listed above:
We still can do some things with
Vectorwithout knowing type of its elements or its length.
- We can recover exact type of the elements if we wish.
Luckily, there is enough type-level machinery around
Nats (provided by the
baselibrary) to avoid using singletons, so that knowing that
nis an instance of
KnownNatis sufficient for everything we might want to do.
Type assertions: back to concrete types
It is not always necessary to write programs passing around existentials and
reifying dictionaries as needed, or worse yet, proving things with
(:~:). Some would be inclined to say
that these are the techniques of perverts. In many cases we want to make an
assumption about types and throw an exception when the assumption turns out
to be wrong. This way we can indeed go back to concrete types!
Here is an example of this that uses the definition of
Vector given above:
assertVector :: SomeVector -- we could have parsed this from a file -> Vector 5 Int -- and we only want to continue if the type is this assertVector (SomeVector etype (v :: Vector n a)) = case etype of ETypeInt -> -- reifies that a ~ Int case sameNat (Proxy :: Proxy n) (Proxy :: Proxy 5) of Nothing -> error "expected a vector of length 5" Just Refl -> -- reifies that n ~ 5 v -- now we can return v because we know enough _ -> error "expected a vector of Ints"
The method allows us to write e.g. parsers that return existentials such as
SomeVector while still being able to go to the more comfortable realm of
concrete types later in the program.
A nice conclusion
When rich types and the real world collide, existentials often arise. Yet with due diligence one can tame them and still write beautiful and meaningful programs.