# Dependent Type Theory and Interactive Theorem Prover

## Preface

This summer I studied Benjamin C. Pierce’s book Software Foundations, as a preparation for the master thesis on type system in automn.

I was so excited playing with the interactive theorem prover **Coq**
that I did all the proof exercises in the book. Throughout the book, I
learned a lot of interesting things that I would always want to dive
into:

- Formulate proofs in Coq
- inductive types
- structural recursion
- dependent type theory behind Coq
- automation of proofs

- Formalise operational semantics for programming language
- big-step and small-step styles
- side effects and/or concurrency
- determinism
- paritial evaluation
- program equivalence
- hoare logic

- Formalise type systems
- normalization
- progress, preservation
- STLC and extensions(reference, records and subtyping)

I’ve already touched some of the topics like operational semantics, hoare logic and type system elsewhere before, but it’s in this book that I capture more mathematical details and subtleties.

In this post, I’d like to explain generally what *dependent type
theory* is, and how *interactive theorem provers* work on top of it.

## Simply Typed Lambda Calculus

The simplest intesting type system is *Simply Typed Lambda
Calculus*(STLC), introduced by mathematician and logician Alonzo
Church in 1940.

Following is the informal specification of STLC:

SYNTAX t ::= terms x variable λx:T.t abstraction t t application v ::= values λx.t abstraction value T ::= types T → T types of functions Γ ::= contexts ∅ empty context Γ , x:T term variable binding EVALUATION (λx:T.t) v ⟶ [x ⟼ v]t (E-AppAbs) t1 ⟶ t1' ------------------ (E-App1) t1 t2 ⟶ t1' t2 t2 ⟶ t2' ------------------ (E-App2) v1 t2 ⟶ v1 t2' TYPING Γ, x: T1 ⊢ t: T2 --------------------- (T-Abs) Γ ⊢ λx:T1.t : T1 → T2 x:T ∈ Γ ---------- (T-Var) Γ ⊢ x : T Γ ⊢ t1: T → T', t2: T ----------------------- (T-App) Γ ⊢ t1 t2: T

Note that pure STLC is useless, it can be easily extended with base
types, sum types, product types, reference types, record types, and so
on. Interested reader can refer to chapter 11 of *Types and
Programming Languages* for more details.

As functions lie at the core of computation, a different approach to enrich the typing for computation is to extend the concept of functions. An ordinary function in STLC takes a value of a specific type and returns a value of a specific type. A curious mind would naturally ask following questions:

- Can functions take a type as parameter?
- Can functions return a type?

As functions taking multiple parameters can be reduced to functions taking only one parameter, via a well known technique called Currying, here we only need to think the case of functions taking a single parameter, though the parameter could also be a function. So there are four possible combinations with regard to the possible conceptions of functions:

- value -> value
- type -> value
- type -> type
- value -> type

The first conception of function is what we have in STLC. The type of
a function taking a parameter of type S and returning a value of type
T is usually denoted as `S -> T`

, the operator `->`

is
right-associative.

## Universal Types ( type -> value )

The idea of functions taking a type as function parameter and
returning a value gives rise to *universal types*, formalized as
System F, which was first introduced by logician Jean-Yves Girard
in 1972. System F is the theoretical foundation for templates in C++
and generics in Java.

For a function `f`

, which takes a type and returns a value, what role
does the parameter `T`

play in the return value of `f T`

? The only
possibility is that the type of `f T`

depends on `T`

. As the type of
`f T`

depends on `T`

, the type of `f`

needs to explicitly introduce
the type parameter `T`

, which is usually denoted as `∀T.S`

. For
example, the following function `twice`

in Scala can be formalized as
`λT.λf:T->T.λx.f (f x)`

in System F, its type is ```
∀T.(T -> T) -> T ->
T
```

:

```
def twice[T](f: T=>T) = (x:T) => f(f(x))
```

Following is the informal specification of System F:

