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 infinite: 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".

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 signature of the function List:

#check List    -- List.{u} (α : Type u) : Type u

Here u 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    -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

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 => x + 5     -- Nat inferred
#check λ x => 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. The ⟨ and ⟩ characters may be typed with \langle and \rangle or \< and \>, respectively.

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          -- Lst.{u} (α : Type u) : Type u
#check Lst.cons     -- Lst.cons.{u} (α : Type u) (a : α) (as : Lst α) : Lst α
#check Lst.nil      -- Lst.nil.{u} (α : Type u) : Lst α
#check Lst.append   -- Lst.append.{u} (α : Type u) (as bs : 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        -- {α : Sort 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.