3.1. Functions🔗

Function types are a built-in feature of Lean. Functions map the values of one type (the domain) into those of another type (the range), and function types specify the domain and range of functions.

There are two kinds of function type:

Dependent: Dependent function types explicitly name the parameter, and the function's range may refer explicitly to this name. Because types can be computed from values, a dependent function may return values from any number of different types, depending on its argument.Dependent functions are sometimes referred to as dependent products, because they correspond to an indexed product of sets.
Non-Dependent: Non-dependent function types do not include a name for the parameter, and the range does not vary based on the specific argument provided.

Dependent Function Types

The function two returns values in different types, depending on which argument it is called with:

def two : (b : Bool) → if b then Unit × Unit else String :=
  fun b =>
    match b with
    | true => ((), ())
    | false => "two"

The body of the function cannot be written with if...then...else... because it does not refine types the same way that Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match does.

In Lean's core language, all function types are dependent: non-dependent function types are dependent function types in which the parameter name does not occur in the range. Additionally, two dependent function types that have different parameter names may be definitionally equal if renaming the parameter makes them equal. However, the Lean elaborator does not introduce a local binding for non-dependent functions' parameters.

Definitional Equality of Dependent and Non-Dependent Functions

The types (x : Nat) → String and Nat → String are definitionally equal:

example : ((x : Nat) → String) = (Nat → String) := rfl

Similarly, the types (n : Nat) → n + 1 = 1 + n and (k : Nat) → k + 1 = 1 + k are definitionally equal:

example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) := rfl

Non-Dependent Functions Don't Bind Variables

A dependent function is required in the following statement that all elements of an array are non-zero:

def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0

This is because the elaborator for array access requires a proof that the index is in bounds. The non-dependent version of the statement does not introduce this assumption:

def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (i < xs.size) → failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
xs : Array Nat
i : Nat
⊢ i < xs.sizexs[i] ≠ 0

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
xs : Array Nat
i : Nat
⊢ i < xs.size

While the core type theory does not feature implicit parameters, function types do include an indication of whether the parameter is implicit. This information is used by the Lean elaborator, but it does not affect type checking or definitional equality in the core theory and can be ignored when thinking only about the core type theory.

Definitional Equality of Implicit and Explicit Function Types

The types {α : Type} → (x : α) → α and (α : Type) → (x : α) → α are definitionally equal, even though the first parameter is implicit in one and explicit in the other.

example :
    ({α : Type} → (x : α) → α)
    =
    ((α : Type) → (x : α) → α)
  := rfl

3.1.1. Function Abstractions

In Lean's type theory, functions are created using function abstractions that bind a variable. In various communities, function abstractions are also known as lambdas, due to Alonzo Church's notation for them, or anonymous functions because they don't need to be defined with a name in the global environment. When the function is applied, the result is found by β-reduction: substituting the argument for the bound variable. In compiled code, this happens strictly: the argument must already be a value. When type checking, there are no such restrictions; the equational theory of definitional equality allows β-reduction with any term.

In Lean's term language, function abstractions may take multiple parameters or use pattern matching. These features are translated to simpler operations in the core language, where all functions abstractions take exactly one parameter. Not all functions originate from abstractions: type constructors, constructors, and recursors may have function types, but they cannot be defined using function abstractions alone.

3.1.2. Currying🔗

In Lean's core type theory, every function maps each element of the domain to a single element of the range. In other words, every function expects exactly one parameter. Multiple-parameter functions are implemented by defining higher-order functions that, when supplied with the first parameter, return a new function that expects the remaining parameters. This encoding is called currying, popularized by and named after Haskell B. Curry. Lean's syntax for defining functions, specifying their types, and applying them creates the illusion of multiple-parameter functions, but the result of elaboration contains only single-parameter functions.

3.1.3. Extensionality🔗

Definitional equality of functions in Lean is intensional. This means that definitional equality is defined syntactically, modulo renaming of bound variables and reduction. To a first approximation, this means that two functions are definitionally equal if they implement the same algorithm, rather than the usual mathematical notion of equality that states that two functions are equal if they map equal elements of the domain to equal elements of the range.

Definitional equality is used by the type checker, so it's important that it be predictable. The syntactic character of intensional equality means that the algorithm to check it can be feasibly specified. Checking extensional equality involves proving essentially arbitrary theorems about equality of functions, and there is no clear specification for an algorithm to check it. This makes extensional equality a poor choice for a type checker. Function extensionality is instead made available as a reasoning principle that can be invoked when proving the proposition that two functions are equal.

In addition to reduction and renaming of bound variables, definitional equality does support one limited form of extensionality, called η-equivalence, in which functions are equal to abstractions whose bodies apply them to the argument. Given f with type (x : α) → β x, f is definitionally equal to fun x => f x.

When reasoning about functions, the theorem funextUnlike some intensional type theories, funext is a theorem in Lean. It can be proved using quotient types. or the corresponding tactics funext or ext can be used to prove that two functions are equal if they map equal inputs to equal outputs.

funext.{u, v} {α : Sort u} {β : α → Sort v}
    {f g : (x : α) → β x}
    (h : ∀ (x : α), f x = g x) : f = g

Function extensionality is the statement that if two functions take equal values every point, then the functions themselves are equal: (∀ x, f x = g x) → f = g. It is called "extensionality" because it talks about how to prove two objects are equal based on the properties of the object (compare with set extensionality, which is (∀ x, x ∈ s ↔ x ∈ t) → s = t).

This is often an axiom in dependent type theory systems, because it cannot be proved from the core logic alone. However in lean's type theory this follows from the existence of quotient types (note the Quot.sound in the proof, as well as the show line which makes use of the definitional equality Quot.lift f h (Quot.mk x) = f x).

3.1.4. Totality and Termination🔗

Functions can be defined recursively using Lean.Parser.Command.declaration : commanddef. From the perspective of Lean's logic, all functions are total, meaning that they map each element of the domain to an element of the range in finite time.Some programming language communities use the term total in a different sense, where functions are considered total if they do not crash due to unhandled cases but non-termination is ignored. The values of total functions are defined for all type-correct arguments, and they cannot fail to terminate or crash due to a missing case in a pattern match.

While the logical model of Lean considers all functions to be total, Lean is also a practical programming language that provides certain "escape hatches". Functions that have not been proven to terminate can still be used in Lean's logic as long as their range is proven nonempty. These functions are treated as uninterpreted functions by Lean's logic, and their computational behavior is ignored. In compiled code, these functions are treated just like any others. Other functions may be marked unsafe; these functions are not available to Lean's logic at all. The section on partial and unsafe function definitions contains more detail on programming with recursive functions.

Similarly, operations that should fail at runtime in compiled code, such as out-of-bounds access to an array, can only be used when the resulting type is known to be inhabited. These operations result in an arbitrarily chosen inhabitant of the type in Lean's logic (specifically, the one specified in the type's Inhabited instance).

Panic

The function thirdChar extracts the third element of an array, or panics if the array has two or fewer elements:

def thirdChar (xs : Array Char) : Char := xs[2]!

The (nonexistent) third elements of #['!'] and #['-', 'x'] are equal, because they result in the same arbitrarily-chosen character:

example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl

Indeed, both are equal to 'A', which happens to be the default fallback for Char:

example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl