Motivation

Haskell has a type extension called ExistentialQuantification; as such there’s plenty of stuff written about existential types in Haskell (and to be honest, a good chunk is applicable to PureScript, including when you might want to use them).

However, PureScript doesn’t have any compiler support for existential types. So we have to implement them ourselves using the tools the compiler does give us.

Background - existential quantification in logic

In first-order (classical) logic, there are two quantifiers, ‘∀’ (the universal quantifier) and ‘∃’ (the existential quantifier). Briefly, the universal quantifier lets you talk about everything in your domain of discourse (“for all”, “every”, etc) and the existential one lets you talk about some things (“for some”, “there exists”, “there’s at least one”, etc.)

They are not equivalent. However, paired with logical negation “¬”, it’s possible to translate between the two. The rules can be thought of as “¬∀ = ∃¬” (or more formally “¬∀x(P x) ⇔ ∃x(¬(P x)”): “‘it is not the case that everyone is standing up’ is the same as ‘there is someone who is not standing up’”.

In a classical logic, we have double negation elimination (¬¬P → P). With this it’s enough to express an existential quantifier using only negation and a universal quantifier:

1. ∃x (P x) ⇔
2. ¬¬∃x (P x) ⇔
3. ¬∀x¬ (P x)

(in an intuitionistic setting, we don’t have double negation elimination, but we do have the inverse P → ¬¬P).

Background - negation in functional programming (and logic)

Of course, we don’t usually think of having negation types in programming. That’s where another trick from logic comes into play: we also have two propositions, ⊤ (top or truth) and ⊥ (bottom, false, falsum). ⊤ is, of course, always true, and ⊥ is always false. Then we can simulate the negation of a proposition P by the proposition P → ⊥ (P implies false).

In PureScript, we have bottom and top types – they’re known as Void and Unit. Any top type is isomorphic to any other top type, and any bottom type is isomorphic to any other bottom type (briefly, they can be completely characterized by their morphisms – by functions with them as their domain or codomain, and using these you can go from one top/bottom type to any other top/bottom type, respectively).

Hence, the negation of a type a is the type a -> void, where void is any bottom type (like Void).

Implementation

The last piece of the puzzle is what I think of more as a mnemonic than anything. Like we discovered above, all bottom types are isomorphic – so we can also create the bottom type type Bottom = ∀ a. a. So we’ll use something similar to construct our existential type. We already know we want to use the form “¬∀¬”, since we have universal quantification and we know how to construct negations. However, using Void by itself is not much use, so we’ll use a rank-2 type instead:

type Exists f = ∀ r. (∀ a. f a -> r) -> r

or,

newtype Exists f = Exists (∀ r. (∀ a. f a -> r) -> r)

Usage

One of the canonical examples of existential type usage is with the typeclass Show:

newtype Showable = Showable (forall r. (forall a. Show a => a -> r) -> r)

(Question: can we write this using the type Exists from above?) Then we can write a smart constructor:

mkShowable :: ∀ a. Show a -> Showable
mkShowable a = Showable (_ $ a)

What can we do with a value of type Showable? Well, all we can do is show it!

instance showShowable :: Show Showable where
  show (Showable a) = a show

And then we can create a “heterogeneous” array of Showables:

showables :: Array Showable
showables = [mkShowable 1, mkShowable unit, mkShowable "hello"]