Additional Conveniences

Lean contains a number of convenience features that make programs much more concise.

Automatic Implicit Arguments

When writing polymorphic functions in Lean, it is typically not necessary to list all the implicit arguments. Instead, they can simply be mentioned. If Lean can determine their type, then they are automatically inserted as implicit arguments. In other words, the previous definition of length:

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

can be written without {α : Type}:

def length (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

This can greatly simplify highly polymorphic definitions that take many implicit arguments.

Pattern-Matching Definitions

When defining functions with def, it is quite common to name an argument and then immediately use it with pattern matching. For instance, in length, the argument xs is used only in match. In these situations, the cases of the match expression can be written directly, without naming the argument at all.

The first step is to move the arguments' types to the right of the colon, so the return type is a function type. For instance, the type of length is List α → Nat. Then, replace the := with each case of the pattern match:

def length : List α → Nat
  | [] => 0
  | y :: ys => Nat.succ (length ys)

This syntax can also be used to define functions that take more than one argument. In this case, their patterns are separated by commas. For instance, drop takes a number $ n $ and a list, and returns the list after removing the first $ n $ entries.

def drop : Nat → List α → List α
  | Nat.zero, xs => xs
  | _, [] => []
  | Nat.succ n, x :: xs => drop n xs

Named arguments and patterns can also be used in the same definition. For instance, a function that takes a default value and an optional value, and returns the default when the optional value is none, can be written:

def fromOption (default : α) : Option α → α
  | none => default
  | some x => x

This function is called Option.getD in the standard library, and can be called with dot notation:

#eval (some "salmonberry").getD ""

"salmonberry"

#eval none.getD ""

""

Local Definitions

It is often useful to name intermediate steps in a computation. In many cases, intermediate values represent useful concepts all on their own, and naming them explicitly can make the program easier to read. In other cases, the intermediate value is used more than once. As in most other languages, writing down the same code twice in Lean causes it to be computed twice, while saving the result in a variable leads to the result of the computation being saved and re-used.

For instance, unzip is a function that transforms a list of pairs into a pair of lists. When the list of pairs is empty, then the result of unzip is a pair of empty lists. When the list of pairs has a pair at its head, then the two fields of the pair are added to the result of unzipping the rest of the list. This definition of unzip follows that description exactly:

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    (x :: (unzip xys).fst, y :: (unzip xys).snd)

Unfortunately, there is a problem: this code is slower than it needs to be. Each entry in the list of pairs leads to two recursive calls, which makes this function take exponential time. However, both recursive calls will have the same result, so there is no reason to make the recursive call twice.

In Lean, the result of the recursive call can be named, and thus saved, using let. Local definitions with let resemble top-level definitions with def: it takes a name to be locally defined, arguments if desired, a type signature, and then a body following :=. After the local definition, the expression in which the local definition is available (called the body of the let-expression) must be on a new line, starting at a column in the file that is less than or equal to that of the let keyword. For instance, let can be used in unzip like this:

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped : List α × List β := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

To use let on a single line, separate the local definition from the body with a semicolon.

Local definitions with let may also use pattern matching when one pattern is enough to match all cases of a datatype. In the case of unzip, the result of the recursive call is a pair. Because pairs have only a single constructor, the name unzipped can be replaced with a pair pattern:

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let (xs, ys) : List α × List β := unzip xys
    (x :: xs, y :: ys)

Judicious use of patterns with let can make code easier to read, compared to writing the accessor calls by hand.

The biggest difference between let and def is that recursive let definitions must be explicitly indicated by writing let rec. For instance, one way to reverse a list involves a recursive helper function, as in this definition:

def reverse (xs : List α) : List α :=
  let rec helper : List α → List α → List α
    | [], soFar => soFar
    | y :: ys, soFar => helper ys (y :: soFar)
  helper xs []

The helper function walks down the input list, moving one entry at a time over to soFar. When it reaches the end of the input list, soFar contains a reversed version of the input.

Type Inference

In many situations, Lean can automatically determine an expression's type. In these cases, explicit types may be omitted from both top-level definitions (with def) and local definitions (with let). For instance, the recursive call to unzip does not need an annotation:

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

As a rule of thumb, omitting the types of literal values (like strings and numbers) usually works, although Lean may pick a type for literal numbers that is more specific than the intended type. Lean can usually determine a type for a function application, because it already knows the argument types and the return type. Omitting return types for function definitions will often work, but function arguments typically require annotations. Definitions that are not functions, like unzipped in the example, do not need type annotations if their bodies do not need type annotations, and the body of this definition is a function application.

Omitting the return type for unzip is possible when using an explicit match expression:

def unzip (pairs : List (α × β)) :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

Generally speaking, it is a good idea to err on the side of too many, rather than too few, type annotations. First off, explicit types communicate assumptions about the code to readers. Even if Lean can determine the type on its own, it can still be easier to read code without having to repeatedly query Lean for type information. Secondly, explicit types help localize errors. The more explicit a program is about its types, the more informative the error messages can be. This is especially important in a language like Lean that has a very expressive type system. Thirdly, explicit types make it easier to write the program in the first place. The type is a specification, and the compiler's feedback can be a helpful tool in writing a program that meets the specification. Finally, Lean's type inference is a best-effort system. Because Lean's type system is so expressive, there is no "best" or most general type to find for all expressions. This means that even if you get a type, there's no guarantee that it's the right type for a given application. For instance, 14 can be a Nat or an Int:

#check 14

14 : Nat

#check (14 : Int)

14 : Int

Missing type annotations can give confusing error messages. Omitting all types from the definition of unzip:

def unzip pairs :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

leads to a message about the match expression:

invalid match-expression, pattern contains metavariables
  []

This is because match needs to know the type of the value being inspected, but that type was not available. A "metavariable" is an unknown part of a program, written ?m.XYZ in error messages—they are described in the section on Polymorphism. In this program, the type annotation on the argument is required.

Even some very simple programs require type annotations. For instance, the identity function just returns whatever argument it is passed. With argument and type annotations, it looks like this:

def id (x : α) : α := x

Lean is capable of determining the return type on its own:

def id (x : α) := x

Omitting the argument type, however, causes an error:

def id x := x

failed to infer binder type

In general, messages that say something like "failed to infer" or that mention metavariables are often a sign that more type annotations are necessary. Especially while still learning Lean, it is useful to provide most types explicitly.

Simultaneous Matching

Pattern-matching expressions, just like pattern-matching definitions, can match on multiple values at once. Both the expressions to be inspected and the patterns that they match against are written with commas between them, similarly to the syntax used for definitions. Here is a version of drop that uses simultaneous matching:

def drop (n : Nat) (xs : List α) : List α :=
  match n, xs with
  | Nat.zero, ys => ys
  | _, [] => []
  | Nat.succ n , y :: ys => drop n ys

Natural Number Patterns

In the section on datatypes and patterns, even was defined like this:

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

Just as there is special syntax to make list patterns more readable than using List.cons and List.nil directly, natural numbers can be matched using literal numbers and +. For instance, even can also be defined like this:

def even : Nat → Bool
  | 0 => true
  | n + 1 => not (even n)

In this notation, the arguments to the + pattern serve different roles. Behind the scenes, the left argument (n above) becomes an argument to some number of Nat.succ patterns, and the right argument (1 above) determines how many Nat.succs to wrap around the pattern. The explicit patterns in halve, which divides a Nat by two and drops the remainder:

def halve : Nat → Nat
  | Nat.zero => 0
  | Nat.succ Nat.zero => 0
  | Nat.succ (Nat.succ n) => halve n + 1

can be replaced by numeric literals and +:

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | n + 2 => halve n + 1

Behind the scenes, both definitions are completely equivalent. Remember: halve n + 1 is equivalent to (halve n) + 1, not halve (n + 1).

When using this syntax, the second argument to + should always be a literal Nat. Even though addition is commutative, flipping the arguments in a pattern can result in errors like the following:

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | 2 + n => halve n + 1

invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 2 n)

