module Types.introduction where
open import Lang.dataStructures using (List; []; _::_; ℕ; one; three; seven; nine)Type Theory can be thought of as the programming language used to implement math. Instead of the more familiar method of writing symbols on a piece of paper, we represent those symbols as code, which a compiler can then parse and type-check, thus guaranteeing the code’s (and hence the represented math’s) correctness. Though to programmers this might seem very natural, it is an extremely powerful method for doing math as the burden of verification becomes automated − thus significantly reducing testing time.
Most of mathematics, as we know it, is based on the foundations of Set Theory. In order to realize our goal of implementing math in Type Theory with some real convenience, the foundations need to be shaken up a bit, and reformulated from the ground-up.
Set Theory is a mathematical theory which studies collections of objects, called sets. These objects,
called members or elements of the set, can literally be anything. The other main component of
Set Theory is first-order logic, which is used to construct and reason around sets. The language of Set Theory can be
used to define almost all of mathematical objects.
Set Theory has existed for centuries, has underdone several alterations, revisions (rewrites) as well as paradox removal (bug fixes, if you will). In fact, theories in mathematics follow similar lifecycles as seen in the programming world (or vice versa to be exact) leading to various flavors / versions / “forks” of the theory. The best-known amongst them is Zermelo-Fraenkel set theory (ZFC).
Zermelo-Fraenkel Set theory (ZFC) consists of:
Sets which are a collection of objects.The basic relation of set theory is that of membership: ∈, i.e. a statement such as
a ∈ Set A which implies a is an element of the set A.
Two sets A and B are equal if ∀ x, x ∈ A iff x ∈ B, read as: for all
x, x is an element of A if and only if x is also an element of
B.
A is a subset of B if every element of A is an element of B,
denoted as A ⊆ B.
Given sets A and B, one can perform some basic operations with them yielding the following
sets:
The set A∪B, called the union of A and B, whose elements are the elements
of A and the elements of B.
The set A∩B, called the intersection of A and B, whose elements are the
elements common to A and B.
The set A−B, called the difference of A and B, whose elements are those
elements of A that are not members of B.
A∪(B∪C)=(A∪B)∪CA∩(B∩C)=(A∩B)∩CA∪B=B∪AA∩B=B∩AA∪(B∩C)=(A∪B)∩(A∪C)A∩(B∪C)=(A∩B)∪(A∩C)A∪A=AA∩A=AA∪∅=AA∩∅=∅A−A=∅ZFC comprises of a bunch of axioms, which we are not going to look into here. The interested reader may explore them on Zermelo–Fraenkel set theory: Wikipedia or nlab.
Type theory is a formal system of symbolic logic where every term has a “type”. “Term” here refers to mathematical
terms such as variable x, function f, operation ★ and so on. Bertrand Russell was
the first to propose this theory in order to fix Russell’s Paradox which plagued naive set theory, though Per Martin-Löf
was the one to come up with a more practically useful version of it, called “Intuitionistic Type Theory”.
A type system in programming languages typically specifies data and appears like a tree of objects, where each
successive level tries to represent data more specifically. E.g., A Float is a subtype of
Number and is a more specialized case of a Number.
In a system of type theory, each term has a type. For example, 4, 2+2 and
2 * 2 are all separate terms with the type ℕ for natural numbers. This is indicated as \(2 : ℕ\) or 2 is of type natural number.
Type theories have explicit computation and it is encoded in rules for rewriting terms. These are called “conversion
rules” or, if the rule only works in one direction, a “reduction rule”. For example, 2+2 and 4
are syntactically different terms, but the former reduces to the latter. This reduction is written
2+2 ↠ 4.
Functions in type theory have a special reduction rule: the argument to the function is substituted for every
instance of the parameter in the function definition. Let’s say the function double is defined as
double(x) = x + x or mathematically \(double: x ↦ x + x\). Then, the
function call double 2 would be reduced by substituting 2 for every x in the
function definition. Thus, double 2 ↠ 2+2.
Logic itself is subsumed in the plain idea of operations on terms of types, by observing that any type X may be thought of as the type of terms satisfying some proposition. In fact, propositions are types and thus finding a proof of the proposition is equivalent to constructing a term of the proposition type. We discuss about this in Proofs as Data.
Since such a proof is constructive, the term witnessing it being a concrete implementation, and since type theory strictly works by rewriting rules, one may identify the construction of a term in type theory as a program whose output is a certain type. Under this “proofs as programs”-paradigm, type theory is a mathematical formalization of a programming language.
(Ignore if the reader is not familiar with category theory) If we consider any term t:X to exist in a
context Γ of other terms x:Γ, then t is naturally identified with a “map”
t:Γ→X, hence: with a morphism. Viewed this way the types and terms of type theory are identified,
respectively, with the objects and morphisms of category theory. From this perspective, type theory provides a formal
language for speaking about categories.