2. Dependent Type Theory

Dependent type theory is a powerful and expressive language, allowing us to express complex mathematical assertions, write complex hardware and software specifications, and reason about both of these in a natural and uniform way. 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. By the end of this chapter, you will understand much of what this means.

2.1. Simple Type Theory

As a foundation for mathematics, set theory has a simple ontology that is rather appealing. Everything is a set, including numbers, functions, triangles, stochastic processes, and Riemannian manifolds. It is a remarkable fact that one can construct a rich mathematical universe from a small number of axioms that describe a few basic set-theoretic constructions.

But for many purposes, including formal theorem proving, it is better to have an infrastructure that helps us manage and keep track of the various kinds of mathematical objects we are working with. “Type theory” gets its name from the fact that every expression has an associated type. For example, in a given context, x + 0 may denote a natural number and f may denote a function on the natural numbers.

Here are some examples of how we can declare objects in Lean and check their types.

/- declare some constants -/

constant m : nat        -- m is a natural number
constant n : nat
constants b1 b2 : bool  -- declare two constants at once

/- check their types -/

#check m            -- output: nat
#check n
#check n + 0        -- nat
#check m * (n + 0)  -- nat
#check b1           -- bool
#check b1 && b2     -- "&&" is boolean and
#check b1 || b2     -- boolean or
#check tt           -- boolean "true"

-- Try some examples of your own.

Any text between the /- and -/ constitutes a comment that is ignored by Lean. Similarly, two dashes indicate that the rest of the line contains a comment that is also ignored. Comment blocks can be nested, making it possible to “comment out” chunks of code, just as in many programming languages.

The constant and constants commands introduce new constant symbols into the working environment. The #check command asks Lean to report their types; in Lean, commands that query the system for information typically begin with the hash symbol. You should try declaring some constants and type checking some expressions on your own. Declaring new objects in this way is a good way to experiment with the system, but it is ultimately undesirable: Lean is a foundational system, which is to say, it provides us with powerful mechanisms to define all the mathematical objects we need, rather than simply postulating them. We will explore these mechanisms in the chapters to come.

What makes simple type theory powerful is that one can build new types out of others. For example, if α and β are types, α β denotes the type of functions from α to β, and α × β denotes the cartesian product, that is, the type of ordered pairs consisting of an element of α paired with an element of β.

constants m n : nat

constant f : nat  nat           -- type the arrow as "\to" or "\r"
constant f' : nat -> nat         -- alternative ASCII notation
constant f'' :                -- alternative notation for nat
constant p : nat × nat           -- type the product as "\times"
constant q : prod nat nat        -- alternative notation
constant g : nat  nat  nat
constant g' : nat  (nat  nat)  -- has the same type as g!
constant h : nat × nat  nat

constant F : (nat  nat)  nat   -- a "functional"

#check f               -- ℕ → ℕ
#check f n             -- ℕ
#check g m n           -- ℕ
#check g m             -- ℕ → ℕ
#check (m, n)          -- ℕ × ℕ
#check p.1             -- ℕ
#check p.2             -- ℕ
#check (m, n).1        -- ℕ
#check (p.1, n)        -- ℕ × ℕ
#check F f             -- ℕ

Once again, you should try some examples on your own.

Let us dispense with some basic syntax. You can enter the unicode arrow by typing \to or \r. You can also use the ASCII alternative ->, so that the expression nat -> nat and nat nat mean the same thing. Both expressions denote the type of functions that take a natural number as input and return a natural number as output. The symbol is alternative unicode notation for nat; you can enter it by typing \nat. The unicode symbol × for the cartesian product is entered \times. We will generally use lower-case greek letters like α, β, and γ to range over types. You can enter these particular ones with \a, \b, and \g.

There are a few more things to notice here. First, the application of a function f to a value x is denoted f x. Second, when writing type expressions, arrows associate to the right; for example, the type of g is nat (nat nat). Thus we can view g as a function that takes natural numbers and returns another function that takes a natural number and returns a natural number. In type theory, this is generally more convenient than writing g as a function that takes a pair of natural numbers as input, and returns a natural number as output. For example, it allows us to “partially apply” the function g. The example above shows that g m has type nat nat, that is, the function that “waits” for a second argument, n, and then returns g m n. Taking a function h of type nat × nat nat and “redefining” it to look like g is a process known as currying, something we will come back to below.

By now you may also have guessed that, in Lean, (m, n) denotes the ordered pair of m and n, and if p is a pair, p.1 and p.2 denote the two projections.

2.2. Types as Objects

One way in which Lean’s dependent type theory extends simple type theory is that types themselves — entities like nat and bool — are first-class citizens, which is to say that they themselves are objects of study. For that to be the case, each of them also has to have a type.

#check nat               -- Type
#check bool              -- Type
#check nat  bool        -- Type
#check nat × bool        -- Type
#check nat  nat         -- ...
#check nat × nat  nat
#check nat  nat  nat
#check nat  (nat  nat)
#check nat  nat  bool
#check (nat  nat)  nat

We see that each one of the expressions above is an object of type Type. We can also declare new constants and constructors for types:

constants α β : Type
constant F : Type  Type
constant G : Type  Type  Type

#check α        -- Type
#check F α      -- Type
#check F nat    -- Type
#check G α      -- Type → Type
#check G α β    -- Type
#check G α nat  -- Type

Indeed, we have already seen an example of a function of type Type Type Type, namely, the Cartesian product.

constants α β : Type

#check prod α β       -- Type
#check prod nat nat   -- Type

Here is another example: given any type α, the type list α denotes the type of lists of elements of type α.

constant α : Type

#check list α    -- Type
#check list nat  -- Type

For those more comfortable with set-theoretic foundations, it may be helpful to think of a type as nothing more than a set, in which case, the elements of the type are just the elements of the set. Given that every expression in Lean has a type, it is natural to ask: what type does Type itself have?

#check Type      -- Type 1

We have actually come up against one of the most subtle aspects of Lean’s typing system. Lean’s underlying foundation has an infinite hierarchy of types:

#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5

Think of Type 0 as a universe of “small” or “ordinary” types. Type 1 is then a larger universe of types, which contains Type 0 as an element, and Type 2 is an even larger universe of types, which contains Type 1 as an element. The list is indefinite, so that there is a Type n for every natural number n. Type is an abbreviation for Type 0:

#check Type
#check Type 0

There is also another type, Prop, which has special properties.

#check Prop -- Type

We will discuss Prop in the next chapter.

We want some operations, however, to be polymorphic over type universes. For example, list α should make sense for any type α, no matter which type universe α lives in. This explains the type annotation of the function list:

#check list    -- Type u_1 → Type u_1

Here u_1 is a variable ranging over type levels. The output of the #check command means that whenever α has type Type n, list α also has type Type n. The function prod is similarly polymorphic:

#check prod    -- Type u_1 → Type u_2 → Type (max u_1 u_2)

To define polymorphic constants and variables, Lean allows us to declare universe variables explicitly:

universe u
constant α : Type u
#check α

Equivalently, we can write Type _ or Type* to avoid giving the arbitrary universe a name:

constant α : Type _
#check α

constant β : Type*
#check β

Throughout this book, we will generally use Type* in examples when we want type constructions to have as much generality as possible. We will come to learn that the ability to treat type constructors as instances of ordinary mathematical functions is a powerful feature of dependent type theory.

2.3. Function Abstraction and Evaluation

We have seen that if we have m n : nat, then we have (m, n) : nat × nat. This gives us a way of creating pairs of natural numbers. Conversely, if we have p : nat × nat, then we have fst p : nat and snd p : nat. This gives us a way of “using” a pair, by extracting its two components.

We already know how to “use” a function f : α β, namely, we can apply it to an element a : α to obtain f a : β. But how do we create a function from another expression?

The companion to application is a process known as “abstraction,” or “lambda abstraction.” Suppose that by temporarily postulating a variable x : α we can construct an expression t : β. Then the expression fun x : α, t, or, equivalently, λ x : α, t, is an object of type α β. Think of this as the function from α to β which maps any value x to the value t, which depends on x. For example, in mathematics it is common to say “let f be the function which maps any natural number x to x + 5.” The expression λ x : nat, x + 5 is just a symbolic representation of the right-hand side of this assignment.

#check fun x : nat, x + 5
#check λ x : nat, x + 5

Here are some more abstract examples:

