Types and Logical Connectives

We are now getting to a really interesting part of the PLFA: the intimate connection between the logical connectives and types.

For the longest time, I saw logic as having a very peculiar relationship with mathematics, functioning as preamble of sorts to it, but not really being a part of it. Logic, after all, is concerned with the truth of propositions, but propositions are, at least on the face of it, not mathematical objects, right? In fact, truth itself is the subject of philosophy, not mathematics proper… Or so I thought. Now, admittedly, over the last century we’ve been able to mathematize (if that’s even a word) logic to some extent, but there was still a sense in which logic allowed us to think about math, but the two were still not on the same plane. Further, it’s not at all obvious that the logical connectives (and, or, if-else, etc.) are equivalent to other mathematical objects, like functions, sets, spaces, etc. It turns out, however, that the connectives, quantifiers, even truth and falsehood, are isomorphic to certain mathematical objects. And, therefore, logic is not so peculiar after all!

This new perspective, called Propositions as types, is akin to the introduction of the Cartesian plane, which allowed geometry and algebra, two math subjects long considered to be about very different things, to become two ways of talking about the same thing. So logic is no longer the strange preamble to mathematics, but is completely located within it.

Product (conjunction)

We’ve dealt with two record types so far: isomorphisms, which have 4 fields, or whose terms are a 4-tuple, and embeddings, which have 3 fields or terms consisting of a triple. We now introduce the Cartesian product type, whose terms consist of pairs, i.e., 2 fields:

record _×_ (A B : Set) : Set where
  constructor ⟨_,_⟩
  field
    proj₁ : A
    proj₂ : B

The definition is as before, with the two projections giving us, each, the components of the pair.¹

One slight difference this time is the appearance of the constructor \(\langle\_,\_\rangle\). If the projections decompose a term of a record type into its components, the constructor re-assembles them back into the full term. For this reason, the projections (the eliminators of the record type) are also called “destructors”.

So, for example, we’ve been defining the terms of a record-type in the following way:²

some-term =
   record
      { fst = foo
      ; snd = bar
      }

With the addition of the constructor \(\langle\_,\_\rangle\), we can express that more compactly as:

some-term = ⟨ foo , bar ⟩

Whereas in the previous notation the projections (the destructors) gave us the individual components of the term, here the constructor \(\langle\_,\_\rangle\) has gathered the components and reassembled the term.

Getting back to logic, let’s say we have the product type \(A\times B\). A term or proof of it is a pair \(\langle a, b\rangle\), where \(a\) is a term or proof of \(A\), and \(b\) is a term or proof of \(B\). Now let’s think about this: if we need both \(a\) and \(b\) to prove \(A\times B\), this corresponds exactly to the logic rule that says \(A \land B\) is true when both \(A\) and \(B\) are true! Therefore, product is conjunction!

eta-equality

Suppose \(w\) is a term or proof of the type \(A\times B\). This means that the proof of \(A\) is obtained by applying the first projection/destructor, \(\mathtt{fst}\), to \(w\), and the proof of \(B\) is obtained by applying the second projection/destructor, \(\mathtt{snd}\), to \(w\). If we then take these two components and apply the constructor \(\langle\_,\_\rangle\) to them, we should get back the original term \(w\), right? This decomposing and re-composing has a name: eta-equality (also eta-expansion):

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× w = refl

Here \(\eta\text{-}\!\times\) is the function that allows us to prove eta equality. It takes a term \(w\) of type \(A\times B\) and returns a proof of the following equality type:

\[ \langle proj_1 (w) , proj_2 (w) \rangle \equiv w \]

Since the left-hand side is definitionally reducible to \(w\), giving us the type \(w \equiv w\), this means that the proof \(\eta\text{-}\!\times\) is the same as \(\mathtt{refl}\).

As data type

We can define the product type as a data type instead of a record type:

data _×′_ (A B : Set) : Set where
  ⟨_,_⟩′ : A → B → A ×′ B

proj₁′ : ∀ {A B : Set} → A ×′ B → A
proj₁′ ⟨ x , y ⟩′ = x

proj₂′ : ∀ {A B : Set} → A ×′ B → B
proj₂′ ⟨ x , y ⟩′ = y

However, not only is this more verbose, but the eta equality rule no longer holds by definition:

η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ ⟨ x , y ⟩′ = refl

You’ll note that we can no longer just provide a variable term \(w\) as argument for \(\eta\text{-}\!\times'\). Instead, we have to provide a term constructed with \(\langle\_,\_\rangle\). This allows Agda to reduce both sides of the equality symbol to the same term by substitution:

\[\begin{align*} \eta\text{-}\!\times' &: (w: A \times' B) \to \langle proj_1' w, proj_2' w \rangle' \equiv w\\ \eta\text{-}\!\times' \langle x, y \rangle' &: \big\langle proj_1' \langle x, y \rangle', proj_2' \langle x, y \rangle' \big\rangle' \equiv \langle x, y \rangle'\\ \eta\text{-}\!\times' \langle x, y \rangle' &: \langle x, y \rangle' \equiv \langle x, y \rangle'\\ \eta\text{-}\!\times' \langle x, y \rangle' &= \mathtt{refl} \end{align*}\]

Properties: commutativity and associativity

Cartesian products are commutative up to isomorphism, meaning that, in general, \(A\times B\) is isomorphic to \(B\times A\) but not equal to it. We’ve seen how addition on the natural numbers is commutative,³ and in that case the commutativity was up to equality. In other words, \(2 + 3\) is the same as \(3 + 2\). Product types are very close to this. Thus, taking an example from the PLFA, the type \(\mathtt{Bool \times Tri}\) is isomorphic (but not identical) to \(\mathtt{Tri \times Bool}\). The proof of commutativity is as follows:

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { to       =  λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; from     =  λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; from∘to  =  λ{ w → refl }
    ; to∘from  =  λ{ w → refl }
    }

The term or proof of commutativity up to isomorphism is, as expected, an isomorphism consisting of four components. In pseudo-code:

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { fst  (×-comm)  = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; snd  (×-comm)  = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; thrd (×-comm)  = λ{ w → refl }
    ; fth  (×-comm)  = λ{ w → refl }
    }

Associativity up to isomorphism means that the type \((A\times B) \times C\) is isomorphic (but not equal) to \(A\times (B \times C)\). This is proven by the isomorphism \(\times\text{-}\mathtt{assoc}\) whose four components are:

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
  record
    { to      = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
    ; from    = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
    ; from∘to = λ{ w → refl }
    ; to∘from = λ{ w → refl }
    }

Or, following my own convention:

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
  record
    { fst  (×-assoc) = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
    ; snd  (×-assoc) = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
    ; thrd (×-assoc) = λ{ w → refl }
    ; frth (×-assoc) = λ{ w → refl }
    }

Refer to the previous entry on isomorphisms for how to interpret the four components.

Unit (truth)

We’ve gone from record-type terms with 4 components (isomorphisms), 3 components (embeddings), and 2 components (the pairs of the product). We now introduce a record type whose only term has no factors, i.e., no components. What does this mean? In general, a type-as-proposition is considered true (to hold or be inhabited) only if we can construct at least one term of it. There is a type, however, that is always true (or is always inhabited), namely, the unit type \(\top\).⁴ You probably recognize the symbol \(\top\) as being the symbol for truth. This is another bridge between type theory and logic!

Unit has a peculiar declaration in Agda:

record ⊤ : Set where
  constructor tt

Since a term of \(\top\) has no factors, it makes little sense to include a record block below the constructor. By the same token, the constructor \(\mathtt{tt}\) takes no arguments: it’s a constant.

Remember that applying the constructor to the destructors is the eta-equality rule? Strangely, it appears in this record type too! Even though there are no destructors or projections… Don’t believe me? Just look!

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ w = refl

The function \(\eta\text{-}\!\top\) takes a term \(w\) of the type \(\top\) and returns proof of the equality type \(\mathtt{tt}\equiv w\). But since there is only one term in \(\top\) by definition, Agda smartly deduces that \(w\) is that unique term \(\mathtt{tt}\). Therefore, the proof \(\eta\text{-}\!\top\ w\) is the same as \(\mathtt{refl}: \mathtt{tt \equiv tt}\).

Now, I know what you’re thinking. If the unique term \(\mathtt{tt}\) has no components, then why is the type \(\top\) a record type? Answer: 🤷‍♂️.

In fact, it can also be declared as a regular data type:

data ⊤′ : Set where
  tt′ : ⊤′

The only difference, according to the PLFA, is that if we declare \(\top\) as a data type, the eta-equality rule does not hold by definition:

η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
η-⊤′ tt′ = refl

The variant \(\eta\text{-}\!\top'\) takes a term \(w\) of \(\top'\) and returns proof of the equality type \(\mathtt{tt}' \equiv w\). However, the term provided must be constructed by \(\mathtt{tt}'\) so that Agda can make the proper substitution:

\[\begin{align*} \eta\text{-}\!\top' &: \forall\ (w : \top') \to \mathtt{tt}' \equiv w\\ \eta\text{-}\!\top'\ \mathtt{tt}' &: \mathtt{tt}' \equiv \mathtt{tt}'\\ \eta\text{-}\!\top'\ \mathtt{tt}' &= \mathtt{refl} \end{align*}\]

Sum / Coproduct (disjunction)

The sum or coproduct type is defined as a regular data type:

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

Here \(\_\uplus\_\) is the type former: it takes two types \(A\) and \(B\) and forms the sum or coproduct type \(A\uplus B\). Then \(A \uplus B\) has two (term) constructors, \(inj_1\) and \(inj_2\), meaning that either of them can provide a term or proof of \(A \uplus B\). This makes it equivalent to the logical disjunction \(A\lor B\), which holds whenever \(A\) or \(B\) is true, and is false when both \(A\) and \(B\) are false. So, if we have \(a: A\), then proof of \(A\uplus B\) is of the form \(inj_1\ a\). Or if we only have \(b: B\), the proof of \(A\uplus B\) is of the form \(inj_2\ b\). If both \(A\) and \(B\) are empty types, then neither constructor can provide a term or proof of \(A\uplus B\), meaning that the type-as-proposition is false.

The names for the constructors, \(inj_1\) and \(inj_2\), suggest that they are a sort of reverse projection/eliminator. That is, whereas in a product type the projection has type \(A\times B \to A\) (or \(A\times B \to B\)), in a coproduct type the “injection” has type \(A \to A\uplus B\) (or \(B \to A \uplus B\)).

eliminators?

The eliminators or destructors of the sum/coprodut type require a bit more explanation than those of the product type. (Hat tip to EuclideanSpace for helping me make sense of why the coproduct eliminator is different from the product eliminator.) In the product, if we have a term \(w: A\times B\), we immediately have terms/proofs of both \(A\) and \(B\) (by definition), and the projections (the eliminators) can provide them. Thus \(proj_1: A\times B \to A\) gives proof of \(A\), and \(proj_2: A\times B \to B\) gives proof of \(B\).

However, suppose we have a term \(p: A\uplus B\), can we readily expect a proof of \(A\)? No, because the term \(p\) could have been constructed with a term of \(B\), i.e., with the constructor \(inj_2\). For the same reason, from having only \(p: A\uplus B\), we cannot expect an immediate proof of \(B\), because \(p\) could have been constructed with a term of \(A\), i.e., with \(inj_1\).

So, what to do? Another way to think of an eliminator is as a function that helps us use a term of a new type in order to get a term of another type (see the nLab’s entry on elimination rules). So instead of an eliminator that gets us a term of \(A\) or \(B\) on the basis of \(A\uplus B\), we define one, call it \([f,g]\) (the name will make sense in a bit), that gets us a term of some other type \(C\) on the basis of \(A\uplus B\). In short, its type is \([f,g]: A\uplus B \to C\). Since a term of \(A\uplus B\) has two ways of being constructed, \([f,g]\) will also get us a term of \(C\) in one of two ways:

\[\begin{align*} [f,g](inj_1\ a) &: C\\ [f,g](inj_2\ b) &: C \end{align*}\]

Lastly, we define each of these possible terms on the basis of two other constructors for \(C\), namely: \(f: A \to C\) and \(g: B \to C\). That is:

\[\begin{align*} [f,g](inj_1\ a) &= f(a)\\ [f,g](inj_2\ b) &= g(b) \end{align*}\]

The way I like to think about the coproduct destructor is that it comes equipped with “knowledge” of \(f\) and \(g\) before taking a term of the coproduct. The PLFA “packages” all the above into a function they call \(\mathtt{case}\text{-}\!\uplus\):⁵

case-⊎ : ∀ {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ y) = g y

But now look: this resembles a rule in propositional logic called disjunction elimination:

Meaning that, if \(A\) implies \(C\) and \(B\) implies \(C\), then, if we have proof of either \(A\) or \(B\) (i.e., \(A\lor B\)), then we can conclude \(C\). This can be translated into the language of type theory:

If we have a term or proof of \(A\to C\) (that is, a function that, given a proof of \(A\), constructs a proof of \(C\)), a term or proof of \(B\to C\), and a term or proof \(A\uplus B\), then type \(C\) holds (is inhabited).

If you’ve studied some category theory, you’ll realize that all of the above can be represented in this neat categorial diagram:

eta equality

Like with products, coproducts also have eta equality, which, again, is the rule that says that applying the destructor to each of the two constructors gives us back the original term. Using my preferred notation, this means that if the destructor comes with knowledge of \(inj_1\) and \(inj_2\), i.e., \([inj_1,inj_2]\), then when it takes a term of the coproduct, it returns back that term as if it did nothing to it. In the PLFA’s notation:

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

Because coproducts are not record types, we have to provide \(\eta\text{-}\uplus\) with a term as constructed with \(inj_1\) or \(inj_2\). When we do this, Agda will perform the appropriate substitutions. Using my notation:

\[\begin{align*} \eta\text{-}\uplus &: (w: A \uplus B) \to [inj_1, inj_2]\ w \equiv w\\ \eta\text{-}\uplus (inj_1\ x) &: [inj_1, inj_2] (inj_1\ x) \equiv inj_1\ x\\ \eta\text{-}\uplus (inj_2\ y) &: [inj_1, inj_2] (inj_2\ y) \equiv inj_2\ y \end{align*}\]

If the left-hand side of the equality can be reduced to the right-hand side, then we can simply define the term as being \(\mathtt{refl}\). But this is easy: we’ve just said that \([f, g](inj_1\ x)\) is the same as \(f(x)\), so, after substitution, we have that \([inj_1, inj_2] (inj_1\ x)\) is the same as \(inj_1\ x\), and the guaranteed term of \(inj_1\ x \equiv inj_1\ x\) is \(\mathtt{refl}\). Same goes for the second case.