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.t                   type abstraction
      t [T]                  type application

v ::=                    values
      λx.t                   abstraction value
      λX.t                  type abstraction value

T ::=                    types
      T → T                  types of functions
      X                      type variable
      ∀X.T                   universal 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 ::=                       types
      X                         type variable
      λX::K.T                   operator abstraction
      T T                       operator application
      T → T                     types of functions

Γ ::=                       contexts
      ∅                         empty context
      Γ , x:T                   term variable binding
      Γ , X::K                  type variable binding

K ::=                       kinds
      *                         kind of proper types
      K⟹K                      kind 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'

KINDING

X::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 EQUIVALENCE

T ≡ 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 ::=                     types
      X                       type/family variable
      Πx:T.T                  dependent product type
      T t                     type family application

K ::=                     kinds
      *                       kind of proper types
      Πx:T.K                  kind of type families

Γ ::=                     contexts
      ∅                       empty context
      Γ , x:T                 term variable binding
      Γ , X::K                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'

WELL-FORMED KINDS

Γ ⊢ *

Γ ⊢ T::*    Γ, x:T ⊢ K
----------------------
      Γ ⊢ Πx:T.K

KINDING

X::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 ≡ K3

TYPE 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::K

TERM 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

[Back to Top]