constants α β  : Type
constants a1 a2 : α
constants b1 b2 : β

constant f : α  α
constant g : α  β
constant h : α  β  α
constant p : α  α  bool

#check fun x : α, f x                      -- α → α
#check λ x : α, f x                        -- α → α
#check λ x : α, f (f x)                    -- α → α
#check λ x : α, h x b1                     -- α → α
#check λ y : β, h a1 y                     -- β → α
#check λ x : α, p (f (f x)) (h (f a1) b2)  -- α → bool
#check λ x : α, λ y : β, h (f x) y         -- α → β → α
#check λ (x : α) (y : β), h (f x) y        -- α → β → α
#check λ x y, h (f x) y                    -- α → β → α

Lean interprets the final three examples as the same expression; in the last expression, Lean infers the type of x and y from the types of f and h.

Try writing some expressions on your own. Some mathematically common examples of operations of functions can be described in terms of lambda abstraction:

constants α β γ : Type
constant f : α  β
constant g : β  γ
constant b : β

#check λ x : α, x        -- α → α
#check λ x : α, b        -- α → β
#check λ x : α, g (f x)  -- α → γ
#check λ x, g (f x)

Think about what these expressions mean. The expression λ x : α, x denotes the identity function on α, the expression λ x : α, b denotes the constant function that always returns b, and λ x : α, g (f x), denotes the composition of f and g. We can, in general, leave off the type annotations on the variable and let Lean infer it for us. So, for example, we can write λ x, g (f x) instead of λ x : α, g (f x).

We can abstract over any of the constants in the previous definitions:

#check λ b : β, λ x : α, x     -- β → α → α
#check λ (b : β) (x : α), x    -- β → α → α
#check λ (g : β  γ) (f : α  β) (x : α), g (f x)
                              -- (β → γ) → (α → β) → α → γ

Lean lets us combine lambdas, so the second example is equivalent to the first. We can even abstract over the type:

#check λ (α β : Type*) (b : β) (x : α), x
#check λ (α β γ : Type*) (g : β  γ) (f : α  β) (x : α), g (f x)

The last expression, for example, denotes the function that takes three types, α, β, and γ, and two functions, g : β γ and f : α β, and returns the composition of g and f. (Making sense of the type of this function requires an understanding of dependent products, which we will explain below.) Within a lambda expression λ x : α, t, the variable x is a “bound variable”: it is really a placeholder, whose “scope” does not extend beyond t. For example, the variable b in the expression λ (b : β) (x : α), x has nothing to do with the constant b declared earlier. In fact, the expression denotes the same function as λ (u : β) (z : α), z. Formally, the expressions that are the same up to a renaming of bound variables are called alpha equivalent, and are considered “the same.” Lean recognizes this equivalence.

Notice that applying a term t : α β to a term s : α yields an expression t s : β. Returning to the previous example and renaming bound variables for clarity, notice the types of the following expressions:

constants α β γ : Type
constant f : α  β
constant g : β  γ
constant h : α  α
constants (a : α) (b : β)

#check (λ x : α, x) a                -- α
#check (λ x : α, b) a                -- β
#check (λ x : α, b) (h a)            -- β
#check (λ x : α, g (f x)) (h (h a))  -- γ

#check (λ (v : β  γ) (u : α  β) x, v (u x)) g f a   -- γ

#check (λ (Q R S : Type*) (v : R  S) (u : Q  R) (x : Q),
        v (u x)) α β γ g f a        -- γ

As expected, the expression x : α, x) a has type α. In fact, more should be true: applying the expression x : α, x) to a should “return” the value a. And, indeed, it does:

constants α β γ : Type
constant f : α  β
constant g : β  γ
constant h : α  α
constants (a : α) (b : β)

#reduce (λ x : α, x) a                -- a
#reduce (λ x : α, b) a                -- b
#reduce (λ x : α, b) (h a)            -- b
#reduce (λ x : α, g (f x)) a          -- g (f a)

#reduce (λ (v : β  γ) (u : α  β) x, v (u x)) g f a   -- g (f a)

#reduce (λ (Q R S : Type*) (v : R  S) (u : Q  R) (x : Q),
       v (u x)) α β γ g f a        -- g (f a)