SYNTAX t ::= terms x variable λx:T.t abstraction t t applicationλX.ttype abstractiont [T]type application v ::= values λx.t abstraction valueλX.ttype abstraction value T ::= types T → T types of functionsXtype variable∀X.Tuniversal type Γ ::= contexts ∅ empty context Γ , x:T term variable binding Γ, X type variable binding EVALUATION (λx:T.t) v ⟶ [x ⟼ v]t (E-AppAbs) t1 ⟶ t1' ------------------ (E-App1) t1 t2 ⟶ t1' t2 t2 ⟶ t2' ------------------ (E-App2) v1 t2 ⟶ v1 t2't1 ⟶ t1' ------------------- (E-TApp) t1 [T2] ⟶ t1' [T2](λX.t) [T] ⟶ [X ⟼ T]t (E-TappTabs)TYPING x:T ∈ Γ ---------- (T-Var) Γ ⊢ x : T Γ, x: T1 ⊢ t: T2 --------------------- (T-Abs) Γ ⊢ λx:T1.t : T1 → T2 Γ ⊢ t1: T → T', t2: T ----------------------- (T-App) Γ ⊢ t1 t2: TΓ , X ⊢ t : T ---------------- (T-TAbs) Γ ⊢ λX.t : ∀X.TΓ ⊢ t : ∀X.T ------------------------- (T-TApp) Γ ⊢ t [T1] : [X ⟼ T1]T

## Type Operators ( type -> type )

The idea of functions taking a type and returning a type leads to
*type operators*, which build new types from existing types. The most
common type operators in real world programming languages are generic
collections like Pair, List, Set, Array and so on. Unlike universal
types, type operators are not terms, they can only exist in the type
domain, thus they have no types themselves. Their well-formedness is
formulated with the concept *kind*. The case class `Pair`

below in
Scala has the *kind* `* => * => *`

:

```
case class Pair[S, T](fst: S, snd: T)
```

Type operators complicate type checking, as there could be a lot of
equivalent types. For example, suppose `Id = λX.X`

, then all of the
following types are equivalent:

```
Nat → Bool Nat → Id Bool Id Nat → Id Bool
Id Nat → Bool Id (Nat → Bool) Id (Id (Id Nat → Bool))
```

The informal specification of type operators is as follows:

SYNTAX t ::= terms x variable λx:T.t abstraction t t application v ::= values λx.t abstraction value T ::= typesXtype variableλX::K.Toperator abstractionT Toperator application T → T types of functions Γ ::= contexts ∅ empty context Γ , x:T term variable binding Γ ,X::Ktype variable bindingK::= kinds*kind of proper typesK⟹Kkind of operators EVALUATION (λx:T.t) v ⟶ [x ⟼ v]t (E-AppAbs) t1 ⟶ t1' ------------------ (E-App1) t1 t2 ⟶ t1' t2 t2 ⟶ t2' ------------------ (E-App2) v1 t2 ⟶ v1 t2'KINDINGX::K ∈ Γ ---------- (K-TVar) Γ ⊢ X :: K Γ, X::K1 ⊢ T2::K2 ----------------------- (K-Abs) Γ ⊢ λX::K1.T2 :: K1⟹K2 Γ ⊢ T1:: K11⟹K12 Γ ⊢ T2::K11 -------------------------------- (K-App) Γ ⊢ T1 T2 :: K12 Γ ⊢ T1 :: * Γ ⊢ T2 :: * --------------------------- (K-Arrow) Γ ⊢ T1→T2 :: *TYPE EQUIVALENCET ≡ T (Q-Refl) T ≡ S ----- (Q-Symm) S ≡ T S ≡ U U ≡ T ------------- (Q-Trans) S ≡ T S1 ≡ T1 S2 ≡ T2 ----------------- (Q-Arrow) S1→S2 ≡ T1→T2 S2 ≡ T2 --------------------- (Q-Abs) λX::K1.S2 ≡ λX::K1.T2 S1 ≡ T1 S2 ≡ T2 ------------------ (Q-App) S1 S2 ≡ T1 T2 (λX::K11.T12) T2 ≡ [X ⟼ T2]T12 (Q-AppAbs) TYPING x:T ∈ Γ ---------- (T-Var) Γ ⊢ x : T Γ ⊢ t1: T → T', t2: T ----------------------- (T-App) Γ ⊢ t1 t2: TΓ ⊢ T1::*Γ, x:T1 ⊢ t:T2 --------------------------- (T-Abs) Γ ⊢ λx:T1.t : T1 → T2 Γ ⊢ t:S S ≡ T Γ ⊢ T::* -------------------------(T-Eq)Γ ⊢ t : T

