Dependent Type Theory
Dependent type theory is a powerful and expressive language, allowing you 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.
Simple Type Theory
"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. For those who like precise definitions, a Lean natural number
is an arbitrary-precision unsigned integer.
Here are some examples of how you can declare objects in Lean and check their types.
/- Define some constants. -/
def m : Nat := 1 -- m is a natural number
def n : Nat := 0
def b1 : Bool := true -- b1 is a Boolean
def b2 : Bool := false
/- 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 the Boolean and
#check b1 || b2 -- Boolean or
#check true -- Boolean "true"
/- Evaluate -/
#eval 5 * 4 -- 20
#eval m + 2 -- 3
#eval b1 && b2 -- false
Any text between /- and -/ constitutes a comment block 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 def keyword declares new constant symbols into the
working environment. In the example above, def m : Nat := 1
defines a new constant m of type Nat whose value is 1.
The #check command asks Lean to report their
types; in Lean, auxiliary commands that query the system for
information typically begin with the hash (#) symbol.
The #eval command asks Lean to evaluate the given expression.
You should try
declaring some constants and type checking some expressions on your
own. Declaring new objects in this manner is a good way to experiment
with the system.
What makes simple type theory powerful is that you can build new types
out of others. For example, if a and b are types, a -> b
denotes the type of functions from a to b, and a × b
denotes the type of pairs consisting of an element of a paired
with an element of b, also known as the Cartesian product. Note
that × is a Unicode symbol. The judicious use of Unicode improves
legibility, and all modern editors have great support for it. In the
Lean standard library, you often see Greek letters to denote types,
and the Unicode symbol → as a more compact version of ->.
#check Nat → Nat -- type the arrow as "\to" or "\r"
#check Nat -> Nat -- alternative ASCII notation
#check Nat × Nat -- type the product as "\times"
#check Prod Nat Nat -- alternative notation
#check Nat → Nat → Nat
#check Nat → (Nat → Nat) -- same type as above
#check Nat × Nat → Nat
#check (Nat → Nat) → Nat -- a "functional"
#check Nat.succ -- Nat → Nat
#check (0, 1) -- Nat × Nat
#check Nat.add -- Nat → Nat → Nat
#check Nat.succ 2 -- Nat
#check Nat.add 3 -- Nat → Nat
#check Nat.add 5 2 -- Nat
#check (5, 9).1 -- Nat
#check (5, 9).2 -- Nat
#eval Nat.succ 2 -- 3
#eval Nat.add 5 2 -- 7
#eval (5, 9).1 -- 5
#eval (5, 9).2 -- 9
Once again, you should try some examples on your own.
Let's take a look at some basic syntax. You can enter the unicode
arrow → by typing \to or \r or \->. You can also use the
ASCII alternative ->, so the expressions 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 unicode symbol × for the Cartesian product
is entered as \times. You 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 (e.g., Nat.succ 2).
Second, when writing type expressions, arrows associate to the right; for
example, the type of Nat.add is Nat → Nat → Nat which is equivalent
to Nat → (Nat → Nat). Thus you can
view Nat.add as a function that takes a natural number and returns
another function that takes a natural number and returns a natural
number. In type theory, this is generally more convenient than
writing Nat.add as a function that takes a pair of natural numbers as
input and returns a natural number as output. For example, it allows
you to "partially apply" the function Nat.add. The example above shows
that Nat.add 3 has type Nat → Nat, that is, Nat.add 3 returns a
function that "waits" for a second argument, n, which is then
equivalent to writing Nat.add 3 n.
You have seen that if you have m : Nat and n : Nat, then
(m, n) denotes the ordered pair of m and n which is of
type Nat × Nat. This gives you a way of creating pairs of natural
numbers. Conversely, if you have p : Nat × Nat, then you can write
p.1 : Nat and p.2 : Nat. This gives you a way of extracting
its two components.
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. 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
You can see that each one of the expressions above is an object of
type Type. You can also declare new constants for types:
def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod
#check α -- Type
#check F α -- Type
#check F Nat -- Type
#check G α -- Type → Type
#check G α β -- Type
#check G α Nat -- Type
As the example above suggests, you have already seen an example of a function of type
Type → Type → Type, namely, the Cartesian product Prod:
def α : Type := Nat
def β : Type := Bool
#check Prod α β -- Type
#check α × β -- Type
#check Prod Nat Nat -- Type
#check Nat × Nat -- Type
Here is another example: given any type α, the type List α
denotes the type of lists of elements of type α.
def α : Type := Nat
#check List α -- Type
#check List Nat -- Type
Given that every expression in Lean has a type, it is natural to ask:
what type does Type itself have?
#check Type -- Type 1
You 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
The following table may help concretize the relationships being discussed. Movement along the x-axis represents a change in the universe, while movement along the y-axis represents a change in what is sometimes referred to as "degree".
| sort | Prop (Sort 0) | Type (Sort 1) | Type 1 (Sort 2) | Type 2 (Sort 3) | ... |
| type | True | Bool | Nat -> Type | Type -> Type 1 | ... |
| term | trivial | true | fun n => Fin n | fun (_ : Type) => Type | ... |
Some operations, however, need 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, Lean allows you to
declare universe variables explicitly using the universe command:
universe u
def F (α : Type u) : Type u := Prod α α
#check F -- Type u → Type u
You can avoid the universe command by providing the universe parameters when defining F.
def F.{u} (α : Type u) : Type u := Prod α α
#check F -- Type u → Type u
Function Abstraction and Evaluation
Lean provides a fun (or λ) keyword to create a function
from an expression as follows:
#check fun (x : Nat) => x + 5 -- Nat → Nat
#check λ (x : Nat) => x + 5 -- λ and fun mean the same thing
#check fun x : Nat => x + 5 -- Nat inferred
#check λ x : Nat => x + 5 -- Nat inferred
You can evaluate a lambda function by passing the required parameters:
#eval (λ x : Nat => x + 5) 10 -- 15
Creating a function from another expression is a process known as
lambda abstraction. Suppose you have the variable x : α and you 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.
Here are some more examples
#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2
#check fun x y => if not y then x + 1 else x + 2 -- Nat → Bool → Nat
Lean interprets the final three examples as the same expression; in
the last expression, Lean infers the type of x and y from the
expression if not y then x + 1 else x + 2.
Some mathematically common examples of operations of functions can be described in terms of lambda abstraction:
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check fun x : Nat => x -- Nat → Nat
#check fun x : Nat => true -- Nat → Bool
#check fun x : Nat => g (f x) -- Nat → Bool
#check fun x => g (f x) -- Nat → Bool
Think about what these expressions mean. The expression
fun x : Nat => x denotes the identity function on Nat, the
expression fun x : Nat => true denotes the constant function that
always returns true, and fun x : Nat => g (f x) denotes the
composition of f and g. You can, in general, leave off the
type annotation and let Lean infer it for you. So, for example, you
can write fun x => g (f x) instead of fun x : Nat => g (f x).
You can pass functions as parameters and by giving them names f
and g you can then use those functions in the implementation:
#check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
-- (String → Bool) → (Nat → String) → Nat → Bool
You can also pass types as parameters:
#check fun (α β γ : 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 will be explained below.)
The general form of a lambda expression is fun x : α => t, where
the variable x is a "bound variable": it is really a placeholder,
whose "scope" does not extend beyond the expression t. For
example, the variable b in the expression fun (b : β) (x : α) => b
has nothing to do with the constant b declared earlier. In fact,
the expression denotes the same function as fun (u : β) (z : α) => u.
Formally, 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:
#check (fun x : Nat => x) 1 -- Nat
#check (fun x : Nat => true) 1 -- Bool
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check
(fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
-- Bool
As expected, the expression (fun x : Nat => x) 1 has type Nat.
In fact, more should be true: applying the expression (fun x : Nat => x) to 1 should "return" the value 1. And, indeed, it does:
#eval (fun x : Nat => x) 1 -- 1
#eval (fun x : Nat => true) 1 -- true
You will see later how these terms are evaluated. For now, notice that this is an important feature of dependent type theory: every term has a computational behavior, and supports a notion of normalization. In principle, two terms that reduce to the same value are called definitionally equal. They are considered "the same" by Lean's type checker, and Lean does its best to recognize and support these identifications.
Lean is a complete programming language. It has a compiler that
generates a binary executable and an interactive interpreter. You can
use the command #eval to execute expressions, and it is the
preferred way of testing your functions.
Definitions
Recall that the def keyword provides one important way of declaring new named
objects.
def double (x : Nat) : Nat :=
x + x
This might look more familiar to you if you know how functions work in
other programming languages. The name double is defined as a
function that takes an input parameter x of type Nat, where the
result of the call is x + x, so it is returning type Nat. You
can then invoke this function using:
def double (x : Nat) : Nat :=
x + x
#eval double 3 -- 6
In this case you can think of def as a kind of named lambda.
The following yields the same result:
def double : Nat → Nat :=
fun x => x + x
#eval double 3 -- 6
You can omit the type declarations when Lean has enough information to infer it. Type inference is an important part of Lean:
def double :=
fun (x : Nat) => x + x
The general form of a definition is def foo : α := bar where
α is the type returned from the expression 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 a matching
type.
The right hand side bar can be any expression, not just a lambda.
So def can also be used to simply name a value like this:
def pi := 3.141592654
def can take multiple input parameters. Let's create one
that adds two natural numbers:
def add (x y : Nat) :=
x + y
#eval add 3 2 -- 5
The parameter list can be separated like this:
def double (x : Nat) : Nat :=
x + x
def add (x : Nat) (y : Nat) :=
x + y
#eval add (double 3) (7 + 9) -- 22
Notice here we called the double function to create the first
parameter to add.
You can use other more interesting expressions inside a def:
def greater (x y : Nat) :=
if x > y then x
else y
You can probably guess what this one will do.
You can also define a function that takes another function as input. The following calls a given function twice passing the output of the first invocation to the second:
def double (x : Nat) : Nat :=
x + x
def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
f (f x)
#eval doTwice double 2 -- 8
Now to get a bit more abstract, you can also specify arguments that are like type parameters:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
This means compose is a function that takes any two functions as input
arguments, so long as those functions each take only one input.
The type algebra β → γ and α → β means it is a requirement
that the type of the output of the second function must match the
type of the input to the first function - which makes sense, otherwise
the two functions would not be composable.
compose also takes a 3rd argument of type α which
it uses to invoke the second function (locally named f) and it
passes the result of that function (which is type β) as input to the
first function (locally named g). The first function returns a type
γ so that is also the return type of the compose function.
compose is also very general in that it works over any type
α β γ. This means compose can compose just about any 2 functions
so long as they each take one parameter, and so long as the type of
output of the second matches the input of the first. For example:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def double (x : Nat) : Nat :=
x + x
def square (x : Nat) : Nat :=
x * x
#eval compose Nat Nat Nat double square 3 -- 18
Local Definitions
Lean also allows you to introduce "local" definitions using the
let keyword. The expression let a := t1; t2 is
definitionally equal to the result of replacing every occurrence of
a in t2 by t1.
#check let y := 2 + 2; y * y -- Nat
#eval let y := 2 + 2; y * y -- 16
def twice_double (x : Nat) : Nat :=
let y := x + x; y * y
#eval twice_double 2 -- 16
Here, twice_double x is definitionally equal to the term (x + x) * (x + x).
You can combine multiple assignments by chaining let statements:
#check let y := 2 + 2; let z := y + y; z * z -- Nat
#eval let y := 2 + 2; let z := y + y; z * z -- 64
The ; can be omitted when a line break is used.
def t (x : Nat) : Nat :=
let y := x + x
y * y
Notice that the meaning of the expression let a := t1; t2 is very
similar to the meaning of (fun 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
fun 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; t2 that cannot be
expressed as (fun 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; fun x : a => x + 2
/-
def bar := (fun a => fun x : a => x + 2) Nat
-/
Variables and Sections
Consider the following three function definitions:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (α : Type) (h : α → α) (x : α) : α :=
h (h x)
def doThrice (α : Type) (h : α → α) (x : α) : α :=
h (h (h x))
Lean provides you with the variable command to make such
declarations look more compact:
variable (α β γ : Type)
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (h : α → α) (x : α) : α :=
h (h x)
def doThrice (h : α → α) (x : α) : α :=
h (h (h x))
You can declare variables of any type, not just Type itself:
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
#print compose
#print doTwice
#print doThrice
Printing them out shows that all three groups of definitions have exactly the same effect.
The variable command instructs Lean to insert the declared
variables as bound variables in definitions that refer to them by
name. Lean is smart enough to figure out which variables are used
explicitly or implicitly in a definition. You can therefore proceed as
though α, β, γ, g, f, h, and x are fixed
objects when you write your definitions, and let Lean abstract the
definitions for you automatically.
When declared in this way, a variable stays in scope until the end of
the file you are working on. Sometimes, however, it is useful to limit
the scope of a variable. For that purpose, Lean provides the notion of
a section:
section useful
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
end useful
When the section is closed, the variables go out of scope, and cannot be referenced any more.
You do not have to indent the lines within a section. 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.
Namespaces
Lean provides you with the ability to group definitions into nested, hierarchical namespaces:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
def ffa : Nat := f (f a)
#check a
#check f
#check fa
#check ffa
#check Foo.fa
end Foo
-- #check a -- error
-- #check f -- error
#check Foo.a
#check Foo.f
#check Foo.fa
#check Foo.ffa
open Foo
#check a
#check f
#check fa
#check Foo.fa
When you declare that you are working in the namespace Foo, every
identifier you declare has a full name with prefix "Foo.". Within
the namespace, you can refer to identifiers by their shorter names,
but once you end the namespace, you have to use the longer names.
Unlike section, namespaces require a name. There is only one
anonymous namespace at the root level.
The open command brings the shorter names into the current
context. Often, when you import a module, you will want to open one or
more of the namespaces it contains, to have access to the short
identifiers. But sometimes you will want to leave this information
protected by a fully qualified name, for example, when they conflict
with identifiers in another namespace you want to use. Thus namespaces
give you a way to manage names in your working environment.
For example, Lean groups definitions and theorems involving lists into
a namespace List.
#check List.nil
#check List.cons
#check List.map
The command open List allows you to use the shorter names:
open List
#check nil
#check cons
#check map
Like sections, namespaces can be nested:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
namespace Bar
def ffa : Nat := 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 : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
end Foo
#check Foo.a
#check Foo.f
namespace Foo
def ffa : Nat := f (f a)
end Foo
Like sections, nested namespaces have to be closed in the order they
are opened. Namespaces and sections serve different purposes:
namespaces organize data and sections declare variables for insertion
in definitions. Sections are also useful for delimiting the scope of
commands such as set_option and open.
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.
What makes dependent type theory dependent?
The short explanation 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 Nat and List Bool. For another example, consider the
type Vector α n, the type of vectors of elements of α of
length n. This type depends on two parameters: the type of the
elements in the vector (α : Type) and the length of the vector
n : Nat.
Suppose you 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: you expect the cons function for
Nat, 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
as : List α, and returns a new list, so you have cons α a as : 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, α.
def cons (α : Type) (a : α) (as : List α) : List α :=
List.cons a as
#check cons Nat -- Nat → List Nat → List Nat
#check cons Bool -- Bool → List Bool → List Bool
#check cons -- (α : Type) → α → List α → List α
This is an instance of a dependent function type, or dependent
arrow 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 (a : α) → β a 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 (a : α) → β makes sense for any expression β : Type. When the value of β depends on a (as does, for
example, the expression β a in the previous paragraph),
(a : α) → β denotes a dependent function type. When β doesn't
depend on a, (a : α) → β is no different from the type
α → β. Indeed, in dependent type theory (and in Lean), α → β
is just notation for (a : α) → β when β does not depend on a.
Returning to the example of lists, you can use the command #check to
inspect the type of the following List functions. The @ symbol
and the difference between the round and curly braces will be
explained momentarily.
#check @List.cons -- {α : Type u_1} → α → List α → List α
#check @List.nil -- {α : Type u_1} → List α
#check @List.length -- {α : Type u_1} → List α → Nat
#check @List.append -- {α : Type u_1} → List α → List α → List α
Just as dependent function types (a : α) → β a generalize the
notion of a function type α → β by allowing β to depend on
α, dependent Cartesian product types (a : α) × β a generalize
the Cartesian product α × β in the same way. Dependent products
are also called sigma types, and you can also write them as
Σ a : α, β a. You can use ⟨a, b⟩ or Sigma.mk a b to create a
dependent pair.
universe u v
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a b
def h1 (x : Nat) : Nat :=
(f Type (fun α => α) Nat x).2
#eval h1 5 -- 5
def h2 (x : Nat) : Nat :=
(g Type (fun α => α) Nat x).2
#eval h2 5 -- 5
The functions f and g above denote the same function.
Implicit Arguments
Suppose we have an implementation of lists as:
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst -- Type u_1 → Type u_1
#check Lst.cons -- (α : Type u_1) → α → Lst α → Lst α
#check Lst.nil -- (α : Type u_1) → Lst α
#check Lst.append -- (α : Type u_1) → Lst α → Lst α → Lst α
Then, you can construct lists of Nat as follows.
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst -- Type u_1 → Type u_1
#check Lst.cons -- (α : Type u_1) → α → Lst α → Lst α
#check Lst.nil -- (α : Type u_1) → Lst α
#check Lst.append -- (α : Type u_1) → Lst α → Lst α → Lst α
#check Lst.cons Nat 0 (Lst.nil Nat)
def as : Lst Nat := Lst.nil Nat
def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat)
#check Lst.append Nat as bs
Because the constructors are polymorphic over types, we have to insert
the type Nat as an argument repeatedly. But this information is
redundant: one can infer the argument α in
Lst.cons Nat 5 (Lst.nil Nat) from the fact that the second argument, 5, has
type Nat. One can similarly infer the argument in Lst.nil Nat, not
from anything else in that expression, but from the fact that it is
sent as an argument to the function Lst.cons, which expects an element
of type Lst α 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."
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst -- Type u_1 → Type u_1
#check Lst.cons -- (α : Type u_1) → α → Lst α → Lst α
#check Lst.nil -- (α : Type u_1) → Lst α
#check Lst.append -- (α : Type u_1) → Lst α → Lst α → Lst α
#check Lst.cons _ 0 (Lst.nil _)
def as : Lst Nat := Lst.nil _
def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)
#check Lst.append _ as bs
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 you to specify that this argument should, by default, be left implicit. This is done by putting the arguments in curly braces, as follows:
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil {α : Type u} : Lst α := List.nil
def Lst.append {α : Type u} (as bs : Lst α) : Lst α := List.append as bs
#check Lst.cons 0 Lst.nil
def as : Lst Nat := Lst.nil
def bs : Lst Nat := Lst.cons 5 Lst.nil
#check Lst.append as bs
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
#check ident -- ?m → ?m
#check ident 1 -- Nat
#check ident "hello" -- String
#check @ident -- {α : Type u_1} → α → α
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 variable command:
universe u
section
variable {α : Type u}
variable (x : α)
def ident := x
end
#check ident
#check ident 4
#check ident "hello"
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 ?m
#check id -- ?m → ?m
#check (List.nil : List Nat) -- List Nat
#check (id : Nat → Nat) -- Nat → Nat
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 -- Nat
#check (2 : Nat) -- Nat
#check (2 : Int) -- Int
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 Nat -- Nat → Nat
#check @id Bool -- Bool → Bool
#check @id Nat 1 -- Nat
#check @id Bool true -- Bool
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.