What’s the theoretical basis for existential types?

by

First of all, take a look at the “Curry Howard correspondence” which states that the types in a computer program correspond to formulas in intuitionistic logic. Intuitionistic logic is just like the “regular” logic you learned in school but without the law of the excluded middle or double negation elimination:

  • Not an axiom: P ⇔ ¬¬P (but P ⇒ ¬¬P is fine)

  • Not an axiom: P ∨ ¬P

Laws of logic

You are on the right track with DeMorgan’s laws, but first we are going to use them to derive some new ones. The relevant version of DeMorgan’s laws are:

  • ∀x. P(x) = ¬∃x. ¬P(x)
  • ∃x. P(x) = ¬∀x. ¬P(x)

We can derive (∀x. P ⇒ Q(x))  =  P ⇒ (∀x. Q(x)):

  1. (∀x. P ⇒ Q(x))
  2. (∀x. ¬P ∨ Q(x))
  3. ¬P ∨ (∀x. Q(x))
  4. P ⇒ (∀x. Q(x))

And (∀x. Q(x) ⇒ P)  =  (∃x. Q(x)) ⇒ P (this one is used below):

  1. (∀x. Q(x) ⇒ P)
  2. (∀x. ¬Q(x) ∨ P)
  3. (¬¬∀x. ¬Q(x)) ∨ P
  4. (¬∃x. Q(x)) ∨ P
  5. (∃x. Q(x)) ⇒ P

Note that these laws hold in intuitionistic logic as well. The two laws we derived are cited in the paper below.

Simple Types

The simplest types are easy to work with. For example:

data T = Con Int | Nil

The constructors and accessors have the following type signatures:

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

Type Constructors

Now let’s tackle type constructors. Take the following data definition:

data T a = Con a | Nil

This creates two constructors,

Con :: a -> T a
Nil :: T a

Of course, in Haskell, type variables are implicitly universally quantified, so these are really:

Con :: ∀a. a -> T a
Nil :: ∀a. T a

And the accessor is similarly easy:

unCon :: ∀a. T a -> a
unCon (Con x) = x

Quantified types

Let’s add the existential quantifier, ∃, to our original type (the first one, without the type constructor). Rather than introducing it in the type definition, which doesn’t look like logic, introduce it in the constructor / accessor definitions, which do look like logic. We’ll fix the data definition later to match.

Instead of Int, we will now use ∃x. t. Here, t is some kind of type expression.

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

Based on the rules of logic (the second rule above), we can rewrite the type of Con to:

Con :: ∀x. t -> T

When we moved the existential quantifier to the outside (prenex form), it turned into a universal quantifier.

So the following are theoretically equivalent:

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

Except there is no syntax for exists in Haskell.

In non-intuitionistic logic, it is permissible to derive the following from the type of unCon:

unCon :: ∃ T -> t -- invalid!

The reason this is invalid is because such a transformation is not permitted in intuitionistic logic. So it is impossible to write the type for unCon without an exists keyword, and it is impossible to put the type signature in prenex form. It’s hard to make a type checker guaranteed to terminate in such conditions, which is why Haskell doesn’t support arbitrary existential quantifiers.

Sources

“First-class Polymorphism with Type Inference”, Mark P. Jones, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (web)

Leave a Comment

tech