#PrayForKyoAni | Blog post: Five wonderful angels: A love letter to K-On | Help KyoAni recover

Why I love type theory

Posted on February 8, 2019

I'm interested in a field of math and computer science called type theory. I would like to share why I find type theory beautiful and fascinating.

Type theory as an alternative to set theory

Type theory was thought up by Bertrand Russell as an alternative to Georg Cantor's naive set theory. Russell had discovered a paradox, known as Russell's Paradox, that made set theory inconsistent. Russell's paradox, \(\{s \mid s \notin s\}\), describes the set of all sets that don't contain themselves; does this set contain itself? With type theory, Russell created a hierarchy of "universes" to prevent this paradox; a type cannot have itself as its own type.

Note that Zermelo-Fraenkel Set Theory does not have Russell's Paradox.

Bertrand Russell wasn't the only person who discovered this paradox; Cantor and Zermelo did so as well.

Further reading: Types as Sets in the Elm programming language's documentation

Types and terms

Alonzo Church invented the lambda calculus with the intention of doing logic with it. His first iteration, the untyped lambda calculus, is the one that most often comes to mind when we think of the lambda calculus. The syntax of the untyped lambda calculus consists of:

\[ \begin{align} term ::= \: & \lambda x . term && \textbf{Lambda abstraction} \\ & term~term && \textbf{Function application} \\ & x, y, z && \textbf{Variable} \\ \end{align} \]

The lambda calculus is a term rewriting system with reduction rules. A lambda calculus program that cannot be reduced further is called a normal form. The evaluation of a lambda calculus program is called normalization.

However, the not all programs in the untyped lambda calculus have a normal form. For some programs, one can keep rewriting them forever and never reach a normal form. Such programs are nonterminating. Alonzo Church had hoped to use the illative lambda calculus, or lambda calculus with mathematical expressions, to do logic, but logician Haskell Curry devised a paradox, Curry' paradox, that showed that the logic in this system was inconsistent due to nonterminating recursion. Consequently, Alonzo Church devised the simply typed lambda calculus:

\[ \begin{align} \tau ::= \: & \tau \to \tau && \textbf{Function type} \\ & A, B, C && \textbf{Base type} \\ \\ term ::= \: & \lambda x : \tau . term && \textbf{Lambda abstraction} \\ & term~term && \textbf{Function application} \\ & x, y, z && \textbf{Variable} \\ \end{align} \]

Types classify terms; terms are said to have a type. The rules of the type system restrict what programs may be expressed as a way of ensuring program correctness.

The type system of the simply typed lambda calculus rejects nonterminating programs. The simply typed lambda calculus is strongly normalizing, meaning that every program has a normal form.

There are many other lambda calculi with different type systems. Examples are System F, System F\(_\omega\), and the Calculus of Constructions. These lambda calculi have varying expressive power due to the ability to write functions from types to terms (the parametric polymorphism of System F), types to types (the higher-kinded types of System F\(_\omega\)), or even terms to types (dependent types). These lambda calculi are classified according to the "lambda cube."

Further reading: The Lambda Calculus on the Stanford Encyclopedia of Philosophy

The algebra of types

The terms of a type are called the type's inhabitants. Types are algebraic and their names indicate how many terms they have:

Let's do an example. \(Bool\) has \(2\) inhabitants, \(True\) and \(False\). \(Bool \times Bool\) has \(4\), or \(2 \times 2\) inhabitants:

Let the sum \(A + B\) either be \(Left\:A\) or \(Right\:B\).

The sum of \(Bool\) and \(Bool\) also has \(4\) inhabitants, because \(2 + 2 = 4\).

We then say that \(Bool \times Bool\) and \(Bool + Bool\) are isomorphic. We can write inverse functions between them:

\[ \begin{align} & f : Bool \times Bool \to Bool + Bool\\ & f (True, True) = Left~True\\ & f (True, False) = Left~False\\ & f (False, True) = Right~True\\ & f (False, False) = Right~False\\ \\ & f^{-1} : Bool + Bool \to Bool \times Bool\\ & f^{-1} (Left~True) = (True, True)\\ & f^{-1} (Left~False) = (True, False)\\ & f^{-1} (Right~True) = (False, True)\\ & f^{-1} (Right~False) = (False, False) \end{align} \]

Further reading: The algebra (and calculus!) of algebraic data types by Joel Burget

The algebra of dependent types

The connection goes further. With dependent types, we can mix types and terms. Thus, we introduce the dependent product and dependent sum types.

Confusingly, the dependent product type is a generalization of the exponential, or function type, and the dependent sum type is a generalization of the product type. However, the reason why will soon become crystal clear.

The dependent sum type is written as:

The dependent product type is written as:

\(B\) is actually a function of \(x\); it is said to depend on \(x\).

An exponential or function type is really a dependent product type where \(B\) is a constant function independent of \(A\). A (non-dependent) product or pair type is really a dependent sum type where \(B\) is a constant function as well.

When we use numbers, sigma notation expresses summation: \[ \sum \nolimits_{x : 1}^n f(x) \]