The command #reduce tells Lean to evaluate an expression by reducing it to normal form, which is to say, carrying out all the computational reductions that are sanctioned by the underlying logic. The process of simplifying an expression x, t)s to t[s/x] – that is, t with s substituted for the variable x – is known as beta reduction, and two terms that beta reduce to a common term are called beta equivalent. But the #reduce command carries out other forms of reduction as well:

constants m n : nat
constant b : bool

#print "reducing pairs"
#reduce (m, n).1        -- m
#reduce (m, n).2        -- n

#print "reducing boolean expressions"
#reduce tt && ff        -- ff
#reduce ff && b         -- ff
#reduce b && ff         -- bool.rec ff ff b

#print "reducing arithmetic expressions"
#reduce n + 0           -- n
#reduce n + 2           -- nat.succ (nat.succ n)
#reduce 2 + 3           -- 5

In a later chapter, we will explain how these terms are evaluated. For now, we only wish to emphasize that this is an important feature of dependent type theory: every term has a computational behavior, and supports a notion of reduction, or normalization. In principle, two terms that reduce to the same value are called definitionally equal. They are considered “the same” by the underlying logical framework, and Lean does its best to recognize and support these identifications.

It is this computational behavior that makes it possible to use Lean as a programming language as well. Indeed, Lean extracts bytecode from terms in a computationally pure fragment of the logical framework, and can evaluate them quite efficiently:

#eval 12345 * 54321

In contrast, the #reduce command relies on Lean’s trusted kernel, the part of Lean that is responsible for checking and verifying the correctness of expressions and proofs. As such, the #reduce command is more trustworthy, but far less efficient. We will have more to say about #eval in Chapter 11, and it will play a central role in Programming in Lean. In this tutorial, however, we will generally rely on #reduce instead.

2.4. Introducing Definitions

As we have noted above, declaring constants in the Lean environment is a good way to postulate new objects to experiment with, but most of the time what we really want to do is define objects in Lean and prove things about them. The def command provides one important way of defining new objects.

def foo : (  )   := λ f, f 0

#check foo    -- (ℕ → ℕ) → ℕ
#print foo    -- λ (f : ℕ → ℕ), f 0

We can omit the type when Lean has enough information to infer it:

def foo' := λ f :   , f 0

The general form of a definition is def foo : α := bar. Lean can usually infer the type α, but it is often a good idea to write it explicitly. This clarifies your intention, and Lean will flag an error if the right-hand side of the definition does not have the right type.

Lean also allows us to use an alternative format that puts the abstracted variables before the colon and omits the lambda:

def double (x : ) :  := x + x
#print double
#check double 3
#reduce double 3    -- 6

def square (x : ) := x * x
#print square
#check square 3
#reduce square 3    -- 9

def do_twice (f :   ) (x : ) :  := f (f x)

#reduce do_twice double 2    -- 8

These definitions are equivalent to the following:

def double :    := λ x, x + x
def square :    := λ x, x * x
def do_twice : (  )     := λ f x, f (f x)

We can even use this approach to specify arguments that are types:

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

As an exercise, we encourage you to use do_twice and double to define functions that quadruple their input, and multiply the input by 8. As a further exercise, we encourage you to try defining a function Do_Twice : ((ℕ ℕ) (ℕ ℕ)) (ℕ ℕ) (ℕ ℕ) which applies its argument twice, so that Do_Twice do_twice is a function that applies its input four times. Then evaluate Do_Twice do_twice double 2.

Above, we discussed the process of “currying” a function, that is, taking a function f (a, b) that takes an ordered pair as an argument, and recasting it as a function f' a b that takes two arguments successively. As another exercise, we encourage you to complete the following definitions, which “curry” and “uncurry” a function.

def curry (α β γ : Type*) (f : α × β  γ) : α  β  γ := sorry

def uncurry (α β γ : Type*) (f : α  β  γ) : α × β  γ := sorry

2.5. Local Definitions

Lean also allows you to introduce “local” definitions using the let construct. The expression let a := t1 in t2 is definitionally equal to the result of replacing every occurrence of a in t2 by t1.

#check let y := 2 + 2 in y * y   -- ℕ
#reduce  let y := 2 + 2 in y * y   -- 16

def t (x : ) :  :=
let y := x + x in y * y

