Functions in Lean are defined using the def keyword. The syntax for defining functions in Lean is
similar to defining inductive types.
These are the different types of functions we can define in Lean:
| Type of Function | Description |
|---|---|
| Pattern-matching | Functions that match patterns to produce outputs |
| Recursive | Functions that call themselves to compute results |
| Dependent | Functions where the result type depends on the argument value |
| Lambda | Anonymous functions that can be passed as arguments |
Functions are also first-class citizens in Lean, meaning they can be passed as arguments to other functions, returned as results, and stored in data structures.
Syntax for defining functions in Lean:
def-- 1. Name (not), Type (Bool → Bool)
def not : Bool → Bool
-- 2. Patterns and outputs
| true => false
| false => trueLean provides syntactical sugar to simplify the expression of certain patterns:
-- (x : α) → (y : β) → γ is equivalent to (x : α) (y : β) → γ
-- ∀ (x : α), γ is equivalent to (x : α) → γ
-- ∀ x, γ is equivalent to (x : _) → γ (type is inferred)
-- λ x y => e is equivalent to λ x => λ y => e
-- f a b is equivalent to (f a) bPattern-matching functions are functions that match patterns to produce outputs. They are defined using the
def keyword, followed by the function name, type, and pattern-matching clauses.
The verbose lean syntax for pattern matching functions is:
def functionName : inputType → outputType
match inputType with
| pattern₁ => output₁
| pattern₂ => output₂
...
| patternN => outputNThis can be shortened to:
def functionName : inputType → outputType
| pattern₁ => output₁
| pattern₂ => output₂
...
| patternN => outputNThere is also a version of pattern matching that uses a wildcard pattern (_) to match any value:
def functionName : inputType → outputType
| pattern₁ => output₁
| _ => defaultOutputThere are also infix functions, which are functions that can be used in infix notation. For example, the
and function (,) can be used as true ∧ false.
def functionName : inputType → inputType → outputType
| pattern₁, pattern₂ => output
| pattern₃, pattern₄ => outputFinally, you can define functions with multiple arguments:
def functionName : inputType₁ → inputType₂ → outputType
| pattern₁, pattern₂ => output
| pattern₃, pattern₄ => outputThe simplest of functions simply match patterns. For example, the function for not:
def not : Bool → Bool
| true => false -- return false if we are given a true
| false => true -- return a true if we are given a falseWe could also use a wildcard pattern (_) like this:
def not₁ : Bool → Bool
| true => false -- return false if we are given a true
| _ => true -- return true in all other casesIn Lean, function names containing symbols can be used as infix operators. We can define precedence and associativity
using infix, infixl, or infixr.
def and : Bool → Bool → Bool
| true, b => b -- true AND whatever is whatever
| false, _ => false -- false AND whatever is false
infixr:70 " ∧ " => andWe can use this function as:
def true₀ : Bool := true ∧ true
def false₀ : Bool := true ∧ falsedef or : Bool → Bool → Bool
| true, _ => true -- true or whatever is true
| false, b => b -- false or whatever is whatever
infixr:60 " ∨ " => orThese functions can be applied as:
def notTrue : Bool := not true
def false₁ : Bool := true ∧ false
def true₁ : Bool := true ∨ false ∨ false₁The xor function with multiple arguments and wildcards:
def xor : Bool → Bool → Bool
| true, false => true -- true XOR false is true
| false, true => true -- false XOR true is true
| _, _ => false -- all other cases are false“Guards” are conditions that can be added to pattern-matching clauses to further refine the matching process. They
are represented by if expressions that evaluate to true or false. Guards can be
used to add conditions to patterns:
def max3 (x y z : Nat) : Nat :=
match x, y, z with
| a, b, c =>
if a ≥ b && a ≥ c then a
else if b ≥ a && b ≥ c then b
else cThe max3 function takes three natural numbers x, y, and z and
returns the maximum of the three numbers. It uses pattern matching with guards to compare the numbers and determine the
maximum.
Pattern matching can also be nested to handle more complex patterns:
def deepMatch : List (Option Nat) → Nat
| [] => 0
| none::xs => deepMatch xs
| (some n)::xs => n + deepMatch xsThe deepMatch function takes a list of optional natural numbers and returns the sum of the
non-none values in the list. It uses nested pattern matching to handle the different cases of
none and some values in the list.
Recursive functions are functions that call themselves to compute results. They are useful for defining functions that operate on recursive data structures or have recursive behavior.
The syntax for defining recursive functions in Lean is similar to pattern-matching functions, but with a recursive call to the function itself.
The addition of natural numbers is a classic example of a recursive function. Here’s how it can be defined in Lean:
def add : Nat → Nat → Nat
| 0, n => n -- base case: 0 + n is n
| m+1, n => (add m n) + 1 -- recursive case: (m+1) + n is m + (n+1)
infixl:65 " + " => addThe length of a list consists of traversing through the list and adding one for each element:
def length {α : Type} : List α → Nat
| [] => 0 -- base case: empty list has length 0
| _ :: xs => 1 + length xs -- recursive case: 1 + length of the rest of the listThe length function takes a list of any type α and returns a natural number
(Nat). It uses pattern matching to handle two cases:
[]), the length is 0._ :: xs), the length is 1 plus the length of the rest of the list
(xs).This function recursively processes the list, accumulating the total count of elements until it reaches the empty list.
Dependent function types, also known as Π-types (Pi-types), represent one of the most powerful features in dependent type theory and Lean. Unlike simple function types where input and output types are fixed, dependent function types allow the output type to depend on the input value. This capability enables us to express complex relationships between values and types that would be impossible in simply-typed languages.
In Lean, dependent function types can be written in several ways:
Π (Pi) notation∀ (forall) notation→ when appropriateLet’s start with a simple example to illustrate the concept:
/-- A function that takes a type and returns a type.
Note that even this simple example is a dependent type, as
the result is a type that depends on the input type! -/
def F (α : Type) : Type := List α
/-
The type of F itself is Type → Type. This means it takes a type
and returns a type. While simple, this demonstrates the basic idea
of type dependency.
-/
#check F -- Type → Type
#check F Nat -- TypeOne powerful application of dependent types is the ability to have different return types based on a condition. Here’s an example:
/-- This function returns either a Nat or a String depending on the boolean input.
Note how the return type uses an if-expression directly in the type! -/
def natOrStringThree (b : Bool) : if b then Nat else String :=
match b with
| true => (3 : Nat)
| false => "three"Let’s examine what happens when we use this function:
#check natOrStringThree true -- Nat
#check natOrStringThree false -- String
#eval natOrStringThree true -- 3
#eval natOrStringThree false -- "three"As we can see, the return type of natOrStringThree depends on the input value b. If
b is true, the function returns a Nat, and if b is
false, it returns a String.
Perhaps the most classic example of dependent types is vectors - lists whose lengths are encoded in their types. This example showcases how dependent types can enforce properties at the type level:
A Vector is a list whose length is tracked in its type. α is the type of elements. The second parameter (Nat) indicates this is indexed by natural numbers:
inductive Vector (α : Type) : Nat → Type
| nil : Vector α 0 -- Empty vector has length 0
| cons : α → {n : Nat} → Vector α n → Vector α (n + 1) -- Adding an element increases length by 1Get the length of a vector. Note that we don’t need to examine the vector itself, as the length is encoded in its type:
def vectorLength {α : Type} {n : Nat} (v : Vector α n) : Nat := nAppend two vectors. Notice how the return type shows that lengths add:
def append {α : Type} : {n m : Nat} → Vector α n → Vector α m → Vector α (n + m)
| 0, m, Vector.nil, ys => ys
| n+1, m, Vector.cons x xs, ys => Vector.cons x (append xs ys)Let’s create some vectors to see how this works:
def v1 := Vector.cons 1 Vector.nil -- Vector Nat 1
def v2 := Vector.cons 2 (Vector.cons 3 Vector.nil) -- Vector Nat 2
#check append v1 v2 -- Vector Nat 3Dependent types often work with implicit arguments, which Lean can infer from context. Consider a function that creates a vector of a specified length filled with a value:
-- Notice how {α : Type} is implicit but (n : Nat) is explicit
def replicate {α : Type} (n : Nat) (x : α) : Vector α n :=
match n with
| 0 => Vector.nil
| n+1 => Vector.cons x (replicate n x)Next, we define a map function that applies a function to each element of a vector:
def map {α β : Type} {n : Nat} (f : α → β) : Vector α n → Vector β n
| Vector.nil => Vector.nil
| Vector.cons x xs => Vector.cons (f x) (map f xs)Let’s see how these functions work:
#eval replicate 3 true -- Vector of 3 trues
#check map (· + 1) (replicate 3 0) -- Vector Nat 3As we can see, the replicate function creates a vector of a specified length filled with a given value,
and the map function applies a function to each element of a vector.
Lambda functions, also known as anonymous functions, are functions that are not bound to a specific name. They are
useful for defining functions on the fly, passing functions as arguments, and returning functions as results. In Lean,
lambda functions are defined using the λ symbol.
Lambda (or anonymous) functions can be defined using the following syntax:
def example₁ := λ (α : Type) (x : α) => xHere are a few examples of lambda functions:
Functions in Lean can work with implicit parameters, which means the compiler can infer certain argument values. For example:
def append {α : Type} : List α → List α → List α
| [], ys => ys
| x::xs, ys => x :: append xs ys
infixr:65 " ++ " => appendCurly braces {} denote implicit arguments in Lean. Values of implicit arguments are derived from other
argument values and types by solving type equations. You don’t have to apply them explicitly (though they can be
explicitly passed like @function_name α).
This function takes a type as a parameter α, and thus can work on Lists of any type
α. This feature of functions is called “parametric polymorphism”, more on that later.
Lean supports dependent pattern matching, which is similar to Agda’s dot patterns. Here’s an example:
inductive Square : Nat → Type where
| sq : (m : Nat) → Square (m * m)
def root : (n : Nat) → Square n → Nat
| _, Square.sq m => mWe implement the map function, of “map-reduce” fame, for Lists: A map function for a
List is a function that applies a lambda (un-named) function to all elements of a List.
If f were a lambda function, mapping f over List(a, b, c, d) would produce
List(f(a), f(b), f(c), f(d))
def map {α β : Type} : (α → β) → List α → List β
| _, [] => []
| f, x :: xs => f x :: map f xsHere, we apply the function addOne to a list, using map:
def addOne : Nat → Nat
| x => x + 1
#eval map addOne [1, 2, 3, 4] -- Output: [2, 3, 4, 5]Parametric polymorphism is a feature of some programming languages that allows functions and data types to be generic over types. This means that functions and data types can be defined without specifying the exact type they operate on, making them more flexible and reusable.
In Lean, parametric polymorphism is achieved using type variables. Type variables are placeholders for types that can
be instantiated with any concrete type. They are denoted by names enclosed in curly braces {}.
Here’s an example of a parametrically polymorphic function in Lean:
def id {α : Type} (x : α) : α := xIn this example, id is a function that takes a value of any type α and returns the same
value. The type variable α is used to indicate that the function is generic over types.
Lets now look at a slightly more complex example:
def swap {α β : Type} (p : α × β) : β × α :=
match p with
| (a, b) => (b, a)In this example, swap is a function that takes a pair of values of types α and
β and returns a pair with the values swapped. The type variables α and β indicate
that the function is generic over types. The function swap can be used with any pair of values of any
types:
#eval swap (1, "hello") -- Output: ("hello", 1)
#eval swap ("world", 42) -- Output: (42, "world")Function composition is a fundamental concept in functional programming that allows you to combine multiple functions
to create a new function. In Lean, function composition can be achieved using the ∘ operator.
Here’s an example of function composition in Lean:
def addOne : Nat → Nat := λ x => x + 1
def double : Nat → Nat := λ x => x * 2We can compose the addOne and double functions to create a new function that first adds one
to a number and then doubles the result:
def addOneThenDouble : Nat → Nat := double ∘ addOneThe ∘ operator is used to compose the double function with the addOne
function. The resulting addOneThenDouble function first applies addOne to a number and then
applies double to the result.
Currying is the process of converting a function that takes multiple arguments into a sequence of functions, each taking a single argument. This allows for partial application of functions, where some arguments are provided, and the function returns a new function that takes the remaining arguments.
In Lean, currying and partial application can be achieved using lambda functions. Here’s an example:
def add : Nat → Nat → Nat := λ x y => x + yThe add function takes two arguments and returns their sum. We can curry the add function
to create a new function that takes one argument and returns a function that takes the second argument:
def addCurried : Nat → Nat → Nat := λ x => λ y => x + yWe can then partially apply the addCurried function to create a new function that adds 5 to a
number:
def addFive : Nat → Nat := addCurried 5The addFive function is a partially applied version of the addCurried function that adds 5
to a number. We can use the addFive function to add 5 to any number:
#eval addFive 10 -- Output: 15
#eval addFive 20 -- Output: 25Local definitions are used to define functions or values within the scope of another function. They are useful for breaking down complex functions into smaller, more manageable parts.
Here’s an example of using local definitions in Lean:
def sumOfSquares : Nat → Nat → Nat
| x, y =>
let square (z : Nat) : Nat := z * z
square x + square yIn this example, the sumOfSquares function takes two numbers x and y and
calculates the sum of their squares. The square function is defined locally within the
sumOfSquares function and is used to calculate the square of a number.
Local definitions are scoped to the function in which they are defined and cannot be accessed outside that function. They are a powerful tool for organizing and structuring code.
In Lean, functions are required to be total, meaning they must terminate for all inputs. This is enforced by the termination checker, which ensures that recursive functions make progress towards a base case.
Here’s an example of a recursive function that calculates the factorial of a number:
def factorial : Nat → Nat
| 0 => 1
| n+1 => (n+1) * factorial nThe factorial function calculates the factorial of a number by recursively multiplying the number by the
factorial of the previous number until it reaches the base case of 0. The termination checker ensures that the recursive
calls to factorial make progress towards the base case of 0.
Functions that do not terminate or make progress towards a base case will be rejected by the termination checker, preventing non-terminating functions from being defined in Lean.
Mutual recursion is a technique where two or more functions call each other in a cycle. This can be useful for defining functions that have interdependent behavior.
Here’s an example of mutual recursion in Lean:
mutual
def isEven : Nat → Bool
| 0 => true
| n+1 => isOdd n
def isOdd : Nat → Bool
| 0 => false
| n+1 => isEven nIn this example, the isEven and isOdd functions are defined mutually recursively. The
isEven function checks if a number is even by calling the isOdd function, and the
isOdd function checks if a number is odd by calling the isEven function. This mutual recursion
allows the functions to work together to determine if a number is even or odd.
Higher-order functions are functions that take other functions as arguments or return functions as results. They are a powerful feature of functional programming that allows for the composition and abstraction of functions.
Here’s an example of a higher-order function in Lean:
def apply {α β : Type} (f : α → β) (x : α) : β := f xThe apply function takes a function f that maps values of type α to values of
type β and a value x of type α and applies the function f to the
value x. This higher-order function allows for the application of arbitrary functions to values.
A slight variation of the apply function is the applyTwice function:
def applyTwice {α : Type} (f : α → α) (x : α) : α := f (f x)The applyTwice function takes a function f and a value x of type
α and applies the function f twice to the value x. This higher-order function
allows for the composition of functions by applying a function multiple times.
Similarly, higher order functions can be used to define functions that return functions as results. For example:
def addN : Nat → Nat → Nat := λ n => λ x => x + nThe addN function takes a number n and returns a function that adds n to a
number. This higher-order function allows for the creation of specialized functions that add a specific number to
values.
Filtering functions are another example of higher-order functions. Here’s an example of a filter
function that takes a predicate function and a list and returns a new list containing only the elements that satisfy the
predicate:
def filter {α : Type} (p : α → Bool) : List α → List α
| [], _ => []
| x::xs, p => if p x then x :: filter p xs else filter p xsThe filter function takes a predicate function p that maps values of type α to
booleans, a list of values of type α, and returns a new list containing only the elements that satisfy the
predicate p. This higher-order function allows for the selective extraction of elements from a list based
on a condition.