From a1c52ae1c42dc5e87a88a6ebb26af496b78c05a5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2020 12:48:51 -0800 Subject: [PATCH] doc: expand `functions.md` --- doc/SUMMARY.md | 6 +- doc/functions.md | 136 ++++++++++++++++++++++++++++++++++++++++++++ doc/lean3changes.md | 2 +- 3 files changed, 142 insertions(+), 2 deletions(-) diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 99bcf18109..cd4ad7e3ff 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -2,11 +2,11 @@ - [What is Lean](./whatIsLean.md) - [Tour of Lean](./tour.md) -- [Frequently Asked Questions](./faq.md) # Language Manual - [Significant Changes from Lean 3](./lean3changes.md) +- [Functions](./functions.md) - [String interpolation](./stringinterp.md) - [The `do` Notation]() @@ -23,3 +23,7 @@ - [Windows Setup](./make/msys2.md) - [Building This Manual](./mdbook.md) - [Fixing Tests](./fixing_tests.md) + +# Other + +- [Frequently Asked Questions](./faq.md) diff --git a/doc/functions.md b/doc/functions.md index 0c5faf50f8..43d27f7c15 100644 --- a/doc/functions.md +++ b/doc/functions.md @@ -1 +1,137 @@ # 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. + +```lean +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. +```lean +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 should be used when Lean cannot +establish that a function always terminates. +```lean +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. + +# 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. + +```lean +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 `.` (or `·`) as a placeholder. +```lean +#check (. + 1) +-- fun a => a + 1 +#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`. Note that, the ASCII version `(..1)` +is not supported because `..` is a reserved symbol. + +# Pipelining + +Pipelining enables function calls to be chained together as successive operations. Pipelining works as follows: + +```lean +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 `|>` operatior takes a function and an argument and return a value. +In constrat, the backward pipeline `<|` operator takes an argument and a function and returns a value. +These operators are useful for minimizing the number of parentheses. +```lean +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. +```lean +-- 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`. diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 24dadbb41c..c6f68b22f1 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -84,7 +84,7 @@ def id5 : {α : Type} → α → α := * Sugar for simple functions -In Lean 3, we can creating simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` as a placeholder. Here are a few examples: +In Lean 3, we can creating simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples: ```lean # namespace ex3