#reduce t 2   -- 16

Here, t is definitionally equal to the term (x + x) * (x + x). You can combine multiple assignments in a single let statement:

#check   let y := 2 + 2, z := y + y in z * z   -- ℕ
#reduce  let y := 2 + 2, z := y + y in z * z   -- 64

Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of a, t2) t1, but the two are not the same. In the first expression, you should think of every instance of a in t2 as a syntactic abbreviation for t1. In the second expression, a is a variable, and the expression λ a, t2 has to make sense independently of the value of a. The let construct is a stronger means of abbreviation, and there are expressions of the form let a := t1 in t2 that cannot be expressed as a, t2) t1. As an exercise, try to understand why the definition of foo below type checks, but the definition of bar does not.

def foo := let a := nat  in λ x : a, x + 2

/-
def bar := (λ a, λ x : a, x + 2) nat
-/

2.6. Variables and Sections

This is a good place to introduce some organizational features of Lean that are not a part of the axiomatic framework per se, but make it possible to work in the framework more efficiently.

We have seen that the constant command allows us to declare new objects, which then become part of the global context. Declaring new objects in this way is somewhat crass. Lean enables us to define all of the mathematical objects we need, and declaring new objects willy-nilly is therefore somewhat lazy. In the words of Bertrand Russell, it has all the advantages of theft over honest toil. We will see in the next chapter that it is also somewhat dangerous: declaring a new constant is tantamount to declaring an axiomatic extension of our foundational system, and may result in inconsistency.

So far, in this tutorial, we have used the constant command to create “arbitrary” objects to work with in our examples. For example, we have declared types α, β, and γ to populate our context. This can be avoided, using implicit or explicit lambda abstraction in our definitions to declare such objects “locally”:

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

def do_twice (α : Type*) (h : α  α) (x : α) : α := h (h x)

def do_thrice (α : Type*) (h : α  α) (x : α) : α := h (h (h x))

Repeating declarations in this way can be tedious, however. Lean provides us with the variable and variables commands to make such declarations look global:

variables (α β γ : Type*)

def compose (g : β  γ) (f : α  β) (x : α) : γ := g (f x)
def do_twice (h : α  α) (x : α) : α := h (h x)
def do_thrice (h : α  α) (x : α) : α := h (h (h x))

We can declare variables of any type, not just Type itself:

variables (α β γ : Type*)
variables (g : β  γ) (f : α  β) (h : α  α)
variable x : α

def compose := g (f x)
def do_twice := h (h x)
def do_thrice := h (h (h x))

#print compose
#print do_twice
#print do_thrice

Printing them out shows that all three groups of definitions have exactly the same effect.

The variable and variables commands look like the constant and constants commands we have used above, but there is an important difference. Rather than creating permanent entities, the former commands simply instruct Lean to insert the declared variables as bound variables in definitions that refer to them. Lean is smart enough to figure out which variables are used explicitly or implicitly in a definition. We can therefore proceed as though α, β, γ, g, f, h, and x are fixed objects when we write our definitions, and let Lean abstract the definitions for us automatically.

When declared in this way, a variable stays in scope until the end of the file we are working on, and we cannot declare another variable with the same name. Sometimes, however, it is useful to limit the scope of a variable. For that purpose, Lean provides the notion of a section:

section useful
variables (α β γ : Type*)
variables (g : β  γ) (f : α  β) (h : α  α)
variable x : α

def compose := g (f x)
def do_twice := h (h x)
def do_thrice := h (h (h x))
end useful

When the section is closed, the variables go out of scope, and become nothing more than a distant memory.

You do not have to indent the lines within a section, since Lean treats any string of returns, spaces, and tabs equivalently as whitespace. Nor do you have to name a section, which is to say, you can use an anonymous section / end pair. If you do name a section, however, you have to close it using the same name. Sections can also be nested, which allows you to declare new variables incrementally.

We will see in Chapter 6 that, as a scoping mechanism, sections govern more than just variables; other commands have effects that are only operant in the current section. Similarly, if we use the open command inside a section, it only remains in effect until that section is closed.

2.7. Namespaces

Lean provides us with the ability to group definitions into nested, hierarchical namespaces:

namespace foo
def a :  := 5
def f (x : ) :  := x + 7

