Chapter 2: Dependent Type Theory

Lean is based on a version of dependent type theory known as the Calculus of Constructions, with a countable hierarchy of non-cumulative universes and inductive types.

Prefixing a command with a hash (#) turns it into an auxiliary command, allowing you to query the system.

The #eval command asks Lean to evaluate an expression.

Use Unicode for an arrow → (\r) instead of the ASCII ->

Use the Unicode for product × (\x) instead of the ASCII x

Use the Unicode for alpha α (\a), beta β (\b), and gamma γ (\g)

#check
Nat × Nat → Nat : Type 
Nat: Type
Nat × 
Nat: Type
Nat → 
Nat: Type
Nat
#check
(Nat → Nat) → Nat : Type (
Nat: Type
Nat → 
Nat: Type
Nat) → 
Nat: Type
Nat -- a "functional"

Functionals.

Whitespace is function application.

Arrows are right-associative.

def 
α: Type
α : 
Type: Type 1
Type := 
Nat: Type
Nat
def 
β: Type
β : 
Type: Type 1
Type := 
Bool: Type
Bool
def 
F: Type → Type
F : 
Type: Type 1
Type → 
Type: Type 1
Type := 
List: Type → Type
List
def 
G: Type → Type → Type
G : 
Type: Type 1
Type → 
Type: Type 1
Type → 
Type: Type 1
Type := 
Prod: Type → Type → Type
Prod

#check
α : Type 
α: Type
α        -- Type
#check
F α : Type 
F: Type → Type
F 
α: Type
α      -- Type
#check
F Nat : Type 
F: Type → Type
F 
Nat: Type
Nat    -- Type
#check
G α : Type → Type 
G: Type → Type → Type
G 
α: Type
α      -- Type → Type
#check
G α β : Type 
G: Type → Type → Type
G 
α: Type
α 
β: Type
β    -- Type
#check
G α Nat : Type 
G: Type → Type → Type
G 
α: Type
α 
Nat: Type
Nat  -- Type

-- Prod is a type constructor -- the infix version is ×

#check
Prod : Type u_1 → Type u_2 → Type (max u_1 u_2) 
Prod: Type u_1 → Type u_2 → Type (max u_1 u_2)
Prod -- Type → Type → Type
#check
α × β : Type 
Prod: Type → Type → Type
Prod 
α: Type
α 
β: Type
β       -- Type
#check
α × β : Type 
α: Type
α × 
β: Type
β          -- Type

#check
Nat × Nat : Type 
Prod: Type → Type → Type
Prod 
Nat: Type
Nat 
Nat: Type
Nat   -- Type
#check
Nat × Nat : Type 
Nat: Type
Nat × 
Nat: Type
Nat      -- Type

Lean has a universe of types indexed by the natural numbers. Type is an abbreviation for Type 0.

We can think of Type 0 as a universe of "small" types. Type 1 is a universe of larger types, which contains Type 0. Likewise, Type 2 is a larger-still universe of types, containing Type 1 as an element.

Some functions, like List and Prod, are polymorphic over the universe of types.

#check
List : Type u_1 → Type u_1 
List: Type u_1 → Type u_1
List
#check
Prod : Type u_1 → Type u_2 → Type (max u_1 u_2) 
Prod: Type u_1 → Type u_2 → Type (max u_1 u_2)
Prod

We can define polymorphic constants using the universe command.

universe u₁
def 
F₁: Type u₁ → Type u₁
F₁ (
α: Type u₁
α : 
Type u₁: Type (u₁ + 1)
Type u₁) : 
Type u₁: Type (u₁ + 1)
Type u₁ := 
Prod: Type u₁ → Type u₁ → Type u₁
Prod 
α: Type u₁
α 
α: Type u₁
α

#check
F₁ : Type u_1 → Type u_1 
F₁: Type u_1 → Type u_1
F₁    -- Type u → Type u

We can avoid universe by providing the universe parameters when defining the function.

def 
F₂: Type u₂ → Type u₂
F₂
F₂.{u₂}: Type u₂ → Type u₂
.{u₂} (
α: Type u₂
α : 
Type u₂: Type (u₂ + 1)
Type u₂) : 
Type u₂: Type (u₂ + 1)
Type u₂ := 
Prod: Type u₂ → Type u₂ → Type u₂
Prod 
α: Type u₂
α 
α: Type u₂
α

#check
F₂ : Type u_1 → Type u_1 
F₂: Type u_1 → Type u_1
F₂    -- Type u → Type u

Function Abstraction and Evaluation

In Lean, fun and λ are the same.

Definition: Alpha Equivalence

Expressions which are the same up to renaming of bound variables are alpha equivalent.

Definition: Definitional Equivalence

Two terms which reduce to the same value are definitionally equivalent.

The command #eval executes expressions and is the preferred way of testing your functions.

Variables and Sections

Lean has a variable command which declares variables of any type. For example,

def 
compose₁: (α β γ : Type) → (β → γ) → (α → β) → α → γ
compose₁ (
α: Type
α 
β: Type
β 
γ: Type
γ : 
Type: Type 1
Type) (
g: β → γ
g : 
β: Type
β → 
γ: Type
γ) (
f: α → β
f : 
α: Type
α → 
β: Type
β) (
x: α
x : 
α: Type
α) : 
γ: Type
γ :=
  
g: β → γ
g (
f: α → β
f 
x: α
x)

def 
doTwice₁: (α : Type) → (α → α) → α → α
doTwice₁ (
α: Type
α : 
Type: Type 1
Type) (
h: α → α
h : 
α: Type
α → 
α: Type
α) (
x: α
x : 
α: Type
α) : 
α: Type
α :=
  
h: α → α
h (
h: α → α
h 
x: α
x)

def 
doThrice₁: (α : Type) → (α → α) → α → α
doThrice₁ (
α: Type
α : 
Type: Type 1
Type) (
h: α → α
h : 
α: Type
α → 
α: Type
α) (
x: α
x : 
α: Type
α) : 
α: Type
α :=
  
h: α → α
h (
h: α → α
h (
h: α → α
h 
x: α
x))

becomes

variable (
α: Type
α 
β: Type
β 
γ: Type
γ : 
Type: Type 1
Type)

def 
compose₂: (β → γ) → (α → β) → α → γ
compose₂ (
g: β → γ
g : 
β: Type
β → 
γ: Type
γ) (
f: α → β
f : 
α: Type
α → 
β: Type
β) (
x: α
x : 
α: Type
α) : 
γ: Type
γ :=
  
g: β → γ
g (
f: α → β
f 
x: α
x)

def 
doTwice₂: (α : Type) → (α → α) → α → α
doTwice₂ (
h: α → α
h : 
α: Type
α → 
α: Type
α) (
x: α
x : 
α: Type
α) : 
α: Type
α :=
  
h: α → α
h (
h: α → α
h 
x: α
x)

def 
doThrice₂: (α : Type) → (α → α) → α → α
doThrice₂ (
h: α → α
h : 
α: Type
α → 
α: Type
α) (
x: α
x : 
α: Type
α) : 
α: Type
α :=
  
h: α → α
h (
h: α → α
h (
h: α → α
h 
x: α
x))

Lean has a section command which provides a scoping mechanism. When we close a section, the variables defined within are out of scope. You do not need to name a section, or indent its contents.

section useful
  variable (
α: Type
α 
β: Type
β 
γ: Type
γ : 
Type: Type 1
Type)
  variable (
g: β → γ
g : 
β: Type
β → 
γ: Type
γ) (
f: α → β
f : 
α: Type
α → 
β: Type
β) (
h: α → α
h : 
α: Type
α → 
α: Type
α)
  variable (
x: α
x : 
α: Type
α)

  def 
compose: γ
compose := 
g: β → γ
g (
f: α → β
f 
x: α
x)
  def 
doTwice: (α : Type) → (α → α) → α → α
doTwice := 
h: α → α
h (
h: α → α
h 
x: α
x)
  def 
doThrice: α
doThrice := 
h: α → α
h (
h: α → α
h (
h: α → α
h 
x: α
x))
end useful

Namespaces

Namespaces let you group related definitions. Like sections, they can be nested. However, unlike sections, they require a name, and can be reopened later!

The intended usage is this: namespaces organize data and sections declare variables for use in definitions or delimit the scope of commands like set_option and open.

namespace Foo
  def 
a: Nat
a : 
Nat: Type
Nat := 
5: Nat
5
  def 
f: Nat → Nat
f (
x: Nat
x : 
Nat: Type
Nat) : 
Nat: Type
Nat := 
x: Nat
x + 
7: Nat
7

  def 
fa: Nat
fa : 
Nat: Type
Nat := 
f: Nat → Nat
f 
a: Nat
a
  def 
ffa: Nat
ffa : 
Nat: Type
Nat := 
f: Nat → Nat
f (
f: Nat → Nat
f 
a: Nat
a)

  #check
a : Nat 
a: Nat
a
  #check
f : Nat → Nat 
f: Nat → Nat
f
  #check
fa : Nat 
fa: Nat
fa
  #check
ffa : Nat 
ffa: Nat
ffa
  #check
fa : Nat 
Foo.fa: Nat
Foo.fa
end Foo

-- #check a  -- error
-- #check f  -- error
#check
Foo.a : Nat 
Foo.a: Nat
Foo.a
#check
Foo.f : Nat → Nat 
Foo.f: Nat → Nat
Foo.f
#check
Foo.fa : Nat 
Foo.fa: Nat
Foo.fa
#check
Foo.ffa : Nat 
Foo.ffa: Nat
Foo.ffa

The open command brings the contents of the namespace into scope.

open Foo

#check
a : Nat 
a: Nat
a
#check
f : Nat → Nat 
f: Nat → Nat
f
#check
fa : Nat 
fa: Nat
fa
#check
fa : Nat 
Foo.fa: Nat
Foo.fa

What makes dependent type theory dependent?

Types can depend on parameters! For example, the type Vector α n is the type of vectors with elements α : Type and length n : Nat.

If you were to write a function cons which prepends an element to a list, the function would need to be polymorphic over the type of the list. One could imagine that cons α would be the function which prepends an element to a List α. So cons α would have type α → List α → List α. But what about cons? It cannot have the type of Type → α → List α → List α because α is unrelated to Type. We need to make the type of the elements of the list depend on α: cons : (α : Type) → α → List α → List α.

def 
cons: (α : Type) → α → List α → List α
cons (
α: Type
α : 
Type: Type 1
Type) (
a: α
a : 
α: Type
α) (
as: List α
as : 
List: Type → Type
List 
α: Type
α) : 
List: Type → Type
List 
α: Type
α :=
  
List.cons: {α : Type} → α → List α → List α
List.cons 
a: α
a 
as: List α
as

#check
cons Nat : Nat → List Nat → List Nat 
cons: (α : Type) → α → List α → List α
cons 
Nat: Type
Nat        -- Nat → List Nat → List Nat
#check
cons Bool : Bool → List Bool → List Bool 
cons: (α : Type) → α → List α → List α
cons 
Bool: Type
Bool       -- Bool → List Bool → List Bool
#check
cons : (α : Type) → α → List α → List α 
cons: (α : Type) → α → List α → List α
cons            -- (α : Type) → α → List α → List α

This is an instance of the dependent arrow type.

Given α : Type and β : α → Type, we can think of β as a family of types indexed by α. That is, for each a : α, we have a type β a. Then (a : α) → β a is the type of functions f with the property that f a is an element of the type β a and the type of the value returned by f depends on its input.

Note: When the value of β depends on a, (a : α) → β is called a dependent function type. When β doesn't depend on a, (a : α) → β is equivalent to α → β. In dependent type theory, α → β is the notation used when β does not depend on a.

We can use the #check command to inspect the type of the following functions from List.

#check
@List.cons : {α : Type u_1} → α → List α → List α @
List.cons: {α : Type u_1} → α → List α → List α
List.cons    -- {α : Type u_1} → α → List α → List α
#check
@List.nil : {α : Type u_1} → List α @
List.nil: {α : Type u_1} → List α
List.nil     -- {α : Type u_1} → List α
#check
@List.length : {α : Type u_1} → List α → Nat @
List.length: {α : Type u_1} → List α → Nat
List.length  -- {α : Type u_1} → List α → Nat
#check
@List.append : {α : Type u_1} → List α → List α → List α @
List.append: {α : Type u_1} → List α → List α → List α
List.append  -- {α : Type u_1} → List α → List α → List α

In the same way that the dependent arrow type generalizes the function type α → β by allowing β to depend on α, the dependent Cartesian product type (a : α) × β a generalizes the cartesian product α × β. Dependent products are also called sigma types and are written as Σ a : α, β a. You can use ⟨a, b⟩ (those are angle brackets, which you can insert with \langle (or \lan) and \rangle (or \ran)), or Sigma.mk a b to construct a dependent pair.

TO-DO: Is there another name for dependent function types if dependent Cartesian products are called sigma types? How do dependent pairs relate to dependent Cartesian products?

universe u v

def 
f: (α : Type u) → (β : α → Type v) → (a : α) → β a → (a : α) × β a
f (
α: Type u
α : 
Type u: Type (u + 1)
Type u) (
β: α → Type v
β : 
α: Type u
α → 
Type v: Type (v + 1)
Type v) (
a: α
a : 
α: Type u
α) (
b: β a
b : 
β: α → Type v
β 
a: α
a) : (
a: α
a : 
α: Type u
α) × 
β: α → Type v
β 
a: α
a :=
  ⟨
a: α
a, 
b: β a
b⟩

def 
g: (α : Type u) → (β : α → Type v) → (a : α) → β a → (a : α) × β a
g (
α: Type u
α : 
Type u: Type (u + 1)
Type u) (
β: α → Type v
β : 
α: Type u
α → 
Type v: Type (v + 1)
Type v) (
a: α
a : 
α: Type u
α) (
b: β a
b : 
β: α → Type v
β 
a: α
a) : Σ 
a: α
a : 
α: Type u
α, 
β: α → Type v
β 
a: α
a :=
  
Sigma.mk: {α : Type u} → {β : α → Type v} → (fst : α) → β fst → Sigma β
Sigma.mk 
a: α
a 
b: β a
b

def 
h1: Nat → Nat
h1 (
x: Nat
x : 
Nat: Type
Nat) : 
Nat: Type
Nat :=
  (
f: (α : Type 1) → (β : α → Type) → (a : α) → β a → (a : α) × β a
f 
Type: Type 1
Type (fun 
α: Type
α => 
α: Type
α) 
Nat: Type
Nat 
x: Nat
x).
2: {α : Type 1} → {β : α → Type} → (self : Sigma β) → β self.fst
2

#eval
5
 
h1: Nat → Nat
h1 
5: Nat
5 -- 5

def 
h2: Nat → Nat
h2 (
x: Nat
x : 
Nat: Type
Nat) : 
Nat: Type
Nat :=
  (
g: (α : Type 1) → (β : α → Type) → (a : α) → β a → (a : α) × β a
g 
Type: Type 1
Type (fun 
α: Type
α => 
α: Type
α) 
Nat: Type
Nat 
x: Nat
x).
2: {α : Type 1} → {β : α → Type} → (self : Sigma β) → β self.fst
2

#eval
5
 
h2: Nat → Nat
h2 
5: Nat
5 -- 5

The functions f and g above are the same function.

Implicit Arguments

Omitted. See the original here.