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:
- ∃x (P x) ⇔
- ¬¬∃x (P x) ⇔
- ¬∀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
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
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
newtype Exists f = Exists (∀ r. (∀ a. f a -> r) -> r)
One of the canonical examples of existential type usage is with the typeclass
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
instance showShowable :: Show Showable where show (Showable a) = a show
And then we can create a “heterogeneous” array of
showables :: Array Showable showables = [mkShowable 1, mkShowable unit, mkShowable "hello"]