def fa :  := f a
def ffa :  := f (f a)

#print "inside foo"

#check a
#check f
#check fa
#check ffa
#check foo.fa
end foo

#print "outside the namespace"

-- #check a  -- error
-- #check f  -- error
#check foo.a
#check foo.f
#check foo.fa
#check foo.ffa

open foo

#print "opened foo"

#check a
#check f
#check fa
#check foo.fa

When we declare that we are working in the namespace foo, every identifier we declare has a full name with prefix “foo.” Within the namespace, we can refer to identifiers by their shorter names, but once we end the namespace, we have to use the longer names.

The open command brings the shorter names into the current context. Often, when we import a theory file, we will want to open one or more of the namespaces it contains, to have access to the short identifiers. But sometimes we will want to leave this information hidden, for example, when they conflict with identifiers in another namespace we want to use. Thus namespaces give us a way to manage our working environment.

For example, Lean groups definitions and theorems involving lists into a namespace list.

#check list.nil
#check list.cons
#check list.append

We will discuss their types, below. The command open list allows us to use the shorter names:

open list

#check nil
#check cons
#check append

Like sections, namespaces can be nested:

namespace foo
def a :  := 5
def f (x : ) :  := x + 7

def fa :  := f a

namespace bar
def ffa :  := f (f a)

#check fa
#check ffa
end bar

#check fa
#check bar.ffa
end foo

#check foo.fa
#check foo.bar.ffa

open foo

#check fa
#check bar.ffa

Namespaces that have been closed can later be reopened, even in another file:

namespace foo
def a :  := 5
def f (x : ) :  := x + 7

def fa :  := f a
end foo

#check foo.a
#check foo.f

namespace foo
def ffa :  := f (f a)
end foo

Like sections, nested namespaces have to be closed in the order they are opened. Also, a namespace cannot be declared within a section; namespaces have to live on the outer levels.

Namespaces and sections serve different purposes: namespaces organize data and sections declare variables for insertion in theorems. In many respects, however, a namespace ... end block behaves the same as a section ... end block. In particular, if you use the variable command within a namespace, its scope is limited to the namespace. Similarly, if you use an open command within a namespace, its effects disappear when the namespace is closed.

2.8. Dependent Types

You have now seen one way of defining functions and objects in Lean, and we will gradually introduce you to many more. But an important goal in Lean is to prove things about the objects we define, and the next chapter will introduce you to Lean’s mechanisms for stating theorems and constructing proofs. Meanwhile, let us remain on the topic of defining objects in dependent type theory for just a moment longer. In this section, we will explain what makes dependent type theory dependent, and why dependent types are useful.

The short explanation is that what makes dependent type theory dependent is that types can depend on parameters. You have already seen a nice example of this: the type list α depends on the argument α, and this dependence is what distinguishes list and list bool. For another example, consider the type vec α n, the type of vectors of elements of α of length n. This type depends on two parameters: the type α : Type of the elements in the vector and the length n : .

Suppose we wish to write a function cons which inserts a new element at the head of a list. What type should cons have? Such a function is polymorphic: we expect the cons function for , bool, or an arbitrary type α to behave the same way. So it makes sense to take the type to be the first argument to cons, so that for any type, α, cons α is the insertion function for lists of type α. In other words, for every α, cons α is the function that takes an element a : α and a list l : list α, and returns a new list, so we have cons α a l : list α.

It is clear that cons α should have type α list α list α. But what type should cons have? A first guess might be Type α list α list α, but, on reflection, this does not make sense: the α in this expression does not refer to anything, whereas it should refer to the argument of type Type. In other words, assuming α : Type is the first argument to the function, the type of the next two elements are α and list α. These types vary depending on the first argument, α.

This is an instance of a Pi type, or dependent function type. Given α : Type and β : α Type, think of β as a family of types over α, that is, a type β a for each a : α. In that case, the type Π x : α, β x denotes the type of functions f with the property that, for each a : α, f a is an element of β a. In other words, the type of the value returned by f depends on its input.

