# 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.

```lean id="z4ud6k"
#check fun x : Nat => x + 1
```

Lean reports:

```text id="g2d9vc"
fun x => x + 1 : Nat -> Nat
```

Apply the function by writing the argument after it:

```lean id="9rv5kn"
#eval (fun x : Nat => x + 1) 5
```

Expected result:

```text id="lw4dfn"
6
```

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

```lean id="ow1j3w"
def addOne : Nat -> Nat :=
  fun x => x + 1

#eval addOne 5
```

## Function Types

The type:

```lean id="tddwf5"
Nat -> Nat
```

means a function from natural numbers to natural numbers.

A function with two arguments has a curried type:

```lean id="r7pcfh"
Nat -> Nat -> Nat
```

This associates to the right:

```lean id="7ty3m5"
Nat -> (Nat -> Nat)
```

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

```lean id="49wypu"
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:

```lean id="aowz89"
def add' : Nat -> Nat -> Nat :=
  fun x y => x + y
```

This is syntactic sugar for nested lambdas:

```lean id="7pmt3q"
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:

```lean id="qpjbiw"
def addNamed (x y : Nat) : Nat :=
  x + y
```

This is equivalent in ordinary use to:

```lean id="okb6au"
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.

```lean id="9phvmz"
addNamed 1 2
```

means:

```lean id="ff80rx"
(addNamed 1) 2
```

This matters when functions are returned by other functions.

```lean id="dxrkgh"
def makeAdder (x : Nat) : Nat -> Nat :=
  fun y => x + y

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

Both evaluations return:

```text id="nq92yx"
15
```

## Higher-Order Functions

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

```lean id="34d8vz"
def applyTwice (f : Nat -> Nat) (x : Nat) : Nat :=
  f (f x)

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

Expected result:

```text id="bs5t79"
12
```

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

```lean id="qj8d51"
#eval applyTwice (fun x => x * 2) 10
```

Expected result:

```text id="ixkfy5"
40
```

## Polymorphic Functions

A function can work over any type.

```lean id="5aq3d9"
def idExplicit (α : Type) (x : α) : α :=
  x
```

Using implicit type arguments is more convenient:

```lean id="y3sqzg"
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.

```lean id="896h6w"
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:

```lean id="n51lhx"
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.

```lean id="ss4fzf"
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:

```lean id="f2x54h"
(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.

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

Expected result:

```text id="z32png"
[2, 3, 4]
```

Filtering uses a function returning `Bool`:

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

Expected result:

```text id="7oopxu"
[2, 4, 6]
```

## Partial Application

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

```lean id="kvoen5"
def addTen : Nat -> Nat :=
  addNamed 10

#eval addTen 7
```

Expected result:

```text id="um2p7g"
17
```

This is often cleaner than writing:

```lean id="k0e6lw"
def addTen' : Nat -> Nat :=
  fun x => addNamed 10 x
```

Both definitions are equivalent in behavior.

## Function Composition

Function composition can be written directly:

```lean id="5doeq4"
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:

```text id="lmf6xp"
21
```

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.

```lean id="aegh3s"
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.

```lean id="rftd0t"
fun x : Nat => x + 1
```

If application groups incorrectly, add parentheses.

```lean id="t1f4y2"
(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.

```lean id="2bz43c"
#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`.