Functions

Functions are the fundamental unit of program execution in any programming language. As in other languages, a Lean function has a name, can have parameters and take arguments, and has a body. Lean also supports functional programming constructs such as treating functions as values, using unnamed functions in expressions, composition of functions to form new functions, curried functions, and the implicit definition of functions by way of the partial application of function arguments.

You define functions by using the def keyword followed by its name, a parameter list, return type and its body. The parameter list consists of successive parameters that are separated by spaces. You can specify an explicit type for each parameter. If you do not specify a specific argument type, the compiler tries to infer the type from the function body. An error is returned when it cannot be inferred. The expression that makes up the function body is typically a compound expression consisting of a number of expressions that culminate in a final expression that is the return value. The return type is a colon followed by a type and is optional. If you do not specify the type of the return value explicitly, the compiler tries to determine the return type from the final expression.

def f x := x + 1

In the previous example, the function name is f, the argument is x, which has type Nat, the function body is x + 1, and the return value is of type Nat. The following example defines the factorial recursive function using pattern matching.

def fact x :=
  match x with
  | 0   => 1
  | n+1 => (n+1) * fact n

#eval fact 100

By default, Lean only accepts total functions. The partial keyword may be used to define a recursive function without a termination proof; partial functions compute in compiled programs, but are opaque in proofs and during type checking.

partial def g (x : Nat) (p : Nat -> Bool) : Nat :=
  if p x then
    x
  else
    g (x+1) p

#eval g 0 (fun x => x > 10)

In the previous example, g x p only terminates if there is a y >= x such that p y returns true. Of course, g 0 (fun x => false) never terminates.

However, the use of partial is restricted to functions whose return type is not empty so the soundness of the system is not compromised.

partial def loop? : α := -- failed to compile partial definition 'loop?', failed to
  loop?                  -- show that type is inhabited and non empty

partial def loop [Inhabited α] : α := -- compiles
  loop

example : True := -- accepted
  loop

example : False :=
  loop -- failed to synthesize instance Inhabited False

If we were able to partially define loop?, we could prove False with it.

Lambda expressions

A lambda expression is an unnamed function. You define lambda expressions by using the fun keyword. A lambda expression resembles a function definition, except that instead of the := token, the => token is used to separate the argument list from the function body. As in a regular function definition, the argument types can be inferred or specified explicitly, and the return type of the lambda expression is inferred from the type of the last expression in the body.

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

#eval twice (fun x => x + 1) 3
#eval twice (fun (x : Nat) => x * 2) 3

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

#eval List.map (fun (x, y) => x + y) [(1, 2), (3, 4)]
-- [3, 7]

Syntax sugar for simple lambda expressions

Simple functions can be defined using parentheses and · as a placeholder.

#check (· + 1)
-- fun a => a + 1
#check (2 - ·)
-- fun a => 2 - a
#eval [1, 2, 3, 4, 5].foldl (· * ·) 1
-- 120

def h (x y z : Nat) :=
  x + y + z

#check (h · 1 ·)
-- fun a b => h a 1 b

#eval [(1, 2), (3, 4), (5, 6)].map (·.1)
-- [1, 3, 5]

In the previous example, the term (·.1) is syntax sugar for fun x => x.1.

Pipelining

Pipelining enables function calls to be chained together as successive operations. Pipelining works as follows:

def add1 x := x + 1
def times2 x := x * 2

#eval times2 (add1 100)
#eval 100 |> add1 |> times2
#eval times2 <| add1 <| 100

The result of the previous #eval commands is 202. The forward pipeline |> operator takes a function and an argument and return a value. In contrast, the backward pipeline <| operator takes an argument and a function and returns a value. These operators are useful for minimizing the number of parentheses.

def add1Times3FilterEven (xs : List Nat) :=
  List.filter (· % 2 == 0) (List.map (· * 3) (List.map (· + 1) xs))

#eval add1Times3FilterEven [1, 2, 3, 4]
-- [6, 12]

-- Define the same function using pipes
def add1Times3FilterEven' (xs : List Nat) :=
  xs |> List.map (· + 1) |> List.map (· * 3) |> List.filter (· % 2 == 0)

#eval add1Times3FilterEven' [1, 2, 3, 4]
-- [6, 12]

Lean also supports the operator |>. which combines forward pipeline |> operator with the . field notation.

-- Define the same function using pipes
def add1Times3FilterEven'' (xs : List Nat) :=
  xs.map (· + 1) |>.map (· * 3) |>.filter (· % 2 == 0)

#eval add1Times3FilterEven'' [1, 2, 3, 4]
-- [6, 12]

For users familiar with the Haskell programming language, Lean also supports the notation f $ a for the backward pipeline f <| a.