## Dependent Types ( value -> type )

The idea of taking a value and returning a type gives rise to
*dependent types*. We can think such functions as a special kind of
type operators. The difference is that the parameters for type
operators are types, but the parameters for dependent types are
values. While universal types allow programmers to express more
abstractions in a type system, dependent types enable programmers to
depict more fine-grained types by imposing value restrictions on canon
types.

For a function `f`

, which takes a value and returns a type, where can
the expression `f v`

occur? Can it occur in the value domain? Of
course not, a type can only occur in the type domain. Where does `v`

come from? As it’s a value, obviously it must come from the value
domain. Then how does the value domain entity `v`

meet the type domain
entity `f`

in the expression `f v`

? The answer is that there’s a
function `g`

which takes a value `v`

and returns a value `g v`

, the
type of `g v`

depends on `v`

and `f`

. That’s how a value `v`

plays a
role in the type domain and works together with a function `f`

from
value to types.

As `v`

plays a role in the type of `g v`

, the type of `g`

needs to
introduce `v`

explicitly, which is usually denoted as `Πv:S.T`

. If `T`

doesn’t depend on `v`

, then `Πv:S.T`

is exactly `S -> T`

. Thus,
dependent types is a generalization of function types in STLC.

One instrcutive example in *Advanced Types and Programming Languages*
is to use dependent types to type the function `sprintf`

as follows:

```
sprintf : Πf:Format. Data(f) -> String
```

The function `Data`

can be defined as follows:

```
Data([]) = Unit
Data("%d"::cs) = Nat * Data(cs)
Data("%s"::cs) = String * Data(cs)
Data(c::cs) = Data(cs)
```

The informal specification of dependent types is as follows:

SYNTAX t ::= terms x variable λx:T.t abstraction t t application v ::= values λx.t abstraction value T ::= typesXtype/family variableΠx:T.Tdependent product typeT ttype family application K ::= kinds*kind of proper typesΠx:T.Kkind of type families Γ ::= contexts ∅ empty context Γ , x:T term variable binding Γ ,X::Ktype variable binding EVALUATION (λx:T.t) v ⟶ [x ⟼ v]t (E-AppAbs) t1 ⟶ t1' ------------------ (E-App1) t1 t2 ⟶ t1' t2 t2 ⟶ t2' ------------------ (E-App2) v1 t2 ⟶ v1 t2'WELL-FORMED KINDSΓ ⊢ * Γ ⊢ T::* Γ, x:T ⊢ K ---------------------- Γ ⊢ Πx:T.KKINDINGX::K ∈ Γ Γ ⊢ K ------------------ (K-Var) Γ ⊢ X :: K Γ ⊢ T1::∗ Γ, x:T1 ⊢ T2::∗ ---------------------------- (K-Pi) Γ ⊢ Πx:T1.T2 :: Πx:T1.∗ Γ ⊢ S::Πx:T.K Γ ⊢ t:T -------------------------- (K-App) Γ ⊢ S t :: [x ⟼ t]K Γ ⊢ T::K Γ ⊢ K≡K′ ------------------- (K-Conv) Γ ⊢ T :: K′ TYPING x:T ∈ ΓΓ ⊢ T :: ∗----------------------- (T-Var) Γ ⊢ x : TΓ ⊢ S::∗ Γ, x:S ⊢ t:T ------------------------ (T-Abs) Γ ⊢ λx:S.t : Πx:S.TΓ ⊢ t1: Πx:S.T Γ ⊢ t2:S -------------------------- (T-App) Γ ⊢ t1 t2 : [x ⟼ t2]TΓ ⊢ t:T Γ ⊢ T≡T′::∗ ------------------------ (T-Conv) Γ ⊢ t : T′KIND EQUIVALENCEΓ ⊢ T1 ≡ T2 ::∗ Γ, x:T1 ⊢ K1 ≡ K2 ------------------------------------ (QK-Pi) Γ ⊢ Πx:T.K ≡ Πx:T2.K2 Γ ⊢ K ------------ (QK-Refl) Γ ⊢ K ≡ K Γ ⊢ K1 ≡ K2 --------------- (QK-Sym) Γ ⊢ K2 ≡ K1 Γ ⊢ K1 ≡ K2 Γ ⊢ K2 ≡ K3 ---------------------------- (QK-Trans) Γ ⊢ K1 ≡ K3TYPE EQUIVALENCEΓ ⊢ S1 ≡ T1 ::∗ Γ, x:T1 ⊢ S2 ≡ T2 ::∗ ------------------------------------------- (QT-Pi) Γ ⊢ Πx:S1.S2 ≡ Πx:T1.T2 :: ∗ Γ ⊢ S1 ≡ S2 ::Πx:T.K Γ ⊢ t1 ≡ t2 :T ------------------------------------------ (QT-App) Γ ⊢ S1 t1 ≡ S2 t2 :: [x ⟼ t1]K Γ ⊢ T:K ---------- (QT-Refl) Γ ⊢ T ≡ T::K Γ ⊢ T ≡ S::K ------------- (QT-Sym) Γ ⊢ S ≡ T::K Γ ⊢ S ≡ U::K Γ ⊢ U ≡ T::K --------------------------- (QT-Trans) Γ ⊢ S ≡ T::KTERM EQUIVALENCEΓ ⊢ S1 ≡ S2 ::∗ Γ, x:S1 ⊢ t1 ≡ t2 :T --------------------------------------- (Q-Abs) Γ ⊢ λx:S1.t1 ≡ λx:S2.t2 : Πx:S1.T Γ ⊢ t1 ≡ s1 :Πx:S.T Γ ⊢ t2 ≡ s2 :S --------------------------------------- (Q-App) Γ ⊢ t1 t2 ≡ s1 s2 : [x ⟼ t2]T Γ, x:S ⊢ t:T Γ ⊢ s:S ------------------------------------ (Q-Beta) Γ ⊢ (λx:S.t) s ≡ [x ⟼ s]t:[x ⟼ s]T Γ ⊢ t:Πx:S.T x ∉ FV(t) ------------------------- (Q-Eta) Γ ⊢ λx:T.t x ≡ t: Πx:S.T Γ ⊢ t:T ----------- (Q-Refl) Γ ⊢ t ≡ t:T Γ ⊢ t ≡ s:T ----------- (Q-Sym) Γ ⊢ s ≡ t:T Γ ⊢ s ≡ u : T Γ ⊢ u ≡ t : T ------------------------------ (Q-Trans) Γ ⊢ s ≡ t : T

## Lambda Cube

In the above, I outlined three different approaches to extend STLC:

- universal types(System F)
- type operators(λω)
- dependent types(λΠ)

These approaches can be combined arbitrarily to form a lambda cube, which was introduced by mathematician Henk Barendregt in 1991:

(credit: wikipedia)

Read the cube as follows:

```
λ-> STLC
λP dependent types
λ2 System F
λ_ω type operators
λω System F + type operators( System Fω)
λP2 dependent type + System F
λP_ω dependent type + type operators
λPω dependent type + type operators + System F(Calculus of Constructions)
```

As you can see in the diagram, the cube culminates in *Calculus of
Constructions*(CC), which was introduced by Coquand and Huet in 1988.
CC is the foundation of proof assistants.

The specification of CC is much simpler as can be seen below:

SYNTAX t ::= terms * type x variables Πx:t.t dependent type λx:t.t abstraction t t application EVALUATION (λx:T.t) v ⟶ [x ⟼ v]t (E-AppAbs) t1 ⟶ t1' ------------------ (E-App1) t1 t2 ⟶ t1' t2 t2 ⟶ t2' ------------------ (E-App2) v1 t2 ⟶ v1 t2' T1 ⟶ T1' ------------------ (E-Abs1) λx:T1.t ⟶ λx:T1'.t t ⟶ t' ------------------ (E-Abs2) λx:T.t ⟶ λx:T.t' T1 ⟶ T1' ------------------ (E-Prod1) Πx:T1.t ⟶ Πx:T1'.t t ⟶ t' ------------------ (E-Prod2) Πx:T.t ⟶ Πx:T.t' TYPING Γ ⊢ *:* (T-Axiom) Γ ⊢ T:* ----------------- (T-Var) Γ, x:T ⊢ x : T Γ, x:S ⊢ T:* ---------------- (T-Type) Γ ⊢ (Πx:S.T) : * Γ, x:S ⊢ t:T Γ ⊢ T:* ----------------------- (T-Abs) Γ ⊢ λx:S.t : Πx:S.T Γ ⊢ t: (Πx:S.T) Γ ⊢ v:S --------------------------- (T-App) Γ ⊢ t v: [x ⟼ v]T Γ ⊢ t:T T ⟶ T' Γ ⊢ T':* ---------------------------- (T-Beta) Γ ⊢ t : T'

Note that in the above, the rule *T-Axiom* says the type of “*” is
itself. For programming languages, this rule is harmless. But for CC
to be used as the foundation of proof assistant, this rule will lead to
a problem, well-known as
Girard’s Paradox.

To avoid such a paradox, a hierarchy of type universes has to be
maintained, as Coq does. In Coq, the type of *type n* is *type n+1*. It
means the type of *type* in *universe n* is *type* in *universe
n+1*. Interested readers can refer to this
link for more
details about universes in Coq.

## Propositions as Types

The bridge between logic and type system is the well-known
*Curry-Howard Correspondence*. Strictly speaking, the mapping between
*intuitionistic logic* and *intuitionistic type theory* has two
dimensions:

- propositions correspond to types
- proofs correspond to programs

Thus, to show that a proposition is provable, we only need to show the corresponding types are inhabited by a program. That’s the core idea of behind proof assistants like Coq.

The most important correspondence is the mapping between implication
and function types. In intuitionistic logic, the proof of hypothetical
judgement `A -> B`

is a function which transforms the proof of `A`

to
the proof of `B`

. In type theory, a function of type `A -> B`

would
witness a proof of `A -> B`

.

Theoretically, the more fundamental correspondance is mapping between
universal quantification and dependent types. This is because just
like function types `A -> B`

is a degenerate case of `Πx:A.B`

where
`x`

doesn’t appear in `B`

, an implication `A -> B`

is just a
quantification over a proposition `∀x:A, B`

, where the quantified
variable `x`

is never used.

Following core definitions from Coq make the correspondence between propositions and types more evident:

```
Inductive True : Prop :=
I : True.
Inductive False : Prop :=.
Definition not (A:Prop) := A -> False.
Inductive and (A B:Prop) : Prop :=
conj : A -> B -> A /\ B
where "A /\ B" := (and A B) : type_scope.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
Inductive eq (A:Type) (x:A) : A -> Prop :=
eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.
Notation "´exists´ x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
(at level 200, x binder, right associativity,
format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Inductive sig (A : Type) (P : A -> Prop) : Type :=
exist : forall x : A, P x -> {x : A | P x}.
```

## Interactive Proof Assistants

Proof assistants like Coq actually depend on an extension of CC called
*Calculus of Inductive Constructions*. I refer readers to chapter 2 of
the online book *Certified Programming with Dependent Types* for an
excellent explanation.

## Reference

- Martin-Löf dependent type theory
- On the Meanings of the Logical Constants and the Justifications of the Logical Laws
*Per Martin-Lof¨* - Software Foundations
- Certified Programming with Dependent Types
*Adam Chlipala* - Calculus of Inductive Constructions
- A short and flexible proof of Strong Normalization for the Calculus of Constructions
- Universe