Existential vs. Universally quantified types in Haskell

Question

What exactly is the difference between these? I think I understand how existential types work, they are like having a base class in OO without a way to down cast. How are universal types different?

Accelerant

Do you mean universal as in parametric polymorphism? They're like generics that also work with non-object data (Ints, functions etc). – Adulterant

You might find this answer of mine to another question useful. It covers much the same ground as C.A. McCann's below, but from the starting point of RankNTypes. – Eileneeilis

Excellent, thanks. There seems to be no end to this fascinating journey. – Accelerant

Answer 1

The terms "universal" and "existential" here come from the similarly-named quantifiers in predicate logic.

Universal quantification is normally written as ∀, which you can read as "for all", and means roughly what it sounds like: in a logical statement resembling "∀x. ..." whatever is in place of the "..." is true for all possible "x" you could choose from whatever set of things is being quantified over.

Existential quantification is normally written as ∃, which you can read as "there exists", and means that in a logical statement resembling "∃x. ..." whatever is in place of the "..." is true for some unspecified "x" taken from the set of things being quantified over.

In Haskell, the things being quantified over are types (ignoring certain language extensions, at least), our logical statements are also types, and instead of being "true" we think about "can be implemented".

So, a universally quantified type like forall a. a -> a means that, for any possible type "a", we can implement a function whose type is a -> a. And indeed we can:

id :: forall a. a -> a
id x = x

Since a is universally quantified we know nothing about it, and therefore cannot inspect the argument in any way. So id is the only possible function of that type⁽¹⁾.

In Haskell, universal quantification is the "default"--any type variables in a signature are implicitly universally quantified, which is why the type of id is normally written as just a -> a. This is also known as parametric polymorphism, often just called "polymorphism" in Haskell, and in some other languages (e.g., C#) known as "generics".

An existentially quantified type like exists a. a -> a means that, for some particular type "a", we can implement a function whose type is a -> a. Any function will do, so I'll pick one:

func :: exists a. a -> a
func True = False
func False = True

...which is of course the "not" function on booleans. But the catch is that we can't use it as such, because all we know about the type "a" is that it exists. Any information about which type it might be has been discarded, which means we can't apply func to any values.

This is not very useful.

So what can we do with func? Well, we know that it's a function with the same type for its input and output, so we could compose it with itself, for example. Essentially, the only things you can do with something that has an existential type are the things you can do based on the non-existential parts of the type. Similarly, given something of type exists a. [a] we can find its length, or concatenate it to itself, or drop some elements, or anything else we can do to any list.

That last bit brings us back around to universal quantifiers, and the reason why Haskell⁽²⁾ doesn't have existential types directly (my exists above is entirely fictitious, alas): since things with existentially quantified types can only be used with operations that have universally quantified types, we can write the type exists a. a as forall r. (forall a. a -> r) -> r--in other words, for all result types r, given a function that for all types a takes an argument of type a and returns a value of type r, we can get a result of type r.

If it's not clear to you why those are nearly equivalent, note that the overall type is not universally quantified for a--rather, it takes an argument that itself is universally quantified for a, which it can then use with whatever specific type it chooses.

---

As an aside, while Haskell doesn't really have a notion of subtyping in the usual sense, we can treat quantifiers as expressing a form of subtyping, with a hierarchy going from universal to concrete to existential. Something of type forall a. a could be converted to any other type, so it could be seen as a subtype of everything; on the other hand, any type could be converted to the type exists a. a, making that a parent type of everything. Of course, the former is impossible (there are no values of type forall a. a except errors) and the latter is useless (you can't do anything with the type exists a. a), but the analogy works on paper at least. :]

Note that the equivalence between an existential type and a universally quantified argument works for the same reason that variance flips for function inputs.

---

So, the basic idea is roughly that universally quantified types describe things that work the same for any type, while existential types describe things that work with a specific but unknown type.

---

1: Well, not quite--only if we ignore functions that cause errors, such as notId x = undefined, including functions which never terminate, such as loopForever x = loopForever x.

2: Well, GHC. Without extensions, Haskell only has the implicit universal quantifiers and no real way of talking about existential types at all.

Everybody

Thanks for the excellent explanation. I have one doubt: You have stated that exists a. a and forall r. (forall a. a -> r) -> r both are equivalent. How are they actually equal (is there any derivation for that) ? Is it one of the result of institutional logic ? – Ascension

@Sibi: Yes, it's essentially De Morgan's laws as applied to quantifiers; function inputs are negated, logically speaking. There's a similar equivalence between Either a b and forall r. (a -> r, b -> r) -> r which corresponds to "A or B" being the same as "not (not A) and (not B)". – Everybody

Thanks. But how does r come into picture here ? In the initial premise there is no r, but how does it appear when you appear when you apply De morgan's law ? A derivation of forall r. (forall a. a -> r) -> r to the answer will be very helpful. Thanks again for taking out the time to write an excellent answer. – Ascension

@Sibi: Ah, r here is standing in for "false". Technically "false" should correspond to an uninhabited data type (often called Void), but using r instead lets us get values back out. So "not (not A)" would be either (A -> Void) -> Void (which is useless) or forall r. (A -> r) -> r which lets us extract the A value, i.e. double-negation elimination. Look up the connection between logical double-negation and continuation-passing style if you want to know more. – Everybody

Due to duality, forall a. a can be expressed as exists r. (exists a. a -> r) -> r. – Nettles

Answer 2

Bartosz Milewski in his book offers some good insight about why Haskell doesnt need an existential quantifier:

in pseudo-Haskell:

(exists x. p x x) -> c ≅ forall x. p x x -> c

It tells us that a function that takes an existential type is equivalent to a polymorphic function. This makes perfect sense, because such a function must be prepared to handle any one of the types that may be encoded in the existential type. It’s the same principle that tells us that a function that accepts a sum type must be implemented as a case statement, with a tuple of handlers, one for every type present in the sum. Here, the sum type is replaced by a coend, and a family of handlers becomes an end, or a polymorphic function.

Hence, an example of an existentially quantified type in Haskell is

data Sum = forall a. Constructor a    (i.e. forall a. (Constructor_a:: a -> Sum) ≅ Constructor:: (exists a. a) -> Sum)

which can be thought of as a sum data Sum = int | char | bool | .... In contrast, an example of a universally quantified type in Haskell is

data Product = Constructor (forall a. a)

which can be though of as a product data Product = int char bool ....

Glottic