This restriction enables Lean to transform all uses of the + notation in a pattern into uses of the underlying Nat.succ, keeping the language simpler behind the scenes.

Anonymous Functions

Functions in Lean need not be defined at the top level. As expressions, functions are produced with the fun syntax. Function expressions begin with the keyword fun, followed by one or more arguments, which are separated from the return expression using =>. For instance, a function that adds one to a number can be written:

#check fun x => x + 1

fun x => x + 1 : Nat → Nat

Type annotations are written the same way as on def, using parentheses and colons:

#check fun (x : Int) => x + 1

fun x => x + 1 : Int → Int

Similarly, implicit arguments may be written with curly braces:

#check fun {α : Type} (x : α) => x

fun {α} x => x : {α : Type} → α → α

This style of anonymous function expression is often referred to as a lambda expression, because the typical notation used in mathematical descriptions of programming languages uses the Greek letter λ (lambda) where Lean has the keyword fun. Even though Lean does permit λ to be used instead of fun, it is most common to write fun.

Anonymous functions also support the multiple-pattern style used in def. For instance, a function that returns the predecessor of a natural number if it exists can be written:

#check fun
  | 0 => none
  | n + 1 => some n

fun x =>
  match x with
  | 0 => none
  | Nat.succ n => some n : Nat → Option Nat

Note that Lean's own description of the function has a named argument and a match expression. Many of Lean's convenient syntactic shorthands are expanded to simpler syntax behind the scenes, and the abstraction sometimes leaks.

Definitions using def that take arguments may be rewritten as function expressions. For instance, a function that doubles its argument can be written as follows:

def double : Nat → Nat := fun
  | 0 => 0
  | k + 1 => double k + 2

When an anonymous function is very simple, like fun x => x + 1, the syntax for creating the function can be fairly verbose. In that particular example, six non-whitespace characters are used to introduce the function, and its body consists of only three non-whitespace characters. For these simple cases, Lean provides a shorthand. In an expression surrounded by parentheses, a centered dot character · can stand for an argument, and the expression inside the parentheses becomes the function's body. That particular function can also be written (· + 1).

The centered dot always creates a function out of the closest surrounding set of parentheses. For instance, (· + 5, 3) is a function that returns a pair of numbers, while ((· + 5), 3) is a pair of a function and a number. If multiple dots are used, then they become arguments from left to right:

(· , ·) 1 2
===>
(1, ·) 2
===>
(1, 2)

Anonymous functions can be applied in precisely the same way as functions defined using def or let. The command #eval (fun x => x + x) 5 results in:

while #eval (· * 2) 5 results in:

Namespaces

Each name in Lean occurs in a namespace, which is a collection of names. Names are placed in namespaces using ., so List.map is the name map in the List namespace. Names in different namespaces do not conflict with each other, even if they are otherwise identical. This means that List.map and Array.map are different names. Namespaces may be nested, so Project.Frontend.User.loginTime is the name loginTime in the nested namespace Project.Frontend.User.

Names can be directly defined within a namespace. For instance, the name double can be defined in the Nat namespace:

def Nat.double (x : Nat) : Nat := x + x

Because Nat is also the name of a type, dot notation is available to call Nat.double on expressions with type Nat:

#eval (4 : Nat).double

In addition to defining names directly in a namespace, a sequence of declarations can be placed in a namespace using the namespace and end commands. For instance, this defines triple and quadruple in the namespace NewNamespace:

namespace NewNamespace
def triple (x : Nat) : Nat := 3 * x
def quadruple (x : Nat) : Nat := 2 * x + 2 * x
end NewNamespace

To refer to them, prefix their names with NewNamespace.:

#check NewNamespace.triple

NewNamespace.triple (x : Nat) : Nat

#check NewNamespace.quadruple

NewNamespace.quadruple (x : Nat) : Nat

Namespaces may be opened, which allows the names in them to be used without explicit qualification. Writing open MyNamespace in before an expression causes the contents of MyNamespace to be available in the expression. For example, timesTwelve uses both quadruple and triple after opening NewNamespace:

def timesTwelve (x : Nat) :=
  open NewNamespace in
  quadruple (triple x)

Namespaces can also be opened prior to a command. This allows all parts of the command to refer to the contents of the namespace, rather than just a single expression. To do this, place the open ... in prior to the command.

open NewNamespace in
#check quadruple

NewNamespace.quadruple (x : Nat) : Nat

Function signatures show the name's full namespace. Namespaces may additionally be opened for all following commands for the rest of the file. To do this, simply omit the in from a top-level usage of open.

if let

When consuming values that have a sum type, it is often the case that only a single constructor is of interest. For instance, given this type that represents a subset of Markdown inline elements:

inductive Inline : Type where
  | lineBreak
  | string : String → Inline
  | emph : Inline → Inline
  | strong : Inline → Inline

a function that recognizes string elements and extracts their contents can be written:

def Inline.string? (inline : Inline) : Option String :=
  match inline with
  | Inline.string s => some s
  | _ => none

An alternative way of writing this function's body uses if together with let:

def Inline.string? (inline : Inline) : Option String :=
  if let Inline.string s := inline then
    some s
  else none

This is very much like the pattern-matching let syntax. The difference is that it can be used with sum types, because a fallback is provided in the else case. In some contexts, using if let instead of match can make code easier to read.

Positional Structure Arguments

The section on structures presents two ways of constructing structures:

The constructor can be called directly, as in Point.mk 1 2.
Brace notation can be used, as in { x := 1, y := 2 }.

In some contexts, it can be convenient to pass arguments positionally, rather than by name, but without naming the constructor directly. For instance, defining a variety of similar structure types can help keep domain concepts separate, but the natural way to read the code may treat each of them as being essentially a tuple. In these contexts, the arguments can be enclosed in angle brackets ⟨ and ⟩. A Point can be written ⟨1, 2⟩. Be careful! Even though they look like the less-than sign < and greater-than sign >, these brackets are different. They can be input using \< and \>, respectively.

Just as with the brace notation for named constructor arguments, this positional syntax can only be used in a context where Lean can determine the structure's type, either from a type annotation or from other type information in the program. For instance, #eval ⟨1, 2⟩ yields the following error:

invalid constructor ⟨...⟩, expected type must be an inductive type 
  ?m.34991

The metavariable in the error is because there is no type information available. Adding an annotation, such as in #eval (⟨1, 2⟩ : Point), solves the problem:

{ x := 1.000000, y := 2.000000 }

String Interpolation

In Lean, prefixing a string with s! triggers interpolation, where expressions contained in curly braces inside the string are replaced with their values. This is similar to f-strings in Python and $-prefixed strings in C#. For instance,

#eval s!"three fives is {NewNamespace.triple 5}"

yields the output

"three fives is 15"

Not all expressions can be interpolated into a string. For instance, attempting to interpolate a function results in an error.

#check s!"three fives is {NewNamespace.triple}"

yields the output

failed to synthesize instance
  ToString (Nat → Nat)

This is because there is no standard way to convert functions into strings. The Lean compiler maintains a table that describes how to convert values of various types into strings, and the message failed to synthesize instance means that the Lean compiler didn't find an entry in this table for the given type. This uses the same language feature as the deriving Repr syntax that was described in the section on structures.

Functional Programming in Lean