Notice that Π x : α, β makes sense for any expression β : Type. When the value of β depends on x (as does, for example, the expression β x in the previous paragraph), Π x : α, β denotes a dependent function type. When β doesn’t depend on x, Π x : α, β is no different from the type α β. Indeed, in dependent type theory (and in Lean), the Pi construction is fundamental, and α β is just notation for Π x : α, β when β does not depend on x.

Returning to the example of lists, we can model some basic list operations as follows. We use namespace hidden to avoid a naming conflict with the list type defined in the standard library.

namespace hidden

universe u

constant list   : Type u  Type u

constant cons   : Π α : Type u, α  list α  list α
constant nil    : Π α : Type u, list α
constant head   : Π α : Type u, list α  α
constant tail   : Π α : Type u, list α  list α
constant append : Π α : Type u, list α  list α  list α

end hidden

You can enter the symbol Π by typing \Pi. Here, nil is intended to denote the empty list, head and tail return the first element of a list and the remainder, respectively. The constant append is intended to denote the function that concatenates two lists.

We emphasize that these constant declarations are only for the purposes of illustration. The list type and all these operations are, in fact, defined in Lean’s standard library, and are proved to have the expected properties. Moreover, as the next example shows, the types indicated above are essentially the types of the objects that are defined in the library. (We will explain the @ symbol and the difference between the round and curly brackets momentarily.)

open list

#check list     -- Type u_1 → Type u_1

#check @cons    -- Π {α : Type u_1}, α → list α → list α
#check @nil     -- Π {α : Type u_1}, list α
#check @head    -- Π {α : Type u_1} [_inst_1 : inhabited α], list α → α
#check @tail    -- Π {α : Type u_1}, list α → list α
#check @append  -- Π {α : Type u_1}, list α → list α → list α

There is a subtlety in the definition of head: the type α is required to have at least one element, and when passed the empty list, the function must determine a default element of the relevant type. We will explain how this is done in Chapter 10.

Vector operations are handled similarly:

universe u
constant vec : Type u    Type u

namespace vec
constant empty : Π α : Type u, vec α 0
constant cons :
  Π (α : Type u) (n : ), α  vec α n  vec α (n + 1)
constant append :
  Π (α : Type u) (n m : ),  vec α m  vec α n  vec α (n + m)
end vec

In the coming chapters, you will come across many instances of dependent types. Here we will mention just one more important and illustrative example, the Sigma types, Σ x : α, β x, sometimes also known as dependent products. These are, in a sense, companions to the Pi types. The type Σ x : α, β x denotes the type of pairs sigma.mk a b where a : α and b : β a.

Just as Pi types Π x : α, β x generalize the notion of a function type α β by allowing β to depend on α, Sigma types Σ x : α, β x generalize the cartesian product α × β in the same way: in the expression sigma.mk a b, the type of the second element of the pair, b : β a, depends on the first element of the pair, a : α.

variable α : Type
variable β : α  Type
variable a : α
variable b : β a

#check sigma.mk a b      -- Σ (a : α), β a
#check (sigma.mk a b).1  -- α
#check (sigma.mk a b).2  -- β (sigma.fst (sigma.mk a b))

#reduce  (sigma.mk a b).1  -- a
#reduce  (sigma.mk a b).2  -- b

Notice that the expressions (sigma.mk a b).1 and (sigma.mk a b).2 are short for sigma.fst (sigma.mk a b) and sigma.snd (sigma.mk a b), respectively, and that these reduce to a and b, respectively.

2.9. Implicit Arguments

Suppose we have an implementation of lists as described above.

namespace hidden
universe u
constant list : Type u  Type u

namespace list
constant cons   : Π α : Type u, α  list α  list α
constant nil    : Π α : Type u, list α
constant append : Π α : Type u, list α  list α  list α
end list
end hidden

Then, given a type α, some elements of α, and some lists of elements of α, we can construct new lists using the constructors.

open hidden.list

variable  α : Type
variable  a : α
variables l1 l2 : list α

#check cons α a (nil α)
#check append α (cons α a (nil α)) l1
#check append α (append α (cons α a (nil α)) l1) l2

Because the constructors are polymorphic over types, we have to insert the type α as an argument repeatedly. But this information is redundant: one can infer the argument α in cons α a (nil α) from the fact that the second argument, a, has type α. One can similarly infer the argument in nil α, not from anything else in that expression, but from the fact that it is sent as an argument to the function cons, which expects an element of type list α in that position.

This is a central feature of dependent type theory: terms carry a lot of information, and often some of that information can be inferred from the context. In Lean, one uses an underscore, _, to specify that the system should fill in the information automatically. This is known as an “implicit argument.”

#check cons _ a (nil _)
#check append _ (cons _ a (nil _)) l1
#check append _ (append _ (cons _ a (nil _)) l1) l2

It is still tedious, however, to type all these underscores. When a function takes an argument that can generally be inferred from context, Lean allows us to specify that this argument should, by default, be left implicit. This is done by putting the arguments in curly braces, as follows:

namespace list
constant cons   : Π {α : Type u}, α  list α  list α
constant nil    : Π {α : Type u}, list α
constant append : Π {α : Type u}, list α  list α  list α
end list

open hidden.list

variable  α : Type
variable  a : α
variables l1 l2 : list α

#check cons a nil
#check append (cons a nil) l1
#check append (append (cons a nil) l1) l2

All that has changed are the braces around α : Type u in the declaration of the variables. We can also use this device in function definitions:

universe u
def ident {α : Type u} (x : α) := x

variables α β : Type u
variables (a : α) (b : β)

#check ident      -- ?M_1 → ?M_1
#check ident a    -- α
#check ident b    -- β

This makes the first argument to ident implicit. Notationally, this hides the specification of the type, making it look as though ident simply takes an argument of any type. In fact, the function id is defined in the standard library in exactly this way. We have chosen a nontraditional name here only to avoid a clash of names.

Variables can also be specified as implicit when they are declared with the variables command:

universe u

section
variable {α : Type u}
variable x : α
def ident := x
end

variables α β : Type u
variables (a : α) (b : β)

#check ident
#check ident a
#check ident b

This definition of ident here has the same effect as the one above.

Lean has very complex mechanisms for instantiating implicit arguments, and we will see that they can be used to infer function types, predicates, and even proofs. The process of instantiating these “holes,” or “placeholders,” in a term is often known as elaboration. The presence of implicit arguments means that at times there may be insufficient information to fix the meaning of an expression precisely. An expression like id or list.nil is said to be polymorphic, because it can take on different meanings in different contexts.

One can always specify the type T of an expression e by writing (e : T). This instructs Lean’s elaborator to use the value T as the type of e when trying to resolve implicit arguments. In the second pair of examples below, this mechanism is used to specify the desired types of the expressions id and list.nil:

#check list.nil             -- list ?M1
#check id                   -- ?M1 → ?M1

#check (list.nil : list )  -- list ℕ
#check (id :   )         -- ℕ → ℕ

Numerals are overloaded in Lean, but when the type of a numeral cannot be inferred, Lean assumes, by default, that it is a natural number. So the expressions in the first two #check commands below are elaborated in the same way, whereas the third #check command interprets 2 as an integer.

#check 2            -- ℕ
#check (2 : )      -- ℕ
#check (2 : )      -- ℤ

Sometimes, however, we may find ourselves in a situation where we have declared an argument to a function to be implicit, but now want to provide the argument explicitly. If foo is such a function, the notation @foo denotes the same function with all the arguments made explicit.

#check @id        -- Π {α : Type u_1}, α → α
#check @id α      -- α → α
#check @id β      -- β → β
#check @id α a    -- α
#check @id β b    -- β

Notice that now the first #check command gives the type of the identifier, id, without inserting any placeholders. Moreover, the output indicates that the first argument is implicit.

2.10. Exercises

  1. Define the function Do_Twice, as described in Section 2.4.

  2. Define the functions curry and uncurry, as described in Section 2.4.

  3. Above, we used the example vec α n for vectors of elements of type α of length n. Declare a constant vec_add that could represent a function that adds two vectors of natural numbers of the same length, and a constant vec_reverse that can represent a function that reverses its argument. Use implicit arguments for parameters that can be inferred. Declare some variables and check some expressions involving the constants that you have declared.

  4. Similarly, declare a constant matrix so that matrix α m n could represent the type of m by n matrices. Declare some constants to represent functions on this type, such as matrix addition and multiplication, and (using vec) multiplication of a matrix by a vector. Once again, declare some variables and check some expressions involving the constants that you have declared.