Computational Type Theory

A lecture series given by Bob Harper at OPLSS 2018

Part One

Type theory from a computational perspective

References

Martin-Löf, Constructive Mathematics and Computer Programming
Constable et al., NuPRL System & Semantics

The plan is to develop type theory starting with computation, and developing a theory of truth based on proofs. The connection with formalisms (e.g. theories of proofs, formal derivation, etc.) comes later.

The idea is to emphasize not just playing the Coq/Agda/Lean video game!

Start with a programming language

The language has a deterministic semantics via a transition system.

We have forms of expression called

$E$

and two judgement forms called

$E v a l$

$E \mapsto E^{'}$

These mean that $E$ is fully evaluated, and that we have performed one simplification of $E$ , respectively.

We have a derived notion

$E ⇓ E_{\circ}$

which we can understand by way of a mapping

$E \mapsto^{⋆} E_{\circ} v a l$

As an example expression

$i f (E_{1}; E_{2}) (E)$

Operational semantics for binary decision diagrams

$\frac{E ⟼ E ^{'}}{i f ( E _{1} ; E _{2} ) ( E ) ⟼ i f ( E _{1} ; E _{2} ) ( E ^{'} )}$

$i f ( E _{1} ; E _{2} ) ( t r u e ) ⟼ E _{1}$

$i f ( E _{1} ; E _{2} ) ( f a l se ) ⟼ E _{2}$

Principle: types are specifications of program behavior

Judgements are expressions of knowledge, in the intuitionistic sense (Brouwer), based on the premise that mathematics is a human activity, thus finite, and that the only way to constrain facts about infinite infinities (Gödel, Russell?) is via algorithms.

E.g. there is no way to convey infinitely many utterly disconnected facts about $N a t$ other than to have a uniformity expressed as an algorithm. We agree on such uniformity solely because of the fundamental faculties of the human mind w.r.t. computation.

