Propositions as Types, and the Universal and Existential Quantifiers

    I have noticed that individuals new to dependent type theory (myself included) initially have a hard time understanding the new paradigm of types-as-propositions required for understating dependent type theory. Personally, before I had any (informal) learning about type theory I considered types to be analogous to sets, and that the Liskov substitution principle reflected the notion that propositions that held true of any set A should hold true of a set B ⊆ A. This idea of a set as a collection of objects defined (usually) by some propositions held in common describing how the objects behaved seems very intuitive to me, and probably anyone who has ever taken a discrete mathematics course. But it is exactly this intuition that gets in the way of understanding what occurs when we identify types as propositions.

    Here's the problem: to my mind, one of the reasons the distinction between sets of objects and descriptions of the object's properties remain separate is that classical mathematics, especially pure set theory, do not require that these objects have any describable properties at all! The axiom of choice in set theory guarantees that certain sets of objects exist, even when it's provable that descriptions of the objects are impossible. But for most of us, our intuition does not know how to deal with unknowable sets. The Banach-Tarski paradox is a good example - it's not a paradox in the sense that it leads to a contradiction, but that the result goes against our intuition about geometric figures. Most of us prefer to reason about objects with known or knowable properties. Dependent type theory gives us this - in fact, the guarantee is so strong, that the very distinction between objects and their properties is collapsed.

    In order to avoid much confusion, let me give some definitions and terms. I will henceforth talk about objects in type theory as constructions (in homage to constructive mathematics), and refer to sets and propositions as interpretations of these constructions, in order help the reader make the leap between set theory and type theory. When we consider type A as a proposition, we also say that the term a : A is a proof of A. There are additionally two special types. We define top, which is a trivially inhabited type. In contrast, the empty type (sometimes just empty, or absurd, bottom, or false) is the type that has no inhabitant, and proving that a proposition is false is done by showing that if we assume the proposition, we can derive an inhabitant of empty (i.e. a contradiction).

    One of my professors asked me, if types are supposed to represent propositions, what proposition does the type of natural numbers represent? Indeed, nothing much - the natural numbers are trivially inhabited by 0, making them no more informative as propositions as top (i.e. trivial truth) is. The natural numbers are much more naturally understood as constructions belonging to a set, or as the subjects of propositions. In order to fully realize constructions that are propositions, we need to use dependent types.

    Consider the following definition:

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc 

    This says, "Less-or-equal is a relation on natural numbers (a level zero type) that is created one of two ways - for two numbers m and n, we have m ≤ n either we have that m is 0, or m and n are successors to two numbers who are also less than or equal to each other. Given this definition, ≤ isn't merely inhabited or uninhabited - it isn't true or false - until you have two numbers m and n to consider. What makes, for example, the type 3 ≤ 5 a proposition is the restricted nature of how an element of such a type can be constructed.

example : 3 ≤ 5
example = s≤s (s≤s (s≤s (z≤n {2})))

    This example works by taking a base case, a proof that 0 is less than 2, and using it to construct inhabitants of 1 ≤ 3, 2 ≤ 4, and finally  3 ≤ 5. In general, types that are indexed over other types (like inequality of numbers) can serve as propositions when constructing elements of said type imposes some sort of restriction or structure on the indexed type.

    Consider another example, a definition describing "evenness" for natural numbers:

data Even : ℕ → Set where
  even-0 : Even 0
  even-s : ∀ {n} → Even n → Even (2 + n)

    This says, "there are two ways a number can be even - either it is 0 or it is 2 + another even number." If I get a construction of type Even n, I know that n has to have been made this way, and so I know that n is an even number. However, it gets much more interesting - what if I wanted to express the idea that, for every number n, double n is an even number (as I have defined Even above)? It should suffice to produce a rule, transforming any input n into a proof / inhabitant of Even (double n)

double : ℕ → ℕ
double n = n * 2

double-is-even : (n : ℕ) → Even (double n)
double-is-even 0 = even-0
double-is-even (suc n') with double-is-even n'
...                     | evn = even-s evn

 This says, "In the case that n is 0, we know that 0 is even; in the case that n is a successor of another number, say n', use recursion to show that double n' is even, and then adding two to double n' is the same as double (suc n'), so we have Even (double (suc n')). So, to express universal quantification over natural numbers, we need only to write a function that takes a natural number and return a construction of some type family whose index is that number (or an expression in which the number occurs).

    In fact, recognizing the correspondence between universal quantification and dependent function types, Agda has a nifty syntax for just this type of situation. For the type signature of double-is-even, we could have equivalently written:

double-is-even : ∀ n → Even (double n)

    Feel free to read this as "for all n, the double of n is even."

    Universal quantification seems straightforward enough - what about for the existential quantifier? In constructive mathematics, it does not suffice merely to show that a particular x exists, satisfying some proposition - we must produce the x satisfying the proposition itself. How might we do this? A particularly elegant solution is to use the dependent product type - a tuple whose first element is the x satisfying some proposition P, and whose second element is the proof that x satisfies P (with P itself as the type of this second (proof) construction).

    In order to see how this might be done, we should first take a closer look a P itself. Let us say P is a proposition about constructions of type A. Then, in Agda, we would say P : A → Set (confusing our terminology a bit, in Agda Set is the type of types, and in our case the type of propositions). So what we want from our tuple is, a first element x : A, and a second element p : P x (a proof of proposition P concerning x). In the Agda standard library, the sorts of tuples are defined as follows (modulo some book-keeping concerning universe levels, which I'll leave out for clarity):

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

     In this definition, proj₁ corresponds to x and proj₂ to our proof of P called p. So how do we use this definition to prove a "there exists" proposition? Let us return to our example of even numbers. We had shown that the double of every n is even, and now we shall show that every even number is the double of some number, i.e. that for every even number n there exists a number m such that n ≡ double m (the symbol ≡ represents equality). The proof is given below (the form Σ[_] is just special syntax for the above definition):

even-is-double : ∀ {n} → Even n → Σ[ m ∈ ℕ ] (n ≡ double m)
even-is-double even-0 = (0 , refl)
even-is-double (even-s evn) with even-is-double evn
...                        | (m' , refl) = (1 + m' , refl)

    The type signature says: "For all n, if n is an even number, then there exists an m such that n is equal to double m". The definitions says, "In the case that our even number is 0, we know that double 0 is 0, so we say the number satisfying the equation is 0, and the proof is reflexivity - 0 ≡ 0. If our even number is 2 + another even number (unnamed above, but we'll call it e'), find the number (m') that, when doubled, is our smaller even number e'. double (1 + m') is then equal to 2 + e', which is therefor equal to the even number given to us."

    A closing remark: some time ago someone on the Idris IRC channel complained that Agda should have had a built-in definition of existential types(1) like Idris does, because existentials are "fundamental." I could not disagree more. To me, one of the most beautiful results of dependent type theory is that the "primitive" (i.e. axiomatic) notions of predicate logic for universal and existential quantification can be reduced to even more general notions of dependent function and product types.


1: Idris can of course implement existentials as dependent products, the language just also provides a built-in version as well.