1.8 Functions and Lambda Abstraction

Functions are the main form of computation in Lean. A function takes an input, produces an output, and has a type that records both the input type and the output type. Lambda abstraction is the syntax for constructing a function directly, without first giving it a global name.

Problem

You want to define functions, apply them to arguments, pass them to other functions, and understand the relation between named definitions and anonymous functions.

Solution

Use fun to construct an anonymous function.

#check fun x : Nat => x + 1

Lean reports:

fun x => x + 1 : Nat -> Nat

Apply the function by writing the argument after it:

#eval (fun x : Nat => x + 1) 5

Expected result:

A named definition is usually just a lambda expression with a name attached:

def addOne : Nat -> Nat :=
  fun x => x + 1

#eval addOne 5

Function Types

The type:

Nat -> Nat

means a function from natural numbers to natural numbers.

A function with two arguments has a curried type:

Nat -> Nat -> Nat

This associates to the right:

Nat -> (Nat -> Nat)

So a two-argument function can be understood as a function that takes one argument and returns another function.

def add : Nat -> Nat -> Nat :=
  fun x => fun y => x + y

#check add
#check add 3
#eval add 3 4

The expression add 3 has type Nat -> Nat.

Short Lambda Syntax

Several parameters may be written together:

def add' : Nat -> Nat -> Nat :=
  fun x y => x + y

This is syntactic sugar for nested lambdas:

def add'' : Nat -> Nat -> Nat :=
  fun x => fun y => x + y

Both definitions compute the same way.

Named Parameters

A definition can bind parameters before the type annotation:

def addNamed (x y : Nat) : Nat :=
  x + y

This is equivalent in ordinary use to:

def addLambda : Nat -> Nat -> Nat :=
  fun x y => x + y

The first style is more common for named functions. The second style is useful when discussing functions as values.

Function Application

Function application has high precedence and associates to the left.

addNamed 1 2

means:

(addNamed 1) 2

This matters when functions are returned by other functions.

def makeAdder (x : Nat) : Nat -> Nat :=
  fun y => x + y

#eval makeAdder 10 5
#eval (makeAdder 10) 5

Both evaluations return:

Higher-Order Functions

A higher-order function takes a function as an argument or returns a function as a result.

def applyTwice (f : Nat -> Nat) (x : Nat) : Nat :=
  f (f x)

#eval applyTwice (fun x => x + 1) 10

Expected result:

The function applyTwice is reusable with any function of type Nat -> Nat.

#eval applyTwice (fun x => x * 2) 10

Expected result:

Polymorphic Functions

A function can work over any type.

def idExplicit (α : Type) (x : α) : α :=
  x

Using implicit type arguments is more convenient:

def idImplicit {α : Type} (x : α) : α :=
  x

#check idImplicit 10
#check idImplicit "lean"
#check idImplicit true

Lean infers the type α from the argument.

Lambda Abstraction in Proofs

A proof of implication is a function.

theorem imp_id (P : Prop) : P -> P :=
  fun h => h

This theorem constructs a function from proofs of P to proofs of P.

The tactic version is:

theorem imp_id_by (P : Prop) : P -> P := by
  intro h
  exact h

Both proofs have the same logical shape.

Dependent Functions

In a dependent function type, the output type may depend on the input value.

def chooseFin (n : Nat) : Fin (n + 1) :=
  ⟨0, Nat.succ_pos n⟩

The result type changes with n. For n = 3, the result type is Fin 4; for n = 10, it is Fin 11.

Dependent functions are written with parentheses:

(n : Nat) -> Fin (n + 1)

This means that for each natural number n, the function returns an element of Fin (n + 1).

Anonymous Functions in Collections

Lambda abstraction is common with list operations.

#eval List.map (fun x : Nat => x + 1) [1, 2, 3]

Expected result:

[2, 3, 4]

Filtering uses a function returning Bool:

#eval List.filter (fun x : Nat => x % 2 == 0) [1, 2, 3, 4, 5, 6]

Expected result:

[2, 4, 6]

Partial Application

Because functions are curried, partial application is ordinary function construction.

def addTen : Nat -> Nat :=
  addNamed 10

#eval addTen 7

Expected result:

This is often cleaner than writing:

def addTen' : Nat -> Nat :=
  fun x => addNamed 10 x

Both definitions are equivalent in behavior.

Function Composition

Function composition can be written directly:

def composeNat (f g : Nat -> Nat) : Nat -> Nat :=
  fun x => f (g x)

def inc (n : Nat) : Nat :=
  n + 1

def double (n : Nat) : Nat :=
  n * 2

#eval composeNat inc double 10

Expected result:

The function double runs first, then inc.

Extensional View of Functions

Two functions are equal when they give equal outputs for every input. In Lean this usually requires function extensionality.

theorem add_zero_fun_eq : (fun n : Nat => n + 0) = (fun n : Nat => n) := by
  funext n
  simp

The tactic funext n reduces equality of functions to equality of values at an arbitrary input n.

Common Pitfalls

If Lean cannot infer the type of a lambda parameter, add an annotation.

fun x : Nat => x + 1

If application groups incorrectly, add parentheses.

(f x) y
f (x y)

If a partially applied function has an unexpected type, inspect it with #check.

If an implicit type argument is not inferred, use @ to expose all arguments.

#check @idImplicit

Takeaway

Functions in Lean are first-class values. Lambda abstraction constructs functions directly, named definitions attach names to function expressions, and currying makes partial application natural. The same mechanism also explains implication in proofs: a proof of P -> Q is a function from proofs of P to proofs of Q.