$M$ and $A$ here are programs, and are behavioral, not structural. ${A t y p e M \in A$

For example:

$i f (17;_) (t r u e) \in N a t$

Why? Because the simplification step entails $17 \in N a t$ .

Further:

$i f (N a t; B oo l) (M)$

is a type precisely when:

$M \in B oo l$

This applies to type expressions as well, e.g.

$i f (17; t r u e) (M) \in i f (N a t; B oo l) (M)$

This helps explain why a deterministic operational semantics is required, because it is the same $M$ in the simplification step. Types/specifications are programs.

Type-indexed families of types a.k.a. dependent types

We can make a judgement that:

$se q (n) t y p e$

precisely when

$n \in N a t$

And that:

$n : N a t ≫ se q t y p e$

That is, a family of types is indexed by a type. Another way to phrase it, which emphasizes the indexing of a sequence by $n \in N a t$ is:

$\forall n \exists se q (n)$

where:

$se q (n) ≐ [0.. n - 1]$

In NuPRL notation:

$f \in n : N a t \to S e q (n)$

This is sometimes represented in the literature as:

$Π n : N a t S e q (n)$

Functionality

Families (of types, of elements) must respect equality of indices. So what is equality?

Trivially:

$se q (2 + 2)$

is "the same as"

$se q (4)$

or in other words

$se q (i f (17; 18) (M))$

is "the same as"

$i f (se q (17); se q (18)) (M)$

which can be clarified with a slight change in notation, substituting $a : B oo l$ for $M$

As a type structure gets richer, when two things are equal is a property of the type they inhabit, and it can be arbitrarily complicated. The situation about what is true has a much higher -- in fact -- unbounded quantifier of complexity, whereas the question of what is written down in any formalism is always relentlessly recursively enumerable. This means that formalisms can never approach equality-based truth! This standpoint is validated by Gödel's theorem.

Indeed, the entire endeavour of higher-dimensional type theory arises from investigating when two types are the same.

Judgements

When $A$ is a type:

$A ≐ A^{'}$

specifies an exact equality of types.

When $M \in A$ :

$M ≐ M^{'} \in A$

specifies an exact equality of elements.

Thus, equal indices deterministically produce equal results (this is also why a deterministic operational semantics is a necessity). A term for this is equisatisfaction.

A simple example is the following:

$2 ≐ 4 \in N a t$

cannot be true...

However:

$2 ≐ 4 \in N a t /2 (e v e n s)$

is true!. It always depends on type inhabitants.

This is in contrast to the older tradition in formalized type theory of axioms as being somehow type-independent. By the principle of propositions-as-types, we now know this is is a logical fallacy.

To make the notation a little clearer, from here on we will try to write:

$M ≐ M^{'} \in A$

as:

$M ≐_{A} M^{'}$

A computational semantics

$A ≐ A^{'}$

means that

$A ≐ A^{'} ⎩ ⎨ ⎧ A ⇓ A_{\circ} A^{'} ⇓ A_{\circ}^{'} A_{\circ} ≐_{\circ} A_{\circ}^{'}$

$A_{\circ}$ and $A_{\circ}^{'}$ are equal type-values, or what Martin-Löf called canonical types.

$M ≐_{A} M^{'}$ is thus a program which evaluates to equal type-values.

A few core ideas

Given that

$A ⇓ A_{\circ} A_{\circ} ≐_{\circ} A_{\circ}$

we can say

$⎩ ⎨ ⎧ M ⇓ M_{\circ} M^{'} ⇓ M_{\circ}^{'} M_{\circ} ≐_{\circ} M_{\circ}^{'} \in A_{\circ}$

Thus

$a : A ≫ B ≐ B^{'}$

means

$i f (M ≐ M^{'} \in A) t h e n (B [M / a] ≐ B^{'} [M^{'} / a])$

This induces a certain implication about type indexing, called functionality:

Check that $⎩ ⎨ ⎧ a : A ≫ B where B M^{'} implies B [M / a] ≐ B ≐ M^{'} \in A ≐ B [M^{'} / a]$

A final example in the general case:

$a : A ≫ N ≐ N^{'}$

means

$i f M ≐ M^{'} \in A t h e n (N [M / a] ≐ N^{'} [M^{'} a] \in B [M / a])$

assuming

$a ≫ B ≐ B$

A specific example by deriving the Boolean type

$B oo l ≐_{\circ} B oo l$

i.e. $B oo l$ names a type-value (hence the $_\circ$ ).

What type does it name? The membership relation for canonical elements is

$M_{\circ} ≐ M_{\circ}^{'} \in_{\circ} B oo l$ is the strongest relation $R$ (though some literature calls this least, the extremal nature is what is important)

such that

$R \subseteq (E x p \times E x p) {(t r u e ≐_{\circ} t r u e \in B oo l) i . e . t r u e \in_{\circ} B oo l (f a l se ≐_{\circ} f a l se \in B oo l) i . e . f a l se \in_{\circ} B oo l$

The extremal clause is that

The stated conditions hold.
Nothing else!

We can now make proposition/fact/claim, and prove it. We'll use this format from here onward.

Fact

$M \in B oo l$

and

$A t y p e$

and

$M_{1} \in A$

and

$M_{2} \in A$

then

$i f (M_{1}; M_{2}) (M) \in A$

Proof

$_\in B oo l$ is given by a universal property, the least (or most) containing ${t r u e \in B oo l f a l se \in B oo l$
Fix some type $A$ , $M_{1} \in A$ , $M_{2} \in A$ .
If $M \in B oo l$ then $i f (M_{1}; M_{2}) (M) \in A$
Thus, $M \in B oo l$ means $M ⇓ M_{\circ}$ and either ${M_{0} M_{0} ≐ t r u e ≐ f a l se$
It suffices to show that ${i f (M_{1}; M_{2}) (t r u e) \in A i f (M_{1}; M_{2}) (f a l se) \in A$
$i f$ evaluates its principal arguments (via a transition step). Typing is closed under "head-expansion" or alternatively "reverse execution".
$■$

Part Two

Lecture 2

Where we are so far

A type system consists of $A ≐ A$ with $A$ called a $t y p e$ $i ff$ $A ≐ A$ .

$M ≐ M$ with $M \in A$ $i ff$ $M ≐ M \in A$ .

The expression above is both symmetric and transitive, that is

If $A ≐ A^{'}$ and $M ≐ M^{'} \in A$ then $M ≐ M^{'} \in A$

Hypotheticals express functionality:

$a : A ≫ B t y p e$

This means $B$ is a family of types that depends functionally on $a : A$ .

$M ≐ M^{'} \in A$

implies

$B [M / a] ≐ B [M^{'} / a]$

$a : A ≫ N \in B$

means that $B$ is a family of elements; A family of elements is a mapping.

The expression

$M ≐ M^{'} \in A$

implies

$N [M / a] ≐ N [M^{'} / a] \in B [M / a] ≐ B [M^{'} / a]$

Similarly for $B ≐ B^{'}$ , $N ≐ N^{'} \in B$

All of the above constitutes a type system defined in terms of evaluation (hence computational) using the language of constructive mathematics.

Now we can start to write down fragments of our own type theories.

There exists a type system containing a type `bool`

Presuming

$B oo l ≐ B oo l$

The expression

$M ≐ M^{'} \in B oo l$

is true $i ff$ either

$(M ^{'} ⇓ t r u e M ⇓ t r u e)$

$(M ^{'} ⇓ f a l se M ⇓ f a l se)$

Fact

$a : B oo l ≫ B t y p e$

and

$M_{1} \in B [t r u e / a]$

and

$M_{2} \in B [f a l se / a]$

and

$M \in B oo l$

then

$i f (M_{1}; M_{2}) (M) \in B [M / a]$

Proof

Either $M ⇓ t r u e$
- $∴ M ≐ t r u e \in B oo l$ by head expansion (reverse execution)
or $M ⇓ f a l se$
- $∴ M ≐ f a l se \in B oo l$ by head expansion (reverse execution)
$■$

An example

Given $M_{1} \in B [t r u e / a]$

$i f (M_{1}; M_{2}) (M) ≐ i f (M_{1}; M_{2}) (t r u e) ≐ M_{1} \in B [t r u e / a] ≐ B [M / a]$ ✅

This can be generalized by Shannon expansion.

If $a : B oo l ≫ P \in B$ then $P [M / a] ≐ i f (P [t r u e / a]; P [f a l se / a]) (M)$

Which can be seen as a "pivot on $M$ ". Binary decision diagrams are created by choosing pivots in a way that minimizes the size of conditionals.

The given facts look like definitions in a formal type system, and this is intentional.
Semantics define what is true, and formalisms that follow are a pale approximation which are useful for impl.
These "little lemmas" are the method of logical relations; type-indexed information determines what equality means.

There exists a type system containing a type `Nat`

$N a t ≐ N a t$

$M ≐ M^{'} \in N a t$

is the extremal (strongest/least) statement s.t.

Either $(M ^{'} ⇓ 0 M ⇓ 0)$
Or $(M ^{'} ⇓ s u cc ( N ^{'} ) M ⇓ s u cc ( N ))$ $N ≐ N^{'} \in N a t$
The extremal clause provides a morally-equivalent notion of an induction principle.

Given some assumptions

$0 v a l$

$s u cc ( M ) v a l$

We can define the Y-combinator

$f i x (a . s u cc (a)) \mapsto ω : = s u cc (f i x a . s u cc (a))$

$ω \in C o N a t$

is thus the greatest solution to the specification

$ω \in / N a t$

We may now define a recursor $R$ .

$R : = rec (M_{\circ}; a, b . M_{1}) (M) \mapsto rec (M_{\circ}; a, b . M_{1}) (M^{'})$

$M \mapsto M^{'}$

and

$R (0) \mapsto M_{\circ}$

and

$R (s u cc (m)) \mapsto M_{1} [M, R (M) / a, b]$

Fact

$a : N a t ≫ B t y p e$ $M_{\circ} \in B [0/ a]$ $a : N a t, b : B ≫ M_{1} \in B [s u cc (a) / a]$

If $M \in N a t$ then $R (M) \in B [M / a]$

Proof

Case for $0$ :

$M ⇓ 0$
$M ≐ 0 \in N a t$
$M_{\circ} \in B [0/ a] ≐ B [m / a]$
$R (M) ≐ R (0) ≐ M_{\circ}$
$R (M) \in B [M / a]$
$■$

Case for $s u cc (N)$

$M ⇓ s u cc (N)$
Given an inductive hypothesis $R (N) \in B [N / a]$ ... (the proof is unfinished)

These ( $B oo l$ , $N a t$ ) are representative examples of inductive types (least extremal clauses that satisfy some conditions). They are not representative examples of coinductive types (most extremal clauses that imply/are consistent with some conditions).

There exists a type system containing a type `Prod`

$(A_{1} \times A_{2}) ≐ (A_{1}^{'} \times A_{2}^{'})$

$i ff$

$A_{1} ≐ A_{1}^{'}$

and

$A_{2} ≐ A_{2}^{'}$

and

$M ≐ M^{'} \in (A_{1} \times A_{2})$

$i ff$

${M ⇓ ⟨ M_{1}, M_{2} ⟩ M^{'} ⇓ ⟨ M_{1}^{'}, M_{2}^{'} ⟩$

where

$M_{n} ≐ M_{n}^{'} \in A_{n}$

that is, that the values for each $M_{n}$ are evaluated under the conditions in $A_{n}$

Fact

If $M \in A_{1} \times A_{2}$ then $M .0 \in A_{1}$ and $M .1 \in A_{2}$ (one could sub other notation here, e.g. fst, etc.)

where

$\frac{M \mapsto M ^{'}}{M . i _{1} \mapsto M . i _{2}}$

and

$( M _{1} , M _{2} ) . i \mapsto M _{i}$

and $(i = f s t, s n d)$

A note about logical relations as a tactic: membership in product types is defined in terms of equality in each of the component types. Constituent types are, in a sense, already given, and then we speak about the composite types.

Going further...

If $M_{1} \in A_{1}$ , then $(M_{1}, M_{2}) .1 ≐ M_{1} \in A_{1}$ , which has no requirement on $M_{2}$ .

Recall that by head-expansion (a.k.a reverse-execution) $(M_{1}, M_{2}) .1 \mapsto M_{1}$ .

This may seem like a "technical anomaly", but is an important insight into how computational type theory relies on specifications as opposed to a grammar for writing down well-formed things according to syntactic rules that impose additional requirements beyond those described by this fact. Formalisms are about obeying protocols.

Completing the proof of fact w.r.t. Prod from the assumptions (in similar vein to the earlier examples) is left as an exercise.

There exists a type system containing a type `Fn`

$A_{1} \to A_{2} ≐ A_{1}^{'} \to A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'}$

and

$A_{2} ≐ A_{2}^{'}$

and

$M ≐ M^{'} \in A_{1} \to A_{2}$

$i ff$

$M ⇓ λa . M_{2}$

and

$M^{'} ⇓ λa . M_{2}^{'}$

where

$a : A ≫ M_{2} ≐ M_2 \in A_{2}$

Given some assumptions

$λa . M v a l$

$\frac{M \mapsto M ^{'}}{a p ( M , M 1 ) \mapsto a p ( M ^{'} , M _{1} )}$

$a p ( λa . M _{2} , M 1 ) \mapsto M _{2} [ M _{1} / a ]$

The latter is a kind of $β$ -reduction, or at least a well-specified reduction strategy.

Fact

If $M \in A_{1} \to A_{2}$ and $M_{1} \in A_{1}$ then $a p (M, M_{1}) \in A_{2}$ .

We can translate this into a usual type-theoretic notation like so

$\frac{Γ ⊢ M : A _{1} \to A _{2} Γ ⊢ M _{1} : A _{1}}{Γ ⊢ a p ( M , M _{1} ) : A _{2}}$

and the inductive definition is the "protocol" or "syntax" of the aforementioned fact.

Observe: what is the quantifier complexity of $M ≐ M^{'} \in N a t \to N a t$ ?

In an informal sense, one can say

$\forall M_{1} ≐ M_{1}^{'} \in N a t \exists P_{1} ≐ P_{1}^{'} \in N a t$

such that

$a p (M, M_{1}) ≐ a p (M^{'}, M_{1}^{'}) \in N a t$

This is the reason that starting with the formal syntax is inadequate, because an induction rule like

$Γ ⊢ M \equiv M ^{'} : N a t \to N a t$

is a derivation tree that results in a quantifier complexity of "there exists something". But $\forall \exists$ cannot be captured by $\exists$ alone!

Fact

$M, M^{'} \in A_{1} \to A_{2}$

and

$a : A_{1} ≫ a p (M, a) ≐ a p (M^{'}, a)$

then

$M ≐ M^{'} \in A_{1} \to A_{2}$

One may call this "function extensionality"

Completing the proof of facts w.r.t. Fn from the assumptions (in similar vein to the earlier examples) is left as an exercise.

This is profound: One cannot axiomatize equality in $N a t \to N a t$ by a deeper understanding of Gödel's theorem.

There exists a type system containing a type `Dependent Prod`

$a : A_{1} \times A_{2} ≐ a : A_{1}^{'} \times A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'}$

$a : A_{1} ≫ A_{2} ≐ A_{2}^{'}$

$M ≐ M^{'} \in (A_{1} \times A_{2})$

$i ff$ ${M ⇓ ⟨ M_{1}, M_{2} ⟩ M^{'} ⇓ ⟨ M_{1}^{'}, M_{2}^{'} ⟩$

where

$M_{1} ≐ M_{1}^{'} \in A_{1}$

and, different from Prod,

$M_{2} ≐ M_{2}^{'} \in A_{2} [M_{1} / a] ≐ A_{2} [M_{1}^{'} / a]$

which encodes the dependency between $A_{1}$ and $A_{2}$ .

There exists a type system containing a type `Dependent Fn`

$a : A_{1} \to A_{2} ≐ a : A_{1}^{'} \to A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'} - a : A_{1} ≫ A_{2} ≐ A_{2}^{'}$

From the definition, it's easy enough to look back at the definitions / initial transitions for Fn and subsitute the following, as we did for Prod

$a : A_{1} ≫ M_{2} ≐ M_{2}^{'} \in A_{2} (a)$

The meaning of the change is as follows:

$M_{1} ≐ M_{1}^{'} \in A_{1}$

then

$M_{2} [M_{1} / a] ≐ M_{2} [M_{1}^{'} / a] \in A_{2} [M_{1} / a] ≐ A_{2} [M_{1}^{'} / a]$

Fact

If $M \in a : A_{1} \times A_{2}$ then $M .0 \in A_{1}$ and $M .1 \in A_{2} [M .0/ a]$
If $M \in a : A_{1} \to A_{2}$ and $M_{1} \in A_{1}$ then $a p (M, M_{1}) \in A_{2} [M_{1} / a]$