The same goes for pi notation for multiplication: \[ \prod \nolimits_{x : 1}^n f(x) \]

When \(f(x)\) is a constant \(c\) independent of \(x\), \(\sum \nolimits_{x : 1}^n c = n \times c\) and \(\prod \nolimits_{x : 1}^n c = c^n\). After all, multiplication is just repeated addition and exponentation is just repeated multiplication! This reason is the exact same reason why the depedent sum type is a generalization of the product type and the dependent product type is a generalization of the sum type.

What happens when \(B\) isn't a constant function? Let's look at an example:

\[ \begin{align} & f : Bool \to Type \\ & f~True = Unit \\ & f~False = Bool \\ \end{align} \]

\[ \begin{align} & typ : Type \\ & typ = \sum \nolimits_{b : Bool} f(b) \\ \\ & (True, ()) : typ \\ & (False, True) : typ \\ & (False, False) : typ \end{align} \]

So, \(typ = f(True) + f(False) = Unit + Bool\). The types are isomorphic; both have \(3\) inhabitants.

Further reading: Andrej Bauer's answer to "Why is product type a dependent SUM?"

Types as propositions, terms as proofs

According to what's known as the Curry-Howard correspondence, one can interpret types and terms as logical propositions and proofs, respectively. By inhabiting a type, one proves the corresponding proposition. This correspondence is named after Haskell Curry and William Alvin Howard.

\[ \begin{align} & \textbf{Proposition} && \textbf{Type} \\ & True && Unit \\ & False && Bottom \\ & A \lor B && A + B \\ & A \land B && A \times B \\ & A \implies B && A \to B \\ & \exists x:A \ldotp B(x) && \sum \nolimits_{x : A} B(x) \\ & \forall x:A \ldotp B(x) && \prod \nolimits_{x : A} B(x) \end{align} \]

The proof of \(True\) is trivial: \(()\). \(False\) has no proof. To prove $A \lor $, one must either inhabit \(A\) or \(B\). To prove \(A \land B\), one must inhabit both \(A\) and \(B\). To prove \(A \implies B\), one must inhabit \(B\) given an inhabitant of \(A\). To inhabit \(\exists x : A \ldotp B(x)\), one must inhabit both \(A\) and \(B(x)\), where \(B(x)\) is a proposition about \(x\), the inhabitant of \(A\). To inhabit \(\forall x : A \ldotp B(x)\), one must show that \(B(x)\) holds, or is inhabited, for every inhabitant \(x\) of \(A\) that exists.

Proofs must have a normal form; type systems that accept diverging programs are inconsistent as a logic. Recursion introduces nontermination into a programming language, but induction is important for many proofs. Therefore, the typechecker needs to make sure that inductive functions are total: They cover all inputs and never diverge. As the halting problem is undecidable, the termination checker must reject some valid programs.

Proofs expressed with types and terms are also algorithms. They embody the notion of a computation and describe how to construct a mathematical object. I think it's exciting that computer science, or the science of computation, has a place in the foundations of math.

Types as objects, terms as morphisms

Not only are types propositions and terms morphisms, the simply typed lambda calculus together with products is the "internal language" of a Cartesian closed category. The three-way correspondence between type theory, logic, and category theory is called the Curry-Howard-Lambek correspondence or computational trinitarianism.

What is a category? A category consists of a collection of objects and a collection of morphisms, also called arrows or maps, between these objects.

The set of morphisms from \(A\) to \(B\) is written \(Hom(A, B)\).

A Cartesian closed category is a category with a "terminal object," denoted \(1\), and for objects \(A\) and \(B\), a product object \(A \times B\) and an exponential object \(A^B\). A terminal object is an object that for each object \(A\), there exists exactly one arrow \(A \to 1\). A Cartesian closed category has these properties:

I'm not knowledgable on category theory, so I may have gotten some things wrong with the Lambek correspondence.

Further reading: Computational Trinitarinism on the nLab

Practical importance of type theory

Not only is type theory theoretically beautiful, it has practical use as well. Types, type systems, and typing judgements are the means of specifying a programming language's static semantics, making statements about a program's behavior at compile time. More compile-time errors mean less runtime errors. While tests only check that a program works on certain inputs, compile-time verification of its properties makes guarantees that it can't go wrong in certain ways.

Although typechecking will always reject valid programs, types aren't here to inconvenience you. Done right, a type system helps programmer productivity by allowing programmers to better specify a program's valid states and expected behavior. Types serve as formal documentation of APIs.

Mathematicians have used dependent types for real work. For example, the Coq proof assistant was used to prove the Four-Color Theorem.

Conclusion

A type truly is a fascinating thing. Is it similar to a set? Is it a proposition? An object? A description of a computation's behavior? Type theory has profound and beautiful connections to many fundamental fields of math.

The ideas that I have described are not the full extent of type theory. There are many other research topics, including but not limited to equality and homotopy type theory, codata types, session types, substructural logic, and module systems. With such a wide wealth of ideas, I am confident that I will never run out of new things to learn about type theory.

Last updated: September 8, 2019, with corrections


Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.