Functional Programming in Lean
by David Thrane Christiansen
This is an inprogress book on using Lean 4 as a programming language.
The most recent release is found at https://leanprover.github.io/functional_programming_in_lean/, and it will be updated monthly.
This version of the text is written for Lean 4 release nightly20221126
.
Release history
November, 2022
This release adds a chapter on programming with monads. Additionally, the example of using JSON in the coercions section has been updated to include the complete code.
October, 2022
This release completes the chapter on type classes. In addition, a short interlude introducing propositions, proofs, and tactics has been added just before the chapter on type classes, because a small amount of familiarity with the concepts helps to understand some of the standard library type classes.
September, 2022
This release adds the first half of a chapter on type classes, which are Lean's mechanism for overloading operators and an important means of organizing code and structuring libraries. Additionally, the second chapter has been updated to account for changes in Lean's stream API.
August, 2022
This third public release adds a second chapter, which describes compiling and running programs along with Lean's model for side effects.
July, 2022
The second public release completes the first chapter.
June, 2022
This was the first public release, consisting of an introduction and part of the first chapter.
About the Author
David Thrane Christiansen has been using functional languages for twenty years, and dependent types for ten. Together with Daniel P. Friedman, he wrote The Little Typer, an introduction to the key ideas of dependent type theory. He has a Ph.D. from the IT University of Copenhagen. During his studies, he was a major contributor to the first version of the Idris language. Since leaving academia, he has worked at Galois in Portland, Oregon and Deon Digital in Copenhagen, Denmark. At the time of writing, he is the Executive Director of the Haskell Foundation.
Lean is an interactive theorem prover developed at Microsoft Research, based on dependent type theory. Dependent type theory unites the worlds of programs and proofs; thus, Lean is also a programming language. Lean takes its dual nature seriously, and it is designed to be suitable for use as a generalpurpose programming language—Lean is even implemented in itself. This book is about writing programs in Lean.
When viewed as a programming language, Lean is a strict pure functional language with dependent types. A large part of learning to program with Lean consists of learning how each of these attributes affects the way programs are written, and how to think like a functional programmer. Strictness means that function calls in Lean work similarly to the way they do in most languages: the arguments are fully computed before the function's body begins running. Purity means that Lean programs cannot have side effects such as modifying locations in memory, sending emails, or deleting files without the program's type saying so. Lean is a functional language in the sense that functions are firstclass values like any other and that the execution model is inspired by the evaluation of mathematical expressions. Dependent types, which are the most unusual feature of Lean, make types into a firstclass part of the language, allowing types to contain programs and programs to compute types.
This book is intended for programmers who want to learn Lean, but who have not necessarily used a functional programming language before. Familiarity with functional languages such as Haskell, OCaml, or F# is not required. On the other hand, this book does assume knowledge of concepts like loops, functions, and data structures that are common to most programming languages. While this book is intended to be a good first book on functional programming, it is not a good first book on programming in general.
Mathematicians who are using Lean as a proof assistant will likely need to write custom proof automation tools at some point. This book is also for them. As these tools become more sophisticated, they begin to resemble programs in functional languages, but most working mathematicians are trained in languages like Python and Mathematica. This book can help bridge the gap, empowering more mathematicians to write maintainable and understandable proof automation tools.
This book is intended to be read linearly, from the beginning to the end. Concepts are introduced one at a time, and later sections assume familiarity with earlier sections. Sometimes, later chapters will go into depth on a topic that was only briefly addressed earlier on. Some sections of the book contain exercises. These are worth doing, in order to cement your understanding of the section. It is also useful to explore Lean as you read the book, finding creative new ways to use what you have learned.
Getting Lean
Before writing and running programs written in Lean, you'll need to set up Lean on your own computer. The Lean tooling consists of the following:
elan
manages the Lean compiler toolchains, similarly torustup
orghcup
.lake
builds Lean packages and their dependencies, similarly tocargo
,make
, or Gradle.lean
type checks and compiles individual Lean files as well as providing information to programmer tools about files that are currently being written. Normally,lean
is invoked by other tools rather than directly by users. Plugins for editors, such as Visual Studio Code or Emacs, that communicate with
lean
and present its information conveniently.
Please refer to the Lean manual for uptodate instructions for installing Lean.
Typographical Conventions
Code examples that are provided to Lean as input are formatted like this:
def add1 (n : Nat) : Nat := n + 1
#eval add1 7
The last line above (beginning with #eval
) is a command that instructs Lean to calculate an answer.
Lean's replies are formatted like this:
8
Error messages returned by Lean are formatted like this:
application type mismatch
add1 "seven"
argument
"seven"
has type
String : Type
but is expected to have type
Nat : Type
Unicode
Idiomatic Lean code makes use of a variety of Unicode characters that are not part of ASCII.
For instance, Greek letters like α
and β
and the arrow →
both occur in the first chapter of this book.
This allows Lean code to more closely resemble ordinary mathematical notation.
With the default Lean settings, both Visual Studio Code and Emacs allow these characters to be typed with a backslash (\
) followed by a name.
For example, to enter α
, type \alpha
.
To find out how to type a character in Visual Studio Code, point the mouse at it and look at the tooltip.
In Emacs, use Cc Ck
with point on the character in question.
According to tradition, a programming language should be introduced by
compiling and running a program that displays "Hello, world!"
on the
console. This simple program ensures that the language tooling is
installed correctly and that the programmer is able to run the
compiled code.
Since the 1970s, however, programming has changed. Today, compilers are typically integrated into text editors, and the programming environment offers feedback as the program is written. Lean is no exception: it implements an extended version of the Language Server Protocol that allows it to communicate with a text editor and provide feedback as the user types.
Languages as varied as Python, Haskell, and JavaScript offer a readevalprintloop (REPL), also known as an interactive toplevel or a browser console, in which expressions or statements can be entered. The language then computes and displays the result of the user's input. Lean, on the other hand, integrates these features into the interaction with the editor, providing commands that cause the text editor to display feedback integrated into the program text itself. This chapter provides a short introduction to interacting with Lean in an editor, while Hello, World! describes how to use Lean traditionally from the command line in batch mode.
It is best if you read this book with Lean open in your editor, following along and typing in each example. Please play with the examples, and see what happens!
Evaluating Expressions
The most important thing to understand as a programmer learning Lean is how evaluation works. Evaluation is the process of finding the value of an expression, just as one does in arithmetic. For instance, the value of 15  6 is 9 and the value of 2 × (3 + 1) is 8. To find the value of the latter expression, 3 + 1 is first replaced by 4, yielding 2 × 4, which itself can be reduced to 8. Sometimes, mathematical expressions contain variables: the value of x + 1 cannot be computed until we know what the value of x is. In Lean, programs are first and foremost expressions, and the primary way to think about computation is as evaluating expressions to find their values.
Most programming languages are imperative, where a program consists of a series of statements that should be carried out in order to find the program's result. Programs have access to mutable memory, so the value referred to by a variable can change over time. In addition to mutable state, programs may have other side effects, such as deleting files, making outgoing network connections, throwing or catching exceptions, and reading data from a database. "Side effects" is essentially a catchall term for describing things that may happen in a program that don't follow the model of evaluating mathematical expressions.
In Lean, however, programs work the same way as mathematical
expressions. Once given a value, variables cannot be reassigned. Evaluating an expression cannot have side effects. If two
expressions have the same value, then replacing one with the other
will not cause the program to compute a different result. This does
not mean that Lean cannot be used to write Hello, world!
to the
console, but performing I/O is not a core part of the experience of
using Lean in the same way. Thus, this chapter focuses on how to
evaluate expressions interactively with Lean, while the next chapter
describes how to write, compile, and run the Hello, world!
program.
To ask Lean to evaluate an expression, write #eval
before it in your
editor, which will then report the result back. Typically, the result
is found by putting the cursor or mouse pointer over #eval
. For
instance,
#eval 1 + 2
yields the value 3
.
Lean obeys the ordinary rules of precedence and associativity for arithmetic operators. That is,
#eval 1 + 2 * 5
yields the value 11
rather than
15
.
While both ordinary mathematical notation and the majority of
programming languages use parentheses (e.g. f(x)
) to apply a function to its
arguments, Lean simply writes the function next to its
arguments (e.g. f x
). Function application is one of the most common operations,
so it pays to keep it concise. Rather than writing
#eval String.append("Hello, ", "Lean!")
to compute "Hello, Lean!"
,
one would instead write
#eval String.append "Hello, " "Lean!"
where the function's two arguments are simply written next to it with spaces.
Just as the orderofoperations rules for arithmetic demand
parentheses in the expression (1 + 2) * 5
, parentheses are also
necessary when a function's argument is to be computed via another
function call. For instance, parentheses are required in
#eval String.append "great " (String.append "oak " "tree")
because otherwise the second String.append
would be interpreted as
an argument to the first, rather than as a function being passed
"oak "
and "tree"
as arguments. The value of the inner String.append
call must be found first, after which it can be appended to "great "
,
yielding the final value "great oak tree"
.
Imperative languages often have two kinds of conditional: a
conditional statement that determines which instructions to carry
out based on a Boolean value, and a conditional expression that
determines which of two expressions to evaluate based on a Boolean
value. For instance, in C and C++, the conditional statement is
written using if
and else
, while the conditional expression is
written with a ternary operator ?
and :
. In Python, the
conditional statement begins with if
, while the conditional
expression puts if
in the middle.
Because Lean is an expressionoriented functional language, there are no conditional statements, only conditional expressions.
They are written using if
, then
, and else
. For
instance,
String.append "it is " (if 1 > 2 then "yes" else "no")
evaluates to
String.append "it is " (if false then "yes" else "no")
which evaluates to
String.append "it is " "no"
which finally evaluates to "it is no"
.
For the sake of brevity, a series of evaluation steps like this will sometimes be written with arrows between them:
String.append "it is " (if 1 > 2 then "yes" else "no")
===>
String.append "it is " (if false then "yes" else "no")
===>
String.append "it is " "no"
===>
"it is no"
Messages You May Meet
Asking Lean to evaluate a function application that is missing an argument will lead to an error message. In particular, the example
#eval String.append "it is "
yields a quite long error message:
expression
String.append "it is "
has type
String → String
but instance
Lean.MetaEval (String → String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
This message occurs because Lean functions that are applied to only some of their arguments return new functions that are waiting for the rest of the arguments. Lean cannot display functions to users, and thus returns an error when asked to do so.
Exercises
What are the values of the following expressions? Work them out by hand, then enter them into Lean to check your work.
42 + 19
String.append "A" (String.append "B" "C")
String.append (String.append "A" "B") "C"
if 3 == 3 then 5 else 7
if 3 == 4 then "equal" else "not equal"
Types
Types classify programs based on the values that they can compute. Types serve a number of roles in a program:

They allow the compiler to make decisions about the inmemory representation of a value.

They help programmers to communicate their intent to others, serving as a lightweight specification for the inputs and outputs of a function that the compiler can ensure the program adheres to.

They prevent various potential mistakes, such as adding a number to a string, and thus reduce the number of tests that are necessary for a program.

They help the Lean compiler automate the production of auxiliary code that can save boilerplate.
Lean's type system is unusually expressive. Types can encode strong specifications like "this sorting function returns a permutation of its input" and flexible specifications like "this function has different return types, depending on the value of its argument". The type system can even be used as a fullblown logic for proving mathematical theorems. This cuttingedge expressive power doesn't obviate the need for simpler types, however, and understanding these simpler types is a prerequisite for using the more advanced features.
Every program in Lean must have a type. In particular, every expression must have a type before it can be evaluated. In the examples so far, Lean has been able to discover a type on its own, but it is sometimes necessary to provide one. This is done using the colon operator:
#eval (1 + 2 : Nat)
Here, Nat
is the type of natural numbers, which are arbitraryprecision unsigned integers.
In Lean, Nat
is the default type for nonnegative integer literals.
This default type is not always the best choice.
In C, unsigned integers underflow to the largest representable numbers when subtraction would otherwise yield a result less than zero.
Nat
, however, can represent arbitrarilylarge unsigned numbers, so there is no largest number to underflow to.
Thus, subtraction on Nat
returns 0
when the answer would have otherwise been negative.
For instance,
#eval 1  2
evaluates to 0
rather
than 1
. To use a type that can represent the negative integers,
provide a it directly:
#eval (1  2 : Int)
With this type, the result is 1
, as expected.
To check the type of an expression without evaluating it, use #check
instead of #eval
. For instance:
#check (1  2 : Int)
reports 1  2 : Int
without actually performing the subtraction.
When a program can't be given a type, an error is returned from both
#check
and #eval
. For instance:
#check String.append "hello" [" ", "world"]
outputs
application type mismatch
String.append "hello" [" ", "world"]
argument
[" ", "world"]
has type
List String : Type
but is expected to have type
String : Type
because the second argument to String.append
is expected to be a
string, but a list of strings was provided instead.
Functions and Definitions
In Lean, definitions are introduced using the def
keyword. For instance, to define the name hello
to refer to the string "Hello"
, write:
def hello := "Hello"
In Lean, new names are defined using the colonequal operator:=
rather than =
. This is because =
is used to describe equalities
between existing expressions, and using two different operators helps
prevent confusion.
In the definition of hello
, the expression "Hello"
is simple enough that Lean is able to determine the definition's type automatically.
However, most definitions are not so simple, so it will usually be necessary to add a type.
This is done using a colon after the name being defined.
def lean : String := "Lean"
Now that the names have been defined, they can be used, so
#eval String.append hello (String.append " " lean)
outputs
"Hello Lean"
In Lean, defined names may only be used after their definitions.
In many languages, definitions of functions use a different syntax than definitions of other values.
For instance, Python function definitions begin with the def
keyword, while other definitions are defined with an equals sign.
In Lean, functions are defined using the same def
keyword as other values.
Nonetheless, definitions such as hello
introduce names that refer directly to their values, rather than to zeroargument functions that return equivalent results each time they are called.
Defining Functions
There are a variety of ways to define functions in Lean. The simplest is to place the function's arguments before the definition's type, separated by spaces. For instance, a function that adds one to its argument can be written:
def add1 (n : Nat) : Nat := n + 1
Testing this function with #eval
gives 8
, as expected:
#eval add1 7
Just as functions are applied to multiple arguments just by writing spaces between each argument, functions that accept multiple arguments are defined with spaces between the arguments' names and types. The function maximum
, whose result is equal to the greatest of its two arguments, takes two Nat
arguments n
and k
and returns a Nat
.
def maximum (n : Nat) (k : Nat) : Nat :=
if n < k then
k
else n
When a defined function like maximum
has been provided with its arguments, the result is determined by first replacing the argument names with the provided values in the body, and then evaluating the resulting body. For example:
maximum (5 + 8) (2 * 7)
===>
maximum 13 14
===>
if 13 < 14 then 14 else 13
===>
14
Expressions that evaluate to natural numbers, integers, and strings have types that say this (Nat
, Int
, and String
, respectively). This is also true of functions. A function that accepts a Nat
and returns a Bool
has type Nat → Bool
, and a function that accepts two Nat
s and returns a Nat
has type Nat → Nat → Nat
.
Entering #check add1
yields add1 : Nat → Nat
and #check maximum
yields maximum : Nat → Nat → Nat
.
This arrow can also be written with an ASCII alternative arrow >
, so the preceding function types can be written Nat > Bool
and Nat > Nat > Nat
, respectively.
Behind the scenes, all functions actually expect precisely one argument.
Functions like maximum
that seem to take more than one argument are in fact functions that take one argument and then return a new function.
This new function takes the next argument, and the process continues until no more arguments are expected.
This can be seen by providing one argument to a multipleargument function: #check maximum 3
yields maximum 3 : Nat → Nat
and #check String.append "Hello "
yields String.append "Hello " : String → String
.
Using a function that returns a function to implement multipleargument functions is called currying after the mathematician Haskell Curry.
Function arrows associate to the right, which means that Nat → Nat → Nat
should be parenthesized Nat → (Nat → Nat)
.
Exercises
 Define the function
joinStringsWith
with typeString > String > String > String
that creates a new string by placing its first argument between its second and third arguments.joinStringsWith ", " "one" "and another"
should evaluate to"one, and another"
.  What is the type of
joinStringsWith ": "
? Check your answer with Lean.  Define a function
volume
with typeNat → Nat → Nat → Nat
that computes the volume of a rectangular prism with the given height, width, and depth.
Defining Types
Most typed programming languages have some means of defining aliases for types, such as C's typedef
.
In Lean, however, types are a firstclass part of the language  they are expressions like any other.
This means that definitions can refer to types just as well as they can refer to other values.
For instance, if String
is too much to type, a shorter abbreviation Str
can be defined:
def Str : Type := String
It is then possible to use Str
as a definition's type instead of String
:
def aStr : Str := "This is a string."
The reason this works is that types follow the same rules as the rest of Lean.
Types are expressions, and in an expression, a defined name can be replaced with its definition.
Because Str
has been defined to mean String
, the definition of aStr
makes sense.
Messages You May Meet
Experimenting with using definitions for types is made more complicated by a feature of Lean that has not yet been introduced.
If Nat
is too short, a longer name NaturalNumber
can be defined:
def NaturalNumber : Type := Nat
However, using NaturalNumber
as a definition's type instead of Nat
does not have the expected effect.
In particular, the definition:
def thirtyEight : NaturalNumber := 38
results in the following error:
failed to synthesize instance
OfNat NaturalNumber 38
This error occurs because Lean allows number literals to be overloaded. When it makes sense to do so, natural number literals can be used for new types, just as if those types were built in to the system. This is part of Lean's mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes. The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above.
One way to work around this limitation is by providing the type Nat
on the righthand side of the definition, causing Nat
's overloading rules to be used for 38
:
def thirtyEight : NaturalNumber := (38 : Nat)
The definition is still typecorrect because NaturalNumber
is the same type as Nat
—by definition!
Another solution is to define an overloading for NaturalNumber
that works equivalently to the one for Nat
.
This requires more advanced features of Lean, however.
Finally, defining the new name for Nat
using abbrev
instead of def
allows overloading resolution to replace the defined name with its definition.
Definitions written using abbrev
are always unfolded.
For instance,
abbrev N : Type := Nat
and
def thirtyNine : N := 39
are accepted without issue.
Behind the scenes, some definitions are internally marked as being unfoldable during overload resolution, while others are not.
Definitions that are to be unfolded are called reducible.
Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand.
Definitions produced with abbrev
are marked as reducible.
Structures
The first step in writing a program is usually to identify the problem domain's concepts, and then find suitable representations for them in code.
Sometimes, a domain concept is a collection of other, simpler, concepts.
In that case, it can be convenient to group these simpler components together into a single "package", which can then be given a meaningful name.
In Lean, this is done using structures, which are analogous to struct
s in C or Rust and record
s in C#.
Defining a structure introduces a completely new type to Lean that can't be reduced to any other type. This is useful because multiple structures might represent different concepts that nonetheless contain the same data. For instance, a point might be represented using either Cartesian or polar coordinates, each being a pair of floatingpoint numbers. Defining separate structures prevents API clients from confusing one for another.
Lean's floatingpoint number type is called Float
, and floatingpoint numbers are written in the usual notation.
#check 1.2
1.2 : Float
#check 454.2123215
454.2123215 : Float
#check 0.0
0.0 : Float
When floating point numbers are written with the decimal point, Lean will infer the type Float
. If they are written without it, then a type annotation may be necessary.
#check 0
0 : Nat
#check (0 : Float)
0 : Float
A Cartesian point is a structure with two Float
fields, called x
and y
.
This is declared using the structure
keyword.
structure Point where
x : Float
y : Float
deriving Repr
After this declaration, Point
is a new structure type.
The final line, which says deriving Repr
, asks Lean to generate code to display values of type Point
.
This code is used by #eval
to render the result of evaluation for consumption by programmers, analogous to the repr
functions in Python and Rust.
It is also possible to override the compiler's generated display code.
The typical way to create a instance of a structure type is to provide values for all of its fields inside of curly braces.
The origin of a Cartesian plane is where both x
and y
are both zero:
def origin : Point := { x := 0.0, y := 0.0 }
If the deriving Repr
line in Point
's definition were omitted, then attempting #eval origin
would yield an error similar to that which occurs when omitting a function's argument:
expression
origin
has type
Point
but instance
Lean.MetaEval Point
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
That message is saying that the evaluation machinery doesn't know how to communicate the result of evaluation back to the user.
Happily, with deriving Repr
, the result of #eval origin
looks very much like the definition of origin
.
{ x := 0.000000, y := 0.000000 }
Because structures exist to "bundle up" a collection of data, naming it and treating it as a single unit, it is also important to be able to extract the individual fields of a structure. This is done using dot notation, as in C, Python, or Rust.
#eval origin.x
0.000000
#eval origin.y
0.000000
This can be used to define functions that take structures as arguments.
For instance, addition of points is performed by adding the underlying coordinate values.
It should be the case that #eval addPoints { x := 1.5, y := 32 } { x := 8, y := 0.2 }
yields
{ x := 6.500000, y := 32.200000 }
The function itself takes two Points
as arguments, called p1
and p2
.
The resulting point is based on the x
and y
fields of both p1
and p2
:
def addPoints (p1 : Point) (p2 : Point) : Point :=
{ x := p1.x + p2.x, y := p1.y + p2.y }
Similarly, the distance between two points, which is the square root of the sum of the squares of the differences in their x
and y
components, can be written:
def distance (p1 : Point) (p2 : Point) : Float :=
Float.sqrt (((p2.x  p1.x) ^ 2.0) + ((p2.y  p1.y) ^ 2.0))
For example, the distance between (1, 2) and (5, 1) is 5:
#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := 1.0 }
5.000000
Multiple structures may have fields with the same names.
For instance, a threedimensional point datatype may share the fields x
and y
, and be instantiated with the same field names:
structure Point3D where
x : Float
y : Float
z : Float
deriving Repr
def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }
This means that the structure's expected type must be known in order to use the curlybrace syntax. If the type is not known, Lean will not be able to instantiate the structure. For instance,
#check { x := 0.0, y := 0.0 }
leads to the error
invalid {...} notation, expected type is not known
As usual, the situation can be remedied by providing a type annotation.
#check ({ x := 0.0, y := 0.0 } : Point)
{ x := 0.0, y := 0.0 } : Point
To make programs more concise, Lean also allows the structure type annotation inside the curly braces.
#check { x := 0.0, y := 0.0 : Point}
{ x := 0.0, y := 0.0 } : Point
Updating Structures
Imagine a function zeroX
that replaces the x
field of a Point
with 0.0
.
In most programming language communities, this sentence would mean that the memory location pointed to by x
was to be overwritten with a new value.
However, Lean does not have mutable state.
In functional programming communities, what is almost always meant by this kind of statement is that a fresh Point
is allocated with the x
field pointing to the new value, and all other fields pointing to the original values from the input.
One way to write zeroX
is to follow this description literally, filling out the new value for x
and manually transferring y
:
def zeroX (p : Point) : Point :=
{ x := 0, y := p.y }
This style of programming has drawbacks, however. First off, if a new field is added to a structure, then every site that updates any field at all must be updated, causing maintenance difficulties. Secondly, if the structure contains multiple fields with the same type, then there is a real risk of copypaste coding leading to field contents being duplicated or switched. Finally, the program becomes long and bureaucratic.
Lean provides a convenient syntax for replacing some fields in a structure while leaving the others alone.
This is done by using the with
keyword in a structure initialization.
The source of unchanged fields occurs before the with
, and the new fields occur after.
For instance, zeroX
can be written with only the new x
value:
def zeroX (p : Point) : Point :=
{ p with x := 0 }
Remember that this structure update syntax does not modify existing values—it creates new values that share some fields with old values.
For instance, given the point fourAndThree
:
def fourAndThree : Point :=
{ x := 4.3, y := 3.4 }
evaluating it, then evaluating an update of it using zeroX
, then evaluating it again yields the original value:
#eval fourAndThree
{ x := 4.300000, y := 3.400000 }
#eval zeroX fourAndThree
{ x := 0.000000, y := 3.400000 }
#eval fourAndThree
{ x := 4.300000, y := 3.400000 }
One consequence of the fact that structure updates do not modify the original structure is that it becomes easier to reason about cases where the new value is computed from the old one. All references to the old structure continue to refer to the same field values in all of the new values provided.
Behind the Scenes
Every structure has a constructor. Here, the term "constructor" may be a source of confusion. Unlike constructors in languages such as Java or Python, constructors in Lean are not arbitrary code to be run when a datatype is initialized. Instead, constructors simply gather the data to be stored in the newlyallocated data structure. It is not possible to provide a custom constructor that preprocesses data or rejects invalid arguments. This is really a case of the word "constructor" having different, but related, meanings in the two contexts.
By default, the constructor for a structure named S
is named S.mk
.
Here, S
is a namespace qualifier, and mk
is the name of the constructor itself.
Instead of using curlybrace initialization syntax, the constructor can also be applied directly.
#check Point.mk 1.5 2.8
However, this is not generally considered to be good Lean style, and Lean even returns its feedback using the standard structure initializer syntax.
{ x := 1.5, y := 2.8 } : Point
Constructors have function types, which means that they can be used anywhere that a function is expected.
For instance, Point.mk
is a function that accepts two Float
s (respectively x
and y
) and returns a new Point
.
#check Point.mk
Point.mk : Float → Float → Point
To override a structure's constructor name, write it with two colons at the beginning.
For instance, to use Point.point
instead of Point.mk
, write:
structure Point where
point ::
x : Float
y : Float
deriving Repr
In addition to the constructor, an accessor function is defined for each field of a structure.
These have the same name as the field, in the structure's namespace.
For Point
, accessor functions Point.x
and Point.y
are generated.
#check Point.x
Point.x : Point → Float
#check Point.y
Point.y : Point → Float
In fact, just as the curlybraced structure construction syntax is converted to a call to the structure's constructor behind the scenes, the syntax p1.x
in the prior definition of addPoints
is converted into a call to the Point.x
accessor.
That is, #eval origin.x
and #eval Point.x origin
both yield
0.000000
Accessor dot notation is usable with more than just structure fields.
It can also be used for functions that take any number of arguments.
More generally, accessor notation has the form TARGET.f ARG1 ARG2 ...
.
If TARGET
has type T
, the function named T.f
is called.
TARGET
becomes its leftmost argument of type T
, which is often but not always the first one, and ARG1 ARG2 ...
are provided in order as the remaining arguments.
For instance, String.append
can be invoked from a string with accessor notation, even though String
is not a structure with an append
field.
#eval "one string".append " and another"
"one string and another"
In that example, TARGET
represents "one string"
and ARG1
represents " and another"
.
The function Point.modifyBoth
(that is, modifyBoth
defined in the Point
namespace) applies a function to both fields in a Point
:
def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
{ x:= f p.x, y := f p.y }
Even though the Point
argument comes after the function argument, it can be used with dot notation as well:
#eval fourAndThree.modifyBoth Float.floor
{ x := 4.000000, y := 3.000000 }
In this case, TARGET
represents fourAndThree
, while ARG1
is Float.floor
.
This is because the target of the accessor notation is used as the first argument in which the type matches, not necessarily the first argument.
Exercises
 Define a structure named
RectangularPrism
that contains the height, width, and depth of a rectangular prism, each as aFloat
.  Define a function named
volume : RectangularPrism → Float
that computes the volume of a rectangular prism.  Define a structure named
Segment
that represents a line segment by its endpoints, and define a functionlength : Segment → Float
that computes the length of a line segment.Segment
should have at most two fields.  Which names are introduced by the declaration of
RectangularPrism
?  Which names are introduced by the following declarations of
Hamster
andBook
? What are their types?
structure Hamster where
name : String
fluffy : Bool
structure Book where
makeBook ::
title : String
author : String
price : Float
Datatypes and Patterns
Structures enable multiple independent pieces of data to be combined into a coherent whole that is represented by a brand new type. Types such as structures that group together a collection of values are called product types. Many domain concepts, however, can't be naturally represented as structures. For instance, an application might need to track user permissions, where some users are document owners, some may edit documents, and others may only read them. A calculator has a number of binary operators, such as addition, subtraction, and multiplication. Structures do not provide an easy way to encode multiple choices.
Similarly, while a structure is an excellent way to keep track of a fixed set of fields, many applications require data that may contain an arbitrary number of elements. Most classic data structures, such as trees and lists, have a recursive structure, where the tail of a list is itself a list, or where the left and right branches of a binary tree are themselves binary trees. In the aforementioned calculator, the structure of expressions themselves is recursive. The summands in an addition expression may themselves be multiplication expressions, for instance.
Datatypes that allow choices are called sum types and datatypes that can include instances of themselves are called recursive datatypes. Recursive sum types are called inductive datatypes, because mathematical induction may be used to prove statements about them. Most userdefined types are inductive datatypes. When programming, inductive datatypes are consumed through pattern matching and recursive functions.
Many of the builtin types are actually inductive datatypes in the standard library.
For instance, Bool
is an inductive datatype:
inductive Bool where
 false : Bool
 true : Bool
This definition has two main parts.
The first line provides the name of the new type (Bool
), while the remaining lines each describe a constructor.
As with constructors of structures, constructors of inductive datatypes are mere inert receivers of and containers for other data, rather than places to insert arbitrary initialization and validation code.
Unlike structures, inductive datatypes may have multiple constructors.
Here, there are two constructors, true
and false
, and neither takes any arguments.
Just as a structure declaration places its names in a namespace named after the declared type, an inductive datatype places the names of its constructors in a namespace.
In the Lean standard library, true
and false
are reexported from this namespace so that they can be written alone, rather than as Bool.true
and Bool.false
, respectively.
From a data modeling perspective, inductive datatypes are used in many of the same contexts where a sealed abstract class might be used in other languages.
In languages like C# or Java, one might write a similar definition of definition of Bool
:
abstract class Bool {}
class True : Bool {}
class False : Bool {}
However, the specifics of these representations are fairly different. In particular, each nonabstract class creates both a new type and new ways of allocating data. In the objectoriented example, True
and False
are both types that are more specific than Bool
, while the Lean definition introduces only the new type Bool
.
The type Nat
of nonnegative integers is an inductive datatype:
inductive Nat where
 zero : Nat
 succ (n : Nat) : Nat
Here, zero
represents 0, while succ
represents the successor of some other number.
The Nat
mentioned in succ
's declaration is the very type Nat
that is in the process of being defined.
Successor means "one greater than", so the successor of five is six and the successor of 32,185 is 32,186.
Using this definition, 4
is represented as Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))
.
This definition is almost like the definition of Bool
with slightly different names.
The only real difference is that succ
is followed by (n : Nat)
, which specifies that the constructor succ
takes an argument of type Nat
which happens to be named n
.
The names zero
and succ
are in a namespace named after their type, so they must be referred to as Nat.zero
and Nat.succ
, respectively.
Argument names, such as n
, may occur in Lean's error messages and in feedback provided when writing mathematical proofs.
Lean also has an optional syntax for providing arguments by name.
Generally, however, the choice of argument name is less important than the choice of a structure field name, as it does not form as large a part of the API.
In C# or Java, Nat
could be defined as follows:
abstract class Nat {}
class Zero : Nat {}
class Succ : Nat {
public Nat n;
public Succ(Nat pred) {
n = pred;
}
}
Just as in the Bool
example above, this defines more types than the Lean equivalent.
Additionally, this example highlights how Lean datatype constructors are much more like subclasses of an abstract class than they are like constructors in C# or Java, as the constructor shown here contains initialization code to be executed.
Pattern Matching
In many languages, these kinds of data are consumed by first using an instanceof operator to check which subclass has been received and then reading the values of the fields that are available in the given subclass. The instanceof check determines which code to run, ensuring that the data needed by this code is available, while the fields themselves provide the data. In Lean, both of these purposes are simultaneously served by pattern matching.
An example of a function that uses pattern matching is isZero
, which is a function that returns true
when its argument is Nat.zero
, or false otherwise.
def isZero (n : Nat) : Bool :=
match n with
 Nat.zero => true
 Nat.succ k => false
The match
expression is provided the function's argument n
for destructuring.
If n
was constructed by Nat.zero
, then the first branch of the pattern match is taken, and the result is true
.
If n
was constructed by Nat.succ
, then the second branch is taken, and the result is false
.
Stepbystep, evaluation of isZero Nat.zero
proceeds as follows:
isZero Nat.zero
===>
match Nat.zero with
 Nat.zero => true
 Nat.succ k => false
===>
true
Evaluation of isZero 5
proceeds similarly:
isZero 5
===>
isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
===>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
 Nat.zero => true
 Nat.succ k => false
===>
false
The k
in the second branch of the pattern in isZero
is not decorative.
It makes the Nat
that is the argument to succ
visible, with the provided name.
That smaller number can then be used to compute the final result of the expression.
Just as the successor of some number n is one greater than n (that is, n + 1), the predecessor of a number is one less than it.
If pred
is a function that finds the predecessor of a Nat
, then it should be the case that the following examples find the expected result:
#eval pred 5
4
#eval pred 839
838
Because Nat
cannot represent negative numbers, 0
is a bit of a conundrum.
Usually, when working with Nat
, operators that would ordinarily produce a negative number are redefined to produce 0
itself:
#eval pred 0
0
To find the predecessor of a Nat
, the first step is to check which constructor was used to create it.
If it was Nat.zero
, then the result is Nat.zero
.
If it was Nat.succ
, then the name k
is used to refer to the Nat
underneath it.
And this Nat
is the desired predecessor, so the result of the Nat.succ
branch is k
.
def pred (n : Nat) : Nat :=
match n with
 Nat.zero => Nat.zero
 Nat.succ k => k
Applying this function to 5
yields the following steps:
pred 5
===>
pred (Nat.succ 4)
===>
match Nat.succ 4 with
 Nat.zero => Nat.zero
 Nat.succ k => k
===>
4
Pattern matching can be used with structures as well as with sum types.
For instance, a function that extracts the third dimension from a Point3D
can be written as follows:
def depth (p : Point3D) : Float :=
match p with
 { x:= h, y := w, z := d } => d
In this case, it would have been much simpler to just use the z
accessor, but structure patterns are occasionally the simplest way to write a function.
Recursive Functions
Definitions that refer to the name being defined are called recursive definitions.
Inductive datatypes are allowed to be recursive; indeed, Nat
is an example of such a datatype because succ
demands another Nat
.
Recursive datatypes can represent arbitrarily large data, limited only by technical factors like available memory.
Just as it would be impossible to write down one constructor for each natural number in the datatype definition, it is also impossible to write down a pattern match case for each possibility.
Recursive datatypes are nicely complemented by recursive functions.
A simple recursive function over Nat
checks whether its argument is even.
In this case, zero
is even.
Nonrecursive branches of the code like this one are called base cases.
The successor of an odd number is even, and the successor of an even number is odd.
This means that a number built with succ
is even if and only if its argument is not even.
def even (n : Nat) : Bool :=
match n with
 Nat.zero => true
 Nat.succ k => not (even k)
This pattern of thought is typical for writing recursive functions on Nat
.
First, identify what to do for zero
.
Then, determine how to transform a result for an arbitrary Nat
into a result for its successor, and apply this transformation to the result of the recursive call.
This pattern is called structural recursion.
Unlike many languages, Lean ensures by default that every recursive function will eventually reach a base case.
From a programming perspective, this rules out accidental infinite loops.
But this feature is especially important when proving theorems, where infinite loops cause major difficulties.
A consequence of this is that Lean will not accept a version of even
that attempts to invoke itself recursively on the original number:
def evenLoops (n : Nat) : Bool :=
match n with
 Nat.zero => true
 Nat.succ k => not (evenLoops n)
The important part of the error message is that Lean could not determine that the recursive function always reaches a base case (because it doesn't).
fail to show termination for
evenLoops
with errors
structural recursion cannot be used
wellfounded recursion cannot be used, 'evenLoops' does not take any (nonfixed) arguments
Even though addition takes two arguments, only one of them needs to be inspected. To add zero to a number n, just return n. To add the successor of k to n, take the successor of the result of adding k to n.
def plus (n : Nat) (k : Nat) : Nat :=
match k with
 Nat.zero => n
 Nat.succ k' => Nat.succ (plus n k')
In the definition of plus
, the name k'
is chosen to indicate that it is connected to, but not identical with, the argument k
.
For instance, walking through the evaluation of plus 3 2
yields the following steps:
plus 3 2
===>
plus 3 (Nat.succ (Nat.succ Nat.zero))
===>
match Nat.succ (Nat.succ Nat.zero) with
 Nat.zero => 3
 Nat.succ k' => Nat.succ (plus 3 k')
===>
Nat.succ (plus 3 (Nat.succ Nat.zero))
===>
Nat.succ (match Nat.succ Nat.zero with
 Nat.zero => 3
 Nat.succ k' => Nat.succ (plus 3 k'))
===>
Nat.succ (Nat.succ (plus 3 Nat.zero))
===>
Nat.succ (Nat.succ (match Nat.zero with
 Nat.zero => 3
 Nat.succ k' => Nat.succ (plus 3 k')))
===>
Nat.succ (Nat.succ 3)
===>
5
One way to think about addition is that n + k applies Nat.succ
k times to n.
Similarly, multiplication n × k adds n to itself k times and subtraction n  k takes n's predecessor k times.
def times (n : Nat) (k : Nat) : Nat :=
match k with
 Nat.zero => Nat.zero
 Nat.succ k' => plus n (times n k')
def minus (n : Nat) (k : Nat) : Nat :=
match k with
 Nat.zero => n
 Nat.succ k' => pred (minus n k')
Not every function can be easily written using structural recursion.
The understanding of addition as iterated Nat.succ
, multiplication as iterated addition, and subtraction as iterated predecessor suggests an implementation of division as iterated subtraction.
In this case, if the numerator is less that the divisor, the result is zero.
Otherwise, the result is the successor of dividing the numerator minus the divisor by the divisor.
def div (n : Nat) (k : Nat) : Nat :=
if n < k then
0
else Nat.succ (div (n  k) k)
This program terminates for all inputs, as it always makes progress towards the base case.
However, it is not structurally recursive, because it doesn't follow the pattern of finding a result for zero and transforming a result for a smaller Nat
into a result for its successor.
In particular, the recursive invocation of the function is applied to the result of another function call, rather than to an input constructor's argument.
Thus, Lean rejects it with the following message:
fail to show termination for
div
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
div (n  k) k
argument #2 was not used for structural recursion
failed to eliminate recursive application
div (n  k) k
structural recursion cannot be used
failed to prove termination, use `termination_by` to specify a wellfounded relation
This message means that div
requires a manual proof of termination.
This topic will be explored in a later chapter.
Polymorphism
Just as in most languages, types in Lean can take arguments.
For instance, the type List Nat
describes lists of natural numbers, List String
describes lists of strings, and List (List Point)
describes lists of lists of points.
This is very similar to List<Nat>
, List<String>
, or List<List<Point>>
in a language like C# or Java.
Just as Lean uses a space to pass an argument to a function, it uses a space to pass an argument to a type.
In functional programming, the term polymorphism typically refers to datatypes and definitions that take types as arguments. This is different from the objectoriented programming community, where the term typically refers to subclasses that may override some behavior of their superclass. In this book, "polymorphism" always refers to the first sense of the word. These type arguments can be used in the datatype or definition, which allows the same datatype or definition to be used with any type that results from replacing the arguments' names with some other types.
The Point
structure requires that both the x
and y
fields are Float
s.
There is, however, nothing about points that require a specific representation for each coordinate.
A polymorphic version of Point
, called PPoint
, can take a type as an argument, and then use that type for both fields:
structure PPoint (α : Type) where
x : α
y : α
deriving Repr
Just as a function definition's arguments are written immediately after the name being defined, a structure's arguments are written immediately after the structure's name.
It is customary to use Greek letters to name type arguments in Lean when no more specific name suggests itself.
Type
is a type that describes other types, so Nat
, List String
, and PPoint Int
all have type Type
.
Just like List
, PPoint
can be used by providing a specific type as its argument:
def natOrigin : PPoint Nat :=
{ x := Nat.zero, y := Nat.zero }
In this example, both fields are expected to be Nat
s.
Just as a function is called by replacing its argument variables with its argument values, providing PPoint
with the type Nat
as an argument yields a structure in which the fields x
and y
have the type Nat
, because the argument name α
has been replaced by the argument type Nat
.
Because types are ordinary expressions in Lean, passing arguments to polymorphic types (like PPoint
) doesn't require any special syntax.
Definitions may also take types as arguments, which makes them polymorphic.
The function replaceX
replaces the x
field of a PPoint
with a new value.
In order to allow replaceX
to work with any polymorphic point, it must be polymorphic itself.
This is achieved by having its first argument be the type of the point's fields, with later arguments referring back to the first argument's name.
def replaceX (α : Type) (point : PPoint α) (newX : α) : PPoint α :=
{ point with x := newX }
In other words, when the types of the arguments point
and newX
mention α
, they are referring to whichever type was provided as the first argument.
This is similar to the way that function argument names refer to the values that were provided when they occur in the function's body.
This can be seen by asking Lean to check the type of replaceX
, and then asking it to check the type of replaceX Nat
.
#check replaceX
replaceX : (α : Type) → PPoint α → α → PPoint α
This function type includes the name of the first argument, and later arguments in the type refer back to this name.
Just as the value of a function application is found by replacing the argument name with the provided argument value in the function's body, the type of a function application is found by replacing the argument's name with the provided value in the function's return type.
Providing the first argument, Nat
, causes all occurrences of α
in the remainder of the type to be replaced with Nat
:
#check replaceX Nat
replaceX Nat : PPoint Nat → Nat → PPoint Nat
Because the remaining arguments are not explicitly named, no further substitution occurs as more arguments are provided:
#check replaceX Nat natOrigin
replaceX Nat natOrigin : Nat → PPoint Nat
#check replaceX Nat natOrigin 5
replaceX Nat natOrigin 5 : PPoint Nat
The fact that the type of the whole function application expression was determined by passing a type as an argument has no bearing on the ability to evaluate it.
#eval replaceX Nat natOrigin 5
{ x := 5, y := 0 }
Polymorphic functions work by taking a named type argument and having later types refer to the argument's name. However, there's nothing special about type arguments that allows them to be named. Given a datatype that represents positive or negative signs:
inductive Sign where
 pos
 neg
it is possible to write a function whose argument is a sign.
If the argument is positive, the function returns a Nat
, while if it's negative, it returns an Int
:
def posOrNegThree (s : Sign) : match s with  Sign.pos => Nat  Sign.neg => Int :=
match s with
 Sign.pos => (3 : Nat)
 Sign.neg => (3 : Int)
Because types are first class and can be computed using the ordinary rules of the Lean language, they can be computed by patternmatching against a datatype.
When Lean is checking this function, it uses the fact that the function's body patternmatches to run the same pattern in the type, showing that Nat
is the expected type for the pos
case and that Int
is the expected type for the neg
case.
Linked Lists
Lean's standard library includes a canonical linked list datatype, called List
, and special syntax that makes it more convenient to use.
Lists are written in square brackets.
For instance, a list that contains the prime numbers less than 10 can be written:
def primesUnder10 : List Nat := [2, 3, 5, 7]
Behind the scenes, List
is an inductive datatype, defined like this:
inductive List (α : Type) where
 nil : List α
 cons : α → List α → List α
The actual definition in the standard library is slightly different, because it uses features that have not yet been presented, but it is substantially similar.
This definition says that List
takes a single type as its argument, just as PPoint
did.
This type is the type of the entries stored in the list.
According to the constructors, a List α
can be built with either nil
or cons
.
The constructor nil
represents empty lists, and the constructor cons
represents a single element in the linked list.
The first argument to cons
is the head of the list, and the second argument is its tail.
The primesUnder10
example can be written more explicitly by using List
's constructors directly:
def explicitPrimesUnder10 : List Nat :=
List.cons 2 (List.cons 3 (List.cons 5 (List.cons 7 List.nil)))
These two definitions are completely equivalent, but primesUnder10
is much easier to read than explicitPrimesUnder10
.
Functions that consume List
s can be defined in much the same way as functions that consume Nat
s.
Indeed, one way to think of a linked list is as a Nat
that has an extra data field dangling off each succ
constructor.
From this point of view, computing the length of a list is the process of replacing each cons
with a succ
and the final nil
with a zero
.
Just as replaceX
took the type of the fields of the point as an argument, length
takes the type of the list's entries.
For example, if the list contains strings, then the first argument is String
: length String ["Sourdough", "bread"]
.
It should compute like this:
length String ["Sourdough", "bread"]
===>
length String (List.cons "Sourdough" (List.cons "bread" List.nil))
===>
Nat.succ (length String (List.cons "bread" List.nil))
===>
Nat.succ (Nat.succ (length String List.nil))
===>
Nat.succ (Nat.succ Nat.zero)
===>
2
The definition of length
is both polymorphic (because it takes the list entry type as an argument) and recursive (because it refers to itself).
Generally, functions follow the shape of the data: recursive datatypes lead to recursive functions, and polymorphic datatypes lead to polymorphic functions.
def length (α : Type) (xs : List α) : Nat :=
match xs with
 List.nil => Nat.zero
 List.cons y ys => Nat.succ (length α ys)
Names such as xs
and ys
are conventionally used to stand for lists of unknown values.
The s
in the name indicates that they are plural, so they are pronounced "exes" and "whys" rather than "x s" and "y s".
To make it easier to read functions on lists, the bracket notation []
can be used to patternmatch against nil
, and an infix ::
can be used in place of cons
:
def length (α : Type) (xs : List α) : Nat :=
match xs with
 [] => 0
 y :: ys => Nat.succ (length α ys)
Implicit Arguments
Both replaceX
and length
are somewhat bureaucratic to use, because the type argument is typically uniquely determined by the later values.
Indeed, in most languages, the compiler is perfectly capable of determining type arguments on its own, and only occasionally needs help from users.
This is also the case in Lean.
Arguments can be declared implicit by wrapping them in curly braces instead of parentheses when defining a function.
For instance, a version of replaceX
with an implicit type argument looks like this:
def replaceX {α : Type} (point : PPoint α) (newX : α) : PPoint α :=
{ point with x := newX }
It can be used with natOrigin
without providing Nat
explicitly, because Lean can infer the value of α
from the later arguments:
#eval replaceX natOrigin 5
{ x := 5, y := 0 }
Similarly, length
can be redefined to take the entry type implicitly:
def length {α : Type} (xs : List α) : Nat :=
match xs with
 [] => 0
 y :: ys => Nat.succ (length ys)
This length
function can be applied directly to primesUnder10
:
#eval length primesUnder10
4
In the standard library, Lean calls this function List.length
, which means that the dot syntax that is used for structure field access can also be used to find the length of a list:
#eval primesUnder10.length
4
Just as C# and Java require type arguments to provided explicitly from time to time, Lean is not always capable of finding implicit arguments.
In these cases, they can be provided using their names.
For instance, a version of List.length
that only works for lists of integers can be specified by setting α
to Int
:
#check List.length (α := Int)
List.length : List Int → Nat
More BuiltIn Datatypes
In addition to lists, Lean's standard library contains a number of other structures and inductive datatypes that can be used in a variety of contexts.
Option
Not every list has a first entry—some lists are empty. Many operations on collections may fail to find what they are looking for. For instance, a function that finds the first entry in a list may not find any such entry. It must therefore have a way to signal that there was no first entry.
Many languages have a null
value that represents the absence of a value.
Instead of equipping existing types with a special null
value, Lean provides a datatype called Option
that equips some other type with an indicator for missing values.
For instance, a nullable Int
is represented by Option Int
, and a nullable list of strings is represented by the type Option (List String)
.
Introducing a new type to represent nullability means that the type system ensures that checks for null
cannot be forgotten, because an Option Int
can't be used in a context where an Int
is expected.
Option
has two constructors, called some
and none
, that respectively represent the nonnull and null versions of the underlying type.
The nonnull constructor, some
, contains the underlying value, while none
takes no arguments:
inductive Option (α : Type) : Type where
 none : Option α
 some (val : α) : Option α
The Option
type is very similar to nullable types in languages like C# and Kotlin, but it is not identical.
In these languages, if a type (say, Boolean
) always refers to actual values of the type (true
and false
), the type Boolean?
or Nullable<Boolean>
additionally admits the null
value.
Tracking this in the type system is very useful: the type checker and other tooling can help programmers remember to check for null, and APIs that explicitly describe nullability through type signatures are more informative than ones that don't.
However, these nullable types differ from Lean's Option
in one very important way, which is that they don't allow multiple layers of optionality.
Option (Option Int)
can be constructed with none
, some none
, or some (some 360)
.
C#, on the other hand, forbids multiple layers of nullability by only allowing ?
to be added to nonnullable types, while Kotlin treats T??
as being equivalent to T?
.
This subtle difference is rarely relevant in practice, but it can matter from time to time.
To find the first entry in a list, if it exists, use List.head?
.
The question mark is part of the name, and is not related to the use of question marks to indicate nullable types in C# or Kotlin.
In the definition of List.head?
, an underscore is used to represent the tail of the list.
In patterns, underscores match anything at all, but do not introduce variables to refer to the matched data.
Using underscores instead of names is a way to clearly communicate to readers that part of the input is ignored.
def List.head? {α : Type} (xs : List α) : Option α :=
match xs with
 [] => none
 y :: _ => some y
A Lean naming convention is to define operations that might fail in groups using the suffixes ?
for a version that returns an Option
, !
for a version that crashes when provided with invalid input, and D
for a version that returns a default value when the operation would otherwise fail.
For instance, head
requires the caller to provide mathematical evidence that the list is not empty, head?
returns an Option
, head!
crashes the program when passed an empty list, and headD
takes a default value to return in case the list is empty.
The question mark and exclamation mark are part of the name, not special syntax, as Lean's naming rules are more liberal than many languages.
Because head?
is defined in the List
namespace, it can be used with accessor notation:
#eval primesUnder10.head?
some 2
However, attempting to test it on the empty list leads to two errors:
#eval [].head?
don't know how to synthesize implicit argument
@List.nil ?m.19130
context:
⊢ Type ?u.19127
don't know how to synthesize implicit argument
@_root_.List.head? ?m.19130 []
context:
⊢ Type ?u.19127
This is because Lean was unable to fully determine the expression's type.
In particular, it could neither find the implicit type argument to List.head?
, nor could it find the implicit type argument to List.nil
.
In Lean's output, ?m.XYZ
represents a part of a program that could not be inferred.
These unknown parts are called metavariables, and they occur in some error messages.
In order to evaluate an expression, Lean needs to be able to find its type, and the type was unavailable because the empty list does not have any entries from which the type can be found.
Explicitly providing a type allows Lean to proceed:
#eval [].head? (α := Int)
none
The error messages provide a useful clue. Both messages use the same metavariable to describe the missing implicit argument, which means that Lean has determined that the two missing pieces will share a solution, even though it was unable to determine the actual value of the solution.
Prod
The Prod
structure, short for "Product", is a generic way of joining two values together.
For instance, a Prod Nat String
contains a Nat
and a String
.
In other words, PPoint Nat
could be replaced by Prod Nat Nat
.
Prod
is very much like C#'s tuples, the Pair
and Triple
types in Kotlin, and tuple
in C++.
Many applications are best served by defining their own structures, even for simple cases like Point
, because using domain terminology can make it easier to read the code.
On the other hand, there are some cases where it is not worth the overhead of defining a new type. Additionally, some libraries are sufficiently generic that there is no more specific concept than "pair". Finally, the standard library contains a variety of convenience functions that make it easier to work with the builtin pair type.
The standard pair structure is called Prod
.
structure Prod (α : Type) (β : Type) : Type where
fst : α
snd : β
Lists are used so frequently that there is special syntax to make them more readable.
For the same reason, both the product type and its constructor have special syntax.
The type Prod α β
is typically written α × β
, mirroring the usual notation for a Cartesian product of sets.
Similarly, the usual mathematical notation for pairs is available for Prod
.
In other words, instead of writing:
def fives : String × Int := { fst := "five", snd := 5 }
it suffices to write:
def fives : String × Int := ("five", 5)
Both notations are rightassociative. This means that the following definitions are equivalent:
def sevens : String × Int × Nat := ("VII", 7, 4 + 3)
def sevens : String × (Int × Nat) := ("VII", (7, 4 + 3))
In other words, all products of more than two types, and their corresponding constructors, are actually nested products and nested pairs behind the scenes.
Sum
The Sum
datatype is a generic way of allowing a choice between values of two different types.
For instance, a Sum String Int
is either a String
or an Int
.
Like Prod
, Sum
should be used either when writing very generic code, for a very small section of code where there is no sensible domainspecific type, or when the standard library contains useful functions.
In most situations, it is more readable and maintainable to use a custom inductive type.
Values of type Sum α β
are either the constructor inl
applied to a value of type α
or the constructor inr
applied to a value of type β
:
inductive Sum (α : Type) (β : Type) : Type where
 inl : α → Sum α β
 inr : β → Sum α β
These names are abbreviations for "left injection" and "right injection", respectively.
Just as the Cartesian product notation is used for Prod
, a "circled plus" notation is used for Sum
, so α ⊕ β
is another way to write Sum α β
.
There is no special syntax for Sum.inl
and Sum.inr
.
For instance, if pet names can either be dog names or cat names, then a type for them can be introduced as a sum of strings:
def PetName : Type := String ⊕ String
In a real program, it would usually be better to define a custom inductive datatype for this purpose with informative constructor names.
Here, Sum.inl
is to be used for dog names, and Sum.inr
is to be used for cat names.
These constructors can be used to write a list of animal names:
def animals : List PetName :=
[Sum.inl "Spot", Sum.inr "Tiger", Sum.inl "Fifi", Sum.inl "Rex", Sum.inr "Floof"]
Pattern matching can be used to distinguish between the two constructors.
For instance, a function that counts the number of dogs in a list of animal names (that is, the number of Sum.inl
constructors) looks like this:
def howManyDogs (pets : List PetName) : Nat :=
match pets with
 [] => 0
 Sum.inl _ :: morePets => howManyDogs morePets + 1
 Sum.inr _ :: morePets => howManyDogs morePets
Function calls are evaluated before infix operators, so howManyDogs morePets + 1
is the same as (howManyDogs morePets) + 1
.
As expected, #eval howManyDogs animals
yields 3
.
Unit
Unit
is a type with just one argumentless constructor, called unit
.
In other words, it describes only a single value, which consists of said constructor applied to no arguments whatsoever.
Unit
is defined as follows:
inductive Unit : Type where
 unit : Unit
On its own, Unit
is not particularly useful.
However, in polymorphic code, it can be used as a placeholder for data that is missing.
For instance, the following inductive datatype represents arithmetic expressions:
inductive ArithExpr (ann : Type) : Type where
 int : ann → Int → ArithExpr ann
 plus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
 minus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
 times : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
The type argument ann
stands for annotations, and each constructor is annotated.
Expressions coming from a parser might be annotated with source locations, so a return type of ArithExpr SourcePos
ensures that the parser put a SourcePos
at each subexpression.
Expressions that don't come from the parser, however, will not have source locations, so their type can be ArithExpr Unit
.
Additionally, because all Lean functions have arguments, zeroargument functions in other languages can be represented as functions that take a Unit
argument.
In a return position, the Unit
type is similar to void
in languages derived from C.
In the C family, a function that returns void
will return control to its caller, but it will not return any interesting value.
By being an intentionally uninteresting value, Unit
allows this to be expressed without requiring a specialpurpose void
feature in the type system.
Unit's constructor can be written as empty parentheses: () : Unit
.
Empty
The Empty
datatype has no constructors whatsoever.
Thus, it indicates unreachable code, because no series of calls can ever terminate with a value at type Empty
.
Empty
is not used nearly as often as Unit
.
However, it is useful in some specialized contexts.
Many polymorphic datatypes do not use all of their type arguments in all of their constructors.
For instance, Sum.inl
and Sum.inr
each use only one of Sum
's type arguments.
Using Empty
as one of the type arguments to Sum
can rule out one of the constructors at a particular point in a program.
This can allow generic code to be used in contexts that have additional restrictions.
Naming: Sums, Products, and Units
Generally speaking, types that offer multiple constructors are called sum types, while types whose single constructor takes multiple arguments are called product types.
These terms are related to sums and products used in ordinary arithmetic.
The relationship is easiest to see when the types involved contain a finite number of values.
If α
and β
are types that contain n and k distinct values, respectively, then α ⊕ β
contains n + k distinct values and α × β
contains n × k distinct values.
For instance, Bool
has two values: true
and false
, and Unit
has one value: Unit.unit
.
The product Bool × Unit
has the two values (true, Unit.unit)
and (false, Unit.unit)
, and the sum Bool ⊕ Unit
has the three values Sum.inl true
, Sum.inl false
, and Sum.inr unit
.
Similarly, 2 × 1 = 2, and 2 + 1 = 3.
Messages You May Meet
Not all definable structures or inductive types can have the type Type
.
In particular, if a constructor takes an arbitrary type as an argument, then the inductive type must have a different type.
These errors usually state something about "universe levels".
For example, for this inductive type:
inductive MyType : Type where
 ctor : (α : Type) → α → MyType
Lean gives the following error:
invalid universe level in constructor 'MyType.ctor', parameter 'α' has type
Type
at universe level
2
it must be smaller than or equal to the inductive datatype universe level
1
A later chapter describes why this is the case, and how to modify definitions to make them work. For now, try making the type an argument to the inductive type as a whole, rather than to the constructor.
Similarly, if a constructor's argument is a function that takes the datatype being defined as an argument, then the definition is rejected. For example:
inductive MyType : Type where
 ctor : (MyType → Int) → MyType
yields the message:
(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared
For technical reasons, allowing these datatypes could make it possible to undermine Lean's internal logic, making it unsuitable for use as a theorem prover.
Forgetting an argument to an inductive type can also yield a confusing message.
For example, when the argument α
is not passed to MyType
in ctor
's type:
inductive MyType (α : Type) : Type where
 ctor : α → MyType
Lean replies with the following error:
type expected, got
(MyType : Type → Type)
The error message is saying that MyType
's type, which is Type → Type
, does not itself describe types.
MyType
requires an argument to become an actual honesttogoodness type.
The same message can appear when type arguments are omitted in other contexts, such as in a type signature for a definition:
inductive MyType (α : Type) : Type where
 ctor : α → MyType α
def ofFive : MyType := ctor 5
Exercises
 Write a function to find the last entry in a list. It should return an
Option
.  Write a function that finds the first entry in a list that satisfies a given predicate. Start the definition with
def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α :=
 Write a function
Prod.swap
that swaps the two fields in a pair. Start the definition withdef Prod.swap {α β : Type} (pair : α × β) : β × α :=
 Rewrite the
PetName
example to use a custom datatype and compare it to the version that usesSum
.  Write a function
zip
that combines two lists into a list of pairs. The resulting list should be as long as the shortest input list. Start the definition withdef zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
.  Write a polymorphic function
take
that returns the first n entries in a list, where n is aNat
. If the list contains fewer thann
entries, then the resulting list should be the input list.#eval take 3 ["bolete", "oyster"]
should yield["bolete", "oyster"]
, and#eval take 1 ["bolete", "oyster"]
should yield["bolete"]
.  Using the analogy between types and arithmetic, write a function that distributes products over sums. In other words, it should have type
α × (β ⊕ γ) → (α × β) ⊕ (α × γ)
.  Using the analogy between types and arithmetic, write a function that turns multiplication by two into a sum. In other words, it should have type
Bool × α → α ⊕ α
.
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.
PatternMatching 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 definition's type, in the form of 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 reused.
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 toplevel 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 toplevel 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 besteffort 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 matchexpression, 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
Patternmatching expressions, just like patternmatching 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.succ
s 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 multiplepattern 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 nonwhitespace characters are used to introduce the function, and its body consists of only three nonwhitespace 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)
.
Type the centered dot using \cdot
.
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:
10
while #eval (· * 2) 5
results in:
10
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
8
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 : Nat → Nat
#check NewNamespace.quadruple
NewNamespace.quadruple : 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
quadruple : Nat → Nat
Finally, namespaces may be opened for all following commands for the rest of the file.
To do this, simply omit the in
from a toplevel 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 patternmatching 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 lessthan sign <
and greaterthan 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.33774
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.
Summary
Evaluating Expressions
In Lean, computation occurs when expressions are evaluated.
This follows the usual rules of mathematical expressions: subexpressions are replaced by their values following the usual order of operations, until the entire expression has become a value.
When evaluating an if
or a match
, the expressions in the branches are not evaluated until the value of the condition or the match subject has been found.
Once they have been given a value, variables never change.
Similarly to mathematics but unlike most programming languages, Lean variables are simply placeholders for values, rather than addresses to which new values can be written.
Variables' values may come from global definitions with def
, local definitions with let
, as named arguments to functions, or from pattern matching.
Functions
Functions in Lean are firstclass values, meaning that they can be passed as arguments to other functions, saved in variables, and used like any other value.
Every Lean function takes exactly one argument.
To encode a function that takes more than one argument, Lean uses a technique called currying, where providing the first argument returns a function that expects the remaining arguments.
To encode a function that takes no arguments, Lean uses the Unit
type, which is the least informative possible argument.
There are three primary ways of creating functions:
 Anonymous functions are written using
fun
. For instance, a function that swaps the fields of aPoint
can be writtenfun (point : Point) => { x := point.y, y := point.x : Point}
 Very simple anonymous functions are written by placing one or more centered dots
·
inside of parentheses. Each centered dot becomes an argument to the function, and the parentheses delimit its body. For instance, a function that subtracts one from its argument can be written as(·  1)
instead of asfun x => x  1
.  Functions can be defined using
def
orlet
by adding an argument list or by using patternmatching notation.
Types
Lean checks that every expression has a type.
Types, such as Int
, Point
, {α : Type} → Nat → α → List α
, and Option (String ⊕ (Nat × String))
, describe the values that may eventually be found for an expression.
Like other languages, types in Lean can express lightweight specifications for programs that are checked by the Lean compiler, obviating the need for certain classes of unit test.
Unlike most languages, Lean's types can also express arbitrary mathematics, unifying the worlds of programming and theorem proving.
While using Lean for proving theorems is mostly out of scope for this book, Theorem Proving in Lean 4 contains more information on this topic.
Some expressions can be given multiple types.
For instance, 3
can be an Int
or a Nat
.
In Lean, this should be understood as two separate expressions, one with type Nat
and one with type Int
, that happen to be written in the same way, rather than as two different types for the same thing.
Lean is sometimes able to determine types automatically, but types must often be provided by the user.
This is because Lean's type system is so expressive.
Even when Lean can find a type, it may not find the desired type—3
could be intended to be used as an Int
, but Lean will give it the type Nat
if there are no further constraints.
In general, it is a good idea to write most types explicitly, only letting Lean fill out the very obvious types.
This improves Lean's error messages and helps make programmer intent more clear.
Some functions or datatypes take types as arguments. They are called polymorphic. Polymorphism allows programs such as one that calculates the length of a list without caring what type the entries in the list have. Because types are first class in Lean, polymorphism does not require any special syntax, so types are passed just like other arguments. Giving an argument a name in a function type allows later types to mention that argument, and the type of applying that function to an argument is found by replacing the argument's name with the argument's value.
Structures and Inductive Types
Brand new datatypes can be introduced to Lean using the structure
or inductive
features.
These new types are not considered to be equivalent to any other type, even if their definitions are otherwise identical.
Datatypes have constructors that explain the ways in which their values can be constructed, and each constructor takes some number of arguments.
Constructors in Lean are not the same as constructors in objectoriented languages: Lean's constructors are inert holders of data, rather than active code that initializes an allocated object.
Typically, structure
is used to introduce a product type (that is, a type with just one constructor that takes any number of arguments), while inductive
is used to introduce a sum type (that is, a type with many distinct constructors).
Datatypes defined with structure
are provided with one accessor function for each of the constructor's arguments.
Both structures and inductive datatypes may be consumed with pattern matching, which exposes the values stored inside of constructors using a subset of the syntax used to call said constructors.
Pattern matching means that knowing how to create a value implies knowing how to consume it.
Recursion
A definition is recursive when the name being defined is used in the definition itself. Because Lean is an interactive theorem prover in addition to being a programming language, there are certain restrictions placed on recursive definitions. In Lean's logical side, circular definitions could lead to logical inconsistency.
In order to ensure that recursive definitions do not undermine the logical side of Lean, Lean must be able to prove that all recursive functions terminate, no matter what arguments they are called with. In practice, this means either that recursive calls are all performed on a structurallysmaller piece of the input, which ensures that there is always progress towards a base case, or that users must provide some other evidence that the function always terminates. Similarly, recursive inductive types are not allowed to have a constructor that takes a function from the type as an argument, because this would make it possible to encode nonterminating functions.
Hello, World!
While Lean has been designed to have a rich interactive environment in which programmers can get quite a lot of feedback from the language without leaving the confines of their favorite text editor, it is also a language in which real programs can be written. This means that it also has a batchmode compiler, a build system, a package manager, and all the other tools that are necessary for writing programs.
While the previous chapter presented the basics of functional programming in Lean, this chapter explains how to start a programming project, compile it, and run the result. Programs that run and interact with their environment (e.g. by reading input from standard input or creating files) are difficult to reconcile with the understanding of computation as the evaluation of mathematical expressions. In addition to a description of the Lean build tools, this chapter also provides a way to think about functional programs that interact with the world.
Running a Program
The simplest way to run a Lean program is to use the run
option to the Lean executable.
Create a file called Hello.lean
and enter the following contents:
def main : IO Unit := IO.println "Hello, world!"
Then, from the command line, run:
lean run Hello.lean
The program displays Hello, world!
and exits.
Anatomy of a Greeting
When Lean is invoked with the run
option, it invokes the program's main
definition.
In programs that do not take commandline arguments, main
should have type IO Unit
.
This means that main
is not a function, because there are no arrows (→
) in its type.
Instead of a being a function that has side effects, main
consists of a description of effects to be carried out.
As discussed in the preceding chapter, Unit
is the simplest inductive type.
It has a single constructor called unit
that takes no arguments.
Languages in the C tradition have a notion of a void
function that does not return any value at all.
In Lean, all functions take an argument and return a value, and the lack of interesting arguments or return values can be signaled by using the Unit
type instead.
If Bool
represents a single bit of information, Unit
represents zero bits of information.
IO α
is the type of a program that, when executed, will either throw an exception or return a value of type α
.
During execution, this program may have side effects.
These programs are referred to as IO
actions.
Lean distinguishes between evaluation of expressions, which strictly adheres to the mathematical model of substitution of values for variables and reduction of subexpressions without side effects, and execution of IO
actions, which rely on an external system to interact with the world.
IO.println
is a function from strings to IO
actions that, when executed, write the given string to standard output.
Because this action doesn't read any interesting information from the environment in the process of emitting the string, IO.println
has type String → IO Unit
.
If it did return something interesting, then that would be indicated by the IO
action having a type other than Unit
.
Functional Programming vs Effects
Lean's model of computation is based on the evaluation of mathematical expressions, in which variables are given exactly one value that does not change over time. The result of evaluating an expression does not change, and evaluating the same expression again will always yield the same result.
On the other hand, useful programs must interact with the world. A program that performs neither input nor output can't ask a user for data, create files on disk, or open network connections. Lean is written in itself, and the Lean compiler certainly reads files, creates files, and interacts with text editors. How can a language in which the same expression always yields the same result support programs that read files from disk, when the contents of these files might change over time?
This apparent contradiction can be resolved by thinking a bit differently about side effects. Imagine a café that sells coffee and sandwiches. This café has two employees: a cook who fulfills orders, and a worker at the counter who interacts with customers and places order slips. The cook is a surly person, who really prefers not to have any contact with the world outside, but who is very good at consistently delivering the food and drinks that the café is known for. In order to do this, however, the cook needs peace and quiet, and can't be disturbed with conversation. The counter worker is friendly, but completely incompetent in the kitchen. Customers interact with the counter worker, who delegates all actual cooking to the cook. If the cook has a question for a customer, such as clarifying an allergy, they send a little note to the counter worker, who interacts with the customer and passes a note back to the cook with the result.
In this analogy, the cook is the Lean language.
When provided with an order, the cook faithfully and consistently delivers what is requested.
The counter worker is the surrounding runtime system that interacts with the world and can accept payments, dispense food, and have conversations with customers.
Working together, the two employees serve all the functions of the restaurant, but their responsibilities are divided, with each performing the tasks that they're best at.
Just as keeping customers away allows the cook to focus on making truly excellent coffee and sandwiches, Lean's lack of side effects allows programs to be used as part of formal mathematical proofs.
It also helps programmers understand the parts of the program in isolation from each other, because there are no hidden state changes that create subtle coupling between components.
The cook's notes represent IO
actions that are produced by evaluating Lean expressions, and the counter worker's replies are the values that are passed back from effects.
This model of side effects is quite similar to how the overall aggregate of the Lean language, its compiler, and its runtime system (RTS) work.
Primitives in the runtime system, written in C, implement all the basic effects.
When running a program, the RTS invokes the main
action, which returns new IO
actions to the RTS for execution.
The RTS executes these actions, delegating to the user's Lean code to carry out computations.
From the internal perspective of Lean, programs are free of side effects, and IO
actions are just descriptions of tasks to be carried out.
From the external perspective of the program's user, there is a layer of side effects that create an interface to the program's core logic.
RealWorld Functional Programming
The other useful way to think about side effects in Lean is by considering IO
actions to be functions that take the entire world as an argument and return a value paired with a new world.
In this case, reading a line of text from standard input is a pure function, because a different world is provided as an argument each time.
Writing a line of text to standard output is a pure function, because the world that the function returns is different from the one that it began with.
Programs do need to be careful to never reuse the world, nor to fail to return a new world—this would amount to time travel or the end of the world, after all.
Careful abstraction boundaries can make this style of programming safe.
If every primitive IO
action accepts one world and returns a new one, and they can only be combined with tools that preserve this invariant, then the problem cannot occur.
This model cannot be implemented. After all, the entire universe cannot be turned in to a Lean value and placed into memory. However, it is possible to implement a variation of this model with an abstract token that stands for the world. When the program is started, it is provided with a world token. This token is then passed on to the IO primitives, and their returned tokens are similarly passed to the next step. At the end of the program, the token is returned to the operating system.
This model of side effects is a good description of how IO
actions as descriptions of tasks to be carried out by the RTS are represented internally in Lean.
The actual functions that transform the real world are behind an abstraction barrier.
But real programs typically consist of a sequence of effects, rather than just one.
To enable programs to use multiple effects, there is a sublanguage of Lean called do
notation that allows these primitive IO
actions to be safely composed into a larger, useful program.
Combining IO
Actions
Most useful programs accept input in addition to producing output.
Furthermore, they may take decisions based on input, using the input data as part of a computation.
The following program, called HelloName.lean
, asks the user for their name and then greets them:
def main : IO Unit := do
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
In this program, the main
action consists of a do
block.
This block contains a sequence of statements, which can be both local variables (introduced using let
) and actions that are to be executed.
Just as SQL can be thought of as a specialpurpose language for interacting with databases, the do
syntax can be thought of as a specialpurpose sublanguage within Lean that is dedicated to modeling imperative programs.
IO
actions that are built with a do
block are executed by executing the statements in order.
This program can be run in the same manner as the prior program:
lean run HelloName.lean
If the user responds with David
, a session of interaction with the program reads:
How would you like to be addressed?
David
Hello, David!
The type signature line is just like the one for Hello.lean
:
def main : IO Unit := do
The only difference is that it ends with the keyword do
, which initiates a sequence of commands.
Each indented line following the keyword do
is part of the same sequence of commands.
The first two lines, which read:
let stdin ← IO.getStdin
let stdout ← IO.getStdout
retrieve the stdin
and stdout
handles by executing the library actions IO.getStdin
and IO.getStdout
, respectively.
In a do
block, let
has a slightly different meaning than in an ordinary expression.
Ordinarily, the local definition in a let
can be used in just one expression, which immediately follows the local definition.
In a do
block, local bindings introduced by let
are available in all statements in the remainder of the do
block, rather than just the next one.
Additionally, let
typically connects the name being defined to its definition using :=
, while some let
bindings in do
use a left arrow (←
or <
) instead.
Using an arrow means that the value of the expression is an IO
action that should be executed, with the result of the action saved in the local variable.
In other words, if the expression to the right of the arrow has type IO α
, then the variable has type α
in the remainder of the do
block.
IO.getStdin
and IO.getStdout
are IO
actions in order to allow stdin
and stdout
to be locally overridden in a program, which can be convenient.
If they were global variables as in C, then there would be no meaningful way to override them, but IO
actions can return different values each time they are executed.
The next part of the do
block is responsible for asking the user for their name:
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
The first line writes the question to stdout
, the second line requests input from stdin
, and the third line removes the trailing newline (plus any other trailing whitespace) from the input line.
The definition of name
uses :=
, rather than ←
, because String.dropRightWhile
is an ordinary function on strings, rather than an IO
action.
Finally, the last line in the program is:
stdout.putStrLn s!"Hello, {name}!"
It uses string interpolation to insert the provided name into a greeting string, writing the result to stdout
.
Step By Step
A do
block can be executed one line at a time.
Start with the program from the prior section:
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
Standard IO
The first line is let stdin ← IO.getStdin
, while the remainder is:
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
To execute a let
statement that uses a ←
, start by evaluating the expression to the right of the arrow (in this case, IO.getStdIn
).
Because this expression is just a variable, its value is looked up.
The resulting value is a builtin primitive IO
action.
The next step is to execute this IO
action, resulting in a value that represents the standard input stream, which has type IO.FS.Stream
.
Standard input is then associated with the name to the left of the arrow (here stdin
) for the remainder of the do
block.
Executing the second line, let stdout ← IO.getStdout
, proceeds similarly.
First, the expression IO.getStdout
is evaluated, yielding an IO
action that will return the standard output.
Next, this action is executed, actually returning the standard output.
Finally, this value is associated with the name stdout
for the remainder of the do
block.
Asking a Question
Now that stdin
and stdout
have been found, the remainder of the block consists of a question and an answer:
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
The first statement in the block, stdout.putStrLn "How would you like to be addressed?"
, consists of an expression.
To execute an expression, it is first evaluated.
In this case, IO.FS.Stream.putStrLn
has type IO.FS.Stream → String → IO Unit
.
This means that it is a function that accepts a stream and a string, returning an IO
action.
The expression uses accessor notation for a function call.
This function is applied to two arguments: the standard output stream and a string.
The value of the expression is an IO
action that will write the string and a newline character to the output stream.
Having found this value, the next step is to execute it, which causes the string and newline to actually be written to stdout
.
Statements that consist only of expressions do not introduce any new variables.
The next statement in the block is let input ← stdin.getLine
.
IO.FS.Stream.getLine
has type IO.FS.Stream → IO String
, which means that it is a function from a stream to an IO
action that will return a string.
Once again, this is an example of accessor notation.
This IO
action is executed, and the program waits until the user has typed a complete line of input.
Assume the user writes "David
".
The resulting line ("David\n"
) is associated with input
, where the escape sequence \n
denotes the newline character.
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
The next line, let name := input.dropRightWhile Char.isWhitespace
, is a let
statement.
Unlike the other let
statements in this program, it uses :=
instead of ←
.
This means that the expression will be evaluated, but the resulting value need not be an IO
action and will not be executed.
In this case, String.dropRightWhile
takes a string and a predicate over characters and returns a new string from which all the characters at the end of the string that satisfy the predicate have been removed.
For example,
#eval "Hello!!!".dropRightWhile (· == '!')
yields
"Hello"
and
#eval "Hello... ".dropRightWhile (fun c => not (c.isAlphanum))
yields
"Hello"
in which all nonalphanumeric characters have been removed from the right side of the string.
In the current line of the program, whitespace characters (including the newline) are removed from the right side of the input string, resulting in "David"
, which is associated with name
for the remainder of the block.
Greeting the User
All that remains to be executed in the do
block is a single statement:
stdout.putStrLn s!"Hello, {name}!"
The string argument to putStrLn
is constructed via string interpolation, yielding the string "Hello, David!"
.
Because this statement is an expression, it is evaluated to yield an IO
action that will print this string with a newline to standard output.
Once the expression has been evaluated, the resulting IO
action is executed, resulting in the greeting.
IO
Actions as Values
In the above description, it can be difficult to see why the distinction between evaluating expressions and executing IO
actions is necessary.
After all, each action is executed immediately after it is produced.
Why not simply carry out the effects during evaluation, as is done in other languages?
The answer is twofold.
First off, separating evaluation from execution means that programs must be explicit about which functions can have side effects.
Because the parts of the program that do not have effects are much more amenable to mathematical reasoning, whether in the heads of programmers or using Lean's facilities for formal proof, this separation can make it easier to avoid bugs.
Secondly, not all IO
actions need be executed at the time that they come into existence.
The ability to mention an action without carrying it out allows ordinary functions to be used as control structures.
For instance, the function twice
takes an IO
action as its argument, returning a new action that will execute the first one twice.
def twice (action : IO Unit) : IO Unit := do
action
action
For instance, executing
twice (IO.println "shy")
results in
shy
shy
being printed. This can be generalized to a version that runs the underlying action any number of times:
def nTimes (action : IO Unit) : Nat → IO Unit
 0 => pure ()
 n + 1 => do
action
nTimes action n
In the base case for Nat.zero
, the result is pure ()
.
The function pure
creates an IO
action that has no side effects, but returns pure
's argument, which in this case is the constructor for Unit
.
As an action that does nothing and returns nothing interesting, pure ()
is at the same time utterly boring and very useful.
In the recursive step, a do
block is used to create an action that first executes action
and then executes the result of the recursive call.
Executing nTimes (IO.println "Hello") 3
causes the following output:
Hello
Hello
Hello
In addition to using functions as control structures, the fact that IO
actions are firstclass values means that they can be saved in data structures for later execution.
For instance, the function countdown
takes a Nat
and returns a list of unexecuted IO
actions, one for each Nat
:
def countdown : Nat → List (IO Unit)
 0 => [IO.println "Blast off!"]
 n + 1 => IO.println s!"{n + 1}" :: countdown n
This function has no side effects, and does not print anything. For example, it can be applied to an argument, and the length of the resulting list of actions can be checked:
def from5 : List (IO Unit) := countdown 5
This list contains six elements (one for each number, plus a "Blast off!"
action for zero):
#eval from5.length
6
The function runActions
takes a list of actions and constructs a single action that runs them all in order:
def runActions : List (IO Unit) → IO Unit
 [] => pure ()
 act :: actions => do
act
runActions actions
Its structure is essentially the same as that of nTimes
, except instead of having one action that is executed for each Nat.succ
, the action under each List.cons
is to be executed.
Similarly, runActions
does not itself run the actions.
It creates a new action that will run them, and that action must be placed in a position where it will be executed as a part of main
:
def main : IO Unit := runActions from5
Running this program results in the following output:
5
4
3
2
1
Blast off!
What happens when this program is run?
The first step is to evaluate main
. That occurs as follows:
main
===>
runActions from5
===>
runActions (countdown 5)
===>
runActions
[IO.println "5",
IO.println "4",
IO.println "3",
IO.println "2",
IO.println "1",
IO.println "Blast off!"]
===>
do IO.println "5"
IO.println "4"
IO.println "3"
IO.println "2"
IO.println "1"
IO.println "Blast off!"
pure ()
The resulting IO
action is a do
block.
Each step of the do
block is then executed, one at a time, yielding the expected output.
The final step, pure ()
, does not have any effects, and it is only present because the definition of runActions
needs a base case.
Exercise
Step through the execution of the following program on a piece of paper:
def main : IO Unit := do
let englishGreeting := IO.println "Hello!"
IO.println "Bonjour!"
englishGreeting
While stepping through the program's execution, identify when an expression is being evaluated and when an IO
action is being executed.
When executing an IO
action results in a side effect, write it down.
After doing this, run the program with Lean and doublecheck that your predictions about the side effects were correct.
Starting a Project
As a program written in Lean becomes more serious, an aheadoftime compilerbased workflow that results in an executable becomes more attractive.
Like other languages, Lean has tools for building multiplefile packages and managing dependencies.
The standard Lean build tool is called Lake (short for "Lean Make"), and it is configured in Lean.
Just as Lean contains a specialpurpose language for writing programs with effects (the do
language), Lake contains a specialpurpose language for configuring builds.
These languages are referred to as embedded domainspecific languages (or sometimes domainspecific embedded languages, abbreviated EDSL or DSEL).
They are domainspecific in the sense that they are used for a particular purpose, with concepts from some subdomain, and they are typically not suitable for generalpurpose programming.
They are embedded because they occur inside another language's syntax.
While Lean contains rich facilities for creating EDSLs, they are beyond the scope of this book.
First steps
To get started with a project that uses Lake, the command lake new greeting
in a directory that does not already contain a file or directory called greeting
.
This creates a directory called greeting
that contains the following files:
Main.lean
is the file in which the Lean compiler will look for themain
action.Greeting.lean
is the scaffolding of a support library for the program.lakefile.lean
contains the configuration thatlake
needs to build the application.leantoolchain
contains an identifier for the specific version of Lean that is used for the project.
Additionally, lake new
initializes the project as a Git repository and configures its .gitignore
file to ignore intermediate build products.
Typically, the majority of the application logic will be in a collection of libraries for the program, while Main.lean
will contain a small wrapper around these pieces that does things like parsing command lines and executing the central application logic.
To create a project in an alreadyexisting directory, run lake init
instead of lake new
.
By default, the library file Greeting.lean
contains a single definition:
def hello := "world"
while the executable source Main.lean
contains:
import Greeting
def main : IO Unit :=
IO.println s!"Hello, {hello}!"
The import
line makes the contents of Greeting.lean
available in Main.lean
.
To build the package, run the command lake build
.
After a number of build commands scroll by, the resulting binary has been placed in build/bin
.
Running ./build/bin/greeting
results in Hello, world!
.
Lakefiles
A lakefile.lean
describes a package, which is a coherent collection of Lean code for distribution, analogous to an npm
or nuget
package or a Rust crate.
A package may contain any number of libraries or executables.
While the documentation for Lake describes the available options in a lakefile, it makes use of a number of Lean features that have not yet been described here.
The generated lakefile.lean
contains the following:
import Lake
open Lake DSL
package greeting {
 add package configuration options here
}
lean_lib Greeting {
 add library configuration options here
}
@[default_target]
lean_exe greeting {
root := `Main
}
This initial Lakefile consists of three items:
 a package declaration, named
greeting
,  a library declaration, named
Greeting
, and  an executable, also named
greeting
.
Each Lakefile will contain exactly one package, but any number of libraries or executables.
Additionally, Lakefiles may contain external libraries, which are libraries not written in Lean to be statically linked with the resulting executable, custom targets, which are build targets that don't fit naturally into the library/executable taxonomy, dependencies, which are declarations of other Lean packages (either locally or from remote Git repositories), and scripts, which are essentially IO
actions (similar to main
), but that additionally have access to metadata about the package configuration.
The items in the Lakefile allow things like source file locations, module hierarchies, and compiler flags to be configured.
Generally speaking, however, the defaults are reasonable.
Libraries, executables, and custom targets are all called targets.
By default, lake build
builds those targets that are annotated with @[default_target]
.
This annotation is an attribute, which is metadata that can be associated with a Lean declaration.
Attributes are similar to Java annotations or C# and Rust attributes.
They are used pervasively throughout Lean.
To build a target that is not annotated with @[default_target]
, specify the target's name as an argument after lake build
.
Libraries and Imports
A Lean library consists of a hierarchically organized collection of source files from which names can be imported, called modules.
By default, a library has a single root file that matches its name.
In this case, the root file for the library Greeting
is Greeting.lean
.
The first line of Main.lean
, which is import Greeting
, makes the contents of Greeting.lean
available in Main.lean
.
Additional module files may be added to the library by creating a directory called Greeting
and placing them inside.
These names can be imported by replacing the directory separator with a dot.
For instance, creating the file Greeting/Smile.lean
with the contents:
def expression : String := "a big smile"
means that Main.lean
can use the definition as follows:
import Greeting
import Greeting.Smile
def main : IO Unit :=
IO.println s!"Hello, {hello}, with {expression}!"
The module name hierarchy is decoupled from the namespace hierarchy.
In Lean, modules are units of code distribution, while namespaces are units of code organization.
That is, names defined in the module Greeting.Smile
are not automatically in a corresponding namespace Greeting.Smile
.
Modules may place names into any namespace they like, and the code that imports them may open
the namespace or not.
import
is used to make the contents of a source file available, while open
makes names from a namespace available in the current context.
In the Lakefile, the line import Lake
makes the contents of the Lake
module available, while the line open Lake DSL
makes the contents of the Lake
and DSL
namespaces available without any prefixes.
The Lake
module places names into both the Lake
and DSL
namespaces.
Worked Example: cat
The standard Unix utility cat
takes a number of commandline options, followed by a zero or more input files.
If no files are provided, or if one of them is a dash (
), then it takes the standard input as the corresponding input instead of reading a file.
The contents of the inputs are written, one after the other, to the standard output.
If a specified input file does not exist, this is noted on standard error, but cat
continues concatenating the remaining inputs.
A nonzero exit code is returned if any of the input files do not exist.
This section describes a simplified version of cat
, called feline
.
Unlike commonlyused versions of cat
, feline
has no commandline options for features such as numbering lines, indicating nonprinting characters, or displaying help text.
Furthermore, it cannot read more than once from a standard input that's associated with a terminal device.
To get the most benefit from this section, follow along yourself. It's OK to copypaste the code examples, but it's even better to type them in by hand. This makes it easier to learn the mechanical process of typing in code, recovering from mistakes, and interpreting feedback from the compiler.
Getting started
The first step in implementing feline
is to create a package and decide how to organize the code.
In this case, because the program is so simple, all the code will be placed in Main.lean
.
The first step is to run lake new feline
.
Edit the Lakefile to remove the library, and delete the generated library code and the reference to it from Main.lean
.
Once this has been done, lakefile.lean
should contain:
import Lake
open Lake DSL
package feline {
 add package configuration options here
}
@[default_target]
lean_exe feline {
root := `Main
}
and Main.lean
should contain something like:
def main : IO Unit :=
IO.println s!"Hello, cats!"
Ensure that the code can be built by running lake build
.
Concatenating Streams
Now that the basic skeleton of the program has been built, it's time to actually enter the code.
A proper implementation of cat
can be used with infinite IO streams, such as /dev/random
, which means that it can't read its input into memory before outputting it.
Furthermore, it should not work one character at a time, as this leads to frustratingly slow performance.
Instead, it's better to read contiguous blocks of data all at once, directing the data to the standard output one block at a time.
The first step is to decide how big of a block to read.
For the sake of simplicity, this implementation uses a conservative 20 kilobyte block.
USize
is analogous to size_t
in C—it's an unsigned integer type that is big enough to represent all valid array sizes.
def bufsize : USize := 20 * 1024
Streams
The main work of feline
is done by dump
, which reads input one block at a time, dumping the result to standard output, until the end of the input has been reached:
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
let stdout ← IO.getStdout
stdout.write buf
dump stream
The dump
function is declared partial
, because it calls itself recursively on input that is not immediately smaller than an argument.
When a function is declared to be partial, Lean does not require a proof that it terminates.
On the other hand, partial functions are also much less amenable to proofs of correctness, because allowing infinite loops in Lean's logic would make it unsound.
However, there is no way to prove that dump
terminates, because infinite input (such as from /dev/random
) would mean that it does not, in fact, terminate.
In cases like this, there is no alternative to declaring the function partial
.
The type IO.FS.Stream
represents a POSIX stream.
Behind the scenes, it is represented as a structure that has one field for each POSIX stream operation.
Each operation is represented as an IO action that provides the corresponding operation:
structure Stream where
flush : IO Unit
read : USize → IO ByteArray
write : ByteArray → IO Unit
getLine : IO String
putStr : String → IO Unit
The Lean compiler contains IO
actions (such as IO.getStdout
, which is called in dump
) to get streams that represent standard input, standard output, and standard error.
These are IO
actions rather than ordinary definitions because Lean allows these standard POSIX streams to be replaced in a process, which makes it easier to do things like capturing the output from a program into a string by writing a custom IO.FS.Stream
.
The control flow in dump
is essentially a while
loop.
When dump
is called, if the stream has reached the end of the file, pure ()
terminates the function by returning the constructor for Unit
.
If the stream has not yet reached the end of the file, one block is read, and its contents are written to stdout
, after which dump
calls itself directly.
The recursive calls continue until stream.read
returns an empty byte array, which indicates that the end of the file has been reached.
When an if
expression occurs as a statement in a do
, as in dump
, each branch of the if
is implicitly provided with a do
.
In other words, the sequence of steps following the else
are treated as a sequence of IO
actions to be executed, just as if they had a do
at the beginning.
Names introduced with let
in the branches of the if
are visible only in their own branches, and are not in scope outside of the if
.
There is no danger of running out of stack space while calling dump
because the recursive call happens as the very last step in the function, and its result is returned directly rather than being manipulated or computed with.
This kind of recursion is called tail recursion, and will be described in more detail later in this book.
Because the compiled code does not need to retain any state, the Lean compiler can compile the recursive call to a jump.
If feline
only redirected standard input to standard output, then dump
would be sufficient.
However, it also needs to be able to open files that are provided as commandline arguments and emit their contents.
When its argument is the name of a file that exists, fileStream
returns a stream that reads the file's contents.
When the argument is not a file, fileStream
emits an error and returns none
.
def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
let fileExists ← filename.pathExists
if not fileExists then
let stderr ← IO.getStderr
stderr.putStrLn s!"File not found: {filename}"
pure none
else
let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
pure (some (IO.FS.Stream.ofHandle handle))
Opening a file as a stream takes two steps.
First, a file handle is created by opening the file in read mode.
A Lean file handle tracks an underlying file descriptor.
When there are no references to the file handle value, a finalizer closes the file descriptor.
Second, the file handle is given the same interface as a POSIX stream using IO.FS.Stream.ofHandle
, which fills each field of the Stream
structure with the corresponding IO
action that works on file handles.
Handling Input
The main loop of feline
is another tailrecursive function, called process
.
In order to return a nonzero exit code if any of the inputs could not be read, process
takes an argument exitCode
that represents the current exit code for the whole program.
Additionally, it takes a list of input files to be processed.
def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
match args with
 [] => pure exitCode
 "" :: args =>
let stdin ← IO.getStdin
dump stdin
process exitCode args
 filename :: args =>
let stream ← fileStream ⟨filename⟩
match stream with
 none =>
process 1 args
 some stream =>
dump stream
process exitCode args
Just as with if
, each branch of a match
that is used as a statement in a do
is implicitly provided with its own do
.
There are three possibilities.
One is that no more files remain to be processed, in which case process
returns the error code unchanged.
Another is that the specified filename is ""
, in which case process
dumps the contents of the standard input and then processes the remaining filenames.
The final possibility is that an actual filename was specified.
In this case, fileStream
is used to attempt to open the file as a POSIX stream.
Its argument is encased in ⟨ ... ⟩
because a FilePath
is a singlefield structure that contains a string.
If the file could not be opened, it is skipped, and the recursive call to process
sets the exit code to 1
.
If it could, then it is dumped, and the recursive call to process
leaves the exit code unchanged.
process
does not need to be marked partial
because it is structurally recursive.
Each recursive call is provided with the tail of the input list, and all Lean lists are finite.
Thus, process
does not introduce any nontermination itself.
Main
The final step is to write the main
action.
Unlike prior examples, main
in feline
is a function.
In Lean, main
can have one of three types:
main : IO Unit
corresponds to programs that cannot read their commandline arguments and always indicate success with an exit code of0
,main : IO UInt32
corresponds toint main(void)
in C, for programs without arguments that return exit codes, andmain : List String → IO UInt32
corresponds toint main(int argc, char **argv)
in C, for programs that take arguments and signal success or failure.
If no arguments were provided, feline
should read from standard input as if it were called with a single ""
argument.
Otherwise, the arguments should be processed one after the other.
def main (args : List String) : IO UInt32 :=
match args with
 [] => process 0 [""]
 _ => process 0 args
Meow!
To check whether feline
works, the first step is to build it with lake build
.
First off, when called without arguments, it should emit what it receives from standard input.
Check that
echo "It works!"  ./build/bin/feline
emits It works!
.
Secondly, when called with files as arguments, it should print them.
If the file test1.txt
contains
It's time to find a warm spot
and test2.txt
contains
and curl up!
then the command
./build/bin/feline test1.txt test2.txt
should emit
It's time to find a warm spot
and curl up!
Finally, the 
argument should be handled appropriately.
echo "and purr"  ./build/bin/feline test1.txt  test2.txt
should yield
It's time to find a warm spot
and purr
and curl up!
Exercise
Extend feline
with support for usage information.
The extended version should accept a commandline argument help
that causes documentation about the available commandline options to be written to standard output.
Additional Conveniences
Nested Actions
Many of the functions in feline
exhibit a repetitive pattern in which an IO
action's result is given a name, and then used immediately and only once.
For instance, in dump
:
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
let stdout ← IO.getStdout
stdout.write buf
dump stream
the pattern occurs for stdout
:
let stdout ← IO.getStdout
stdout.write buf
Similarly, fileStream
contains the following snippet:
let fileExists ← filename.pathExists
if not fileExists then
When Lean is compiling a do
block, expressions that consist of a left arrow immediately under parentheses are lifted to the nearest enclosing do
, and their results are bound to a unique name.
This unique name replaces the origin of the expression.
This means that dump
can also be written as follows:
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
(← IO.getStdout).write buf
dump stream
This version of dump
avoids introducing names that are used only once, which can greatly simplify a program.
IO
actions that Lean lifts from a nested expression context are called nested actions.
fileStream
can be simplified using the same technique:
def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
if not (← filename.pathExists) then
(← IO.getStderr).putStrLn s!"File not found: {filename}"
pure none
else
let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
pure (some (IO.FS.Stream.ofHandle handle))
In this case, the local name of handle
could also have been eliminated using nested actions, but the resulting expression would have been long and complicated.
Even though it's often good style to use nested actions, it can still sometimes be helpful to name intermediate results.
It is important to remember, however, that nested actions are only a shorter notation for IO
actions that occur in a surrounding do
block.
The side effects that are involved in executing them still occur in the same order, and execution of side effects is not interspersed with the evaluation of expressions.
For an example of where this might be confusing, consider the following helper definitions that return data after announcing to the world that they have been executed:
def getNumA : IO Nat := do
(← IO.getStdout).putStrLn "A"
pure 5
def getNumB : IO Nat := do
(← IO.getStdout).putStrLn "B"
pure 7
These definitions are intended to stand in for more complicated IO
code that might validate user input, read a database, or open a file.
A program that prints 0
when number A is five, or number B
otherwise, can be written as follows:
def test : IO Unit := do
let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
(← IO.getStdout).putStrLn s!"The answer is {a}"
However, this program probably has more side effects (such as prompting for user input or reading a database) than was intended.
The definition of getNumA
makes it clear that it will always return 5
, and thus the program should not read number B.
However, running the program results in the following output:
A
B
The answer is 0
getNumB
was executed because test
is equivalent to this definition:
def test : IO Unit := do
let x ← getNumA
let y ← getNumB
let a : Nat := if x == 5 then 0 else y
(← IO.getStdout).putStrLn s!"The answer is {a}"
This is due to the rule that nested actions are lifted to the closest enclosing do
block.
The branches of the if
were not implicitly wrapped in do
blocks because the if
is not itself a statement in the do
block—the statement is the let
that defines a
.
Indeed, they could not be wrapped this way, because the type of the conditional expression is Nat
, not IO Nat
.
Flexible Layouts for do
In Lean, do
expressions are whitespacesensitive.
Each IO
action or local binding in the do
is expected to start on its own line, and they should all have the same indentation.
Almost all uses of do
should be written this way.
In some rare contexts, however, manual control over whitespace and indentation may be necessary, or it may be convenient to have multiple small actions on a single line.
In these cases, newlines can be replaced with a semicolon and indentation can be replaced with curly braces.
For instance, all of the following programs are equivalent:
 This version uses only whitespacesensitive layout
def main : IO Unit := do
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
 This version is as explicit as possible
def main : IO Unit := do {
let stdin ← IO.getStdin;
let stdout ← IO.getStdout;
stdout.putStrLn "How would you like to be addressed?";
let name := (← stdin.getLine).dropRightWhile Char.isWhitespace;
stdout.putStrLn s!"Hello, {name}!"
}
 This version uses a semicolon to put two actions on the same line
def main : IO Unit := do
let stdin ← IO.getStdin; let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
Idiomatic Lean code uses curly braces with do
very rarely.
Running IO
Actions With #eval
Lean's #eval
command can be used to execute IO
actions, rather than just evaluating them.
Normally, adding a #eval
command to a Lean file causes Lean to evaluate the provided expression, convert the resulting value to a string, and provide that string as a tooltip and in the info window.
Rather than failing because IO
actions can't be converted to strings, #eval
executes them, carrying out their side effects.
If the result of execution is the Unit
value ()
, then no result string is shown, but if it is a type that can be converted to a string, then Lean displays the resulting value.
This means that, given the prior definitions of countdown
and runActions
,
#eval runActions (countdown 3)
displays
3
2
1
Blast off!
This is the output produced by running the IO
action, rather than some opaque representation of the action itself.
In other words, for IO
actions, #eval
both evaluates the provided expression and executes the resulting action value.
Quickly testing IO
actions with #eval
can be much more convenient that compiling and running whole programs.
However, there are some limitations.
For instance, reading from standard input simply returns empty input.
Additionally, the IO
action is reexecuted whenever Lean needs to update the diagnostic information that it provides to users, and this can happen at unpredictable times.
An action that reads and writes files, for instance, may do so at inconvenient times.
Summary
Evaluation vs Execution
Side effects are aspects of program execution that go beyond the evaluation of mathematical expressions, such as reading files, throwing exceptions, or triggering industrial machinery.
While most language allow side effects to occur during evaluation, Lean does not.
Instead, Lean has a type called IO
that represents descriptions of programs that use side effects.
These descriptions are then executed by the language's runtime system, which invokes the Lean expression evaluator to carry out specific computations.
Values of type IO α
are called IO
actions.
The simplest is pure
, which returns its argument and has no actual side effects.
IO
actions can also be understood as functions that take the whole world as an argument and return a new world in which the side effect has occurred.
Behind the scenes, the IO
library ensures that the world is never duplicated, created, or destroyed.
While this model of side effects cannot actually be implemented, as the whole universe is too big to fit in memory, the real world can be represented by a token that is passed around through the program.
An IO
action main
is executed when the program starts.
main
can have one of three types:
main : IO Unit
is used for simple programs that cannot read their commandline arguments and always return exit code0
,main : IO UInt32
is used for programs without arguments that may signal success or failure, andmain : List String → IO UInt32
is used for programs that take commandline arguments and signal success or failure.
do
Notation
The Lean standard library provides a number of basic IO
actions that represent effects such as reading from and writing to files and interacting with standard input and standard output.
These base IO
actions are composed into larger IO
actions using do
notation, which is a builtin domainspecific language for writing descriptions of programs with side effects.
A do
expression contains a sequence of statements, which may be:
 expressions that represent
IO
actions,  ordinary local definitions with
let
and:=
, where the defined name refers to the value of the provided expression, or  local definitions with
let
and←
, where the defined name refers to the result of executing the value of the provided expression.
IO
actions that are written with do
are executed one statement at a time.
Furthermore, if
and match
expressions that occur immediately under a do
are implicitly considered to have their own do
in each branch.
Inside of a do
expression, nested actions are expressions with a left arrow immediately under parentheses.
The Lean compiler implicitly lifts them to the nearest enclosing do
, which may be implicitly part of a branch of a match
or if
expression, and given a unique name.
This unique name then replaces the origin site of the nested action.
Compiling and Running Programs
A Lean program that consists of a single file with a main
definition can be run using lean run FILE
.
While this can be a nice way to get started with a simple program, most programs will eventually graduate to a multiplefile project that should be compiled before running.
Lean projects are organized into packages, which are collections of libraries and executables together with information about dependencies and a build configuration.
Packages are described using Lake, a Lean build tool.
Use lake new
to create a Lake package in a new directory, or lake init
to create one in the current directory.
Lake package configuration is another domainspecific language.
Use lake build
to build a project.
Partiality
One consequence of following the mathematical model of expression evaluation is that every expression must have a value.
This rules out both incomplete pattern matches that fail to cover all constructors of a datatype and programs that can fall into an infinite loop.
Lean ensures that all match
expressions cover all cases, and that all recursive functions are either structurally recursive or have an explicit proof of termination.
However, some real programs require the possibility of looping infinitely, because they handle potentiallyinfinite data, such as POSIX streams.
Lean provides an escape hatch: functions whose definition is marked partial
are not required to terminate.
This comes at a cost.
Because types are a firstclass part of the Lean language, functions can return types.
Partial functions, however, are not evaluated during type checking, because an infinite loop in a function could cause the type checker to enter an infinite loop.
Furthermore, mathematical proofs are unable to inspect the definitions of partial functions, which means that programs that use them are much less amenable to formal proof.
Interlude: Propositions, Proofs, and Indexing
Like many languages, Lean uses square brackets for indexing into arrays and lists.
For instance, if woodlandCritters
is defined as follows:
def woodlandCritters : List String :=
["hedgehog", "deer", "snail"]
then the individual components can be extracted:
def hedgehog := woodlandCritters[0]
def deer := woodlandCritters[1]
def snail := woodlandCritters[2]
However, attempting to extract the fourth element results in a compiletime error, rather than a runtime error:
def oops := woodlandCritters[3]
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 perfomed, 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
⊢ 3 < List.length woodlandCritters
This error message is saying Lean tried to automatically mathematically prove that 3 < List.length woodlandCritters
, which would mean that the lookup was safe, but that it could not do so.
Outofbounds errors are a common class of bugs, and Lean uses its dual nature as a programming language and a theorem prover to rule out as many as possible.
Understanding how this works requires an understanding of three key ideas: propositions, proofs, and tactics.
Propositions and Proofs
A proposition is a statement that can be true or false. All of the following are propositions:
 1 + 1 = 2
 Addition is commutative
 There are infinitely many prime numbers
 1 + 1 = 15
 Paris is the capital of France
 Buenos Aires is the capital of South Korea
 All birds can fly
On the other hand, nonsense statements are not propositions. None of the following are propositions:
 1 + green = ice cream
 All capital cities are prime numbers
 At least one gorg is a fleep
Propositions come in two varieties: those that are purely mathematical, relying only on our definitions of concepts, and those that are facts about the world. Theorem provers like Lean are concerned with the former category, and have nothing to say about the flight capabilities of penguins or the legal status of cities.
A proof is a convincing argument that a proposition is true. For mathematical propositions, these arguments make use of the definitions of the concepts that are involved as well as the rules of logical argumentation. Most proofs are written for people to understand, and leave out many tedious details. Computeraided theorem provers like Lean are designed to allow mathematicians to write proofs while omitting many details, while the software fills in the missing explicit steps, decreasing the likelihood of oversights or mistakes.
In Lean, a program's type describes the ways it can be interacted with.
For instance, a program of type Nat → List String
is a function that takes a Nat
argument and produces a list of strings.
In other words, each type specifies what counts as a program with that type.
In Lean, propositions are a kind of type that describes what counts as evidence that it is true. The proposition is proved by providing this evidence. On the other hand, if the proposition is false, then it will be impossible to construct this evidence.
For example, the proposition "1 + 1 = 2" can be written directly in Lean.
The evidence for this proposition is the constructor rfl
, which is short for reflexivity:
def onePlusOneIsTwo : 1 + 1 = 2 := rfl
On the other hand, rfl
does not prove the false proposition "1 + 1 = 15":
def onePlusOneIsFifteen : 1 + 1 = 15 := rfl
type mismatch
rfl
has type
1 + 1 = 1 + 1 : Prop
but is expected to have type
1 + 1 = 15 : Prop
This error message indicates that rfl
can prove that two expressions are equal when both sides of the equality statement are already the same number.
Because 1 + 1
evaluates directly to 2
, they are considered to be the same, which allows onePlusOneIsTwo
to be accepted.
Just as Type
describes types such as Nat
, String
, and List (Nat × String × (Int → Float))
that represent data structures and functions, Prop
describes propositions.
When a proposition has been proven, it is called a theorem.
In Lean, it is conventional to declare theorems with the theorem
keyword instead of def
.
This helps readers see which declarations are intended to be read as mathematical proofs, and which are definitions.
Generally speaking, with a proof, what matters is that there is evidence that a proposition is true, but it's not particularly important which evidence was provided.
With definitions, on the other hand, it matters very much which particular value is selected—after all, a definition of addition that always returns 0
is clearly wrong.
The prior example could be rewritten as follows:
def OnePlusOneIsTwo : Prop := 1 + 1 = 2
theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl
Tactics
Proofs are normally written using tactics, rather than by providing evidence directly. Tactics are small programs that construct evidence for a proposition. These programs run in a proof state that tracks the statement that is to be proved (called the goal) along with the assumptions that are available to prove it. Running a tactic on a goal results in a new proof state that contains new goals. The proof is complete when all goals have been proven.
To write a proof with tactics, begin the definition with by
.
Writing by
puts Lean into tactic mode until the end of the next indented block.
While in tactic mode, Lean provides ongoing feedback about the current proof state.
Written with tactics, onePlusOneIsTwo
is still quite short:
theorem onePlusOneIsTwo : 1 + 1 = 2 := by
simp
The simp
tactic, short for "simplify", is the workhorse of Lean proofs.
It rewrites the goal to as simple a form as possible, taking care of parts of the proof that are small enough.
In particular, it proves simple equality statements.
Behind the scenes, a detailed formal proof is constructed, but using simp
hides this complexity.
Tactics are useful for a number of reasons:
 Many proofs are complicated and tedious when written out down to the smallest detail, and tactics can automate these uninteresting parts.
 Proofs written with tactics are easier to maintain over time, because flexible automation can paper over small changes to definitions.
 Because a single tactic can prove many different theorems, Lean can use tactics behind the scenes to free users from writing proofs by hand. For instance, an array lookup requires a proof that the index is in bounds, and a tactic can typically construct that proof without the user needing to worry about it.
Behind the scenes, indexing notation uses a tactic to prove that the user's lookup operation is safe.
This tactic is simp
, configured to take certain arithmetic identities into account.
Connectives
The basic building blocks of logic, such as "and", "or", "true", "false", and "not", are called logical connectives. Each connective defines what counts as evidence of its truth. For example, to prove a statement "A and B", one must prove both A and B. This means that evidence for "A and B" is a pair that contains both evidence for A and evidence for B. Similarly, evidence for "A or B" consists of either evidence for A or evidence for B.
In particular, most of these connectives are defined like datatypes, and they have constructors.
If A
and B
are propositions, then "A
and B
" (written A ∧ B
) is a proposition.
Evidence for A ∧ B
consists of the constructor And.intro
, which has the type A → B → A ∧ B
.
Replacing A
and B
with concrete propositions, it is possible to prove 1 + 1 = 2 ∧ "Str".append "ing" = "String"
with And.intro rfl rfl
.
Of course, simp
is also powerful enough to find this proof:
theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by simp
Similarly, "A
or B
" (written A ∨ B
) has two constructors, because a proof of "A
or B
" requires only that one of the two underlying propositions be true.
There are two constructors: Or.inl
, with type A → A ∨ B
, and Or.inr
, with type B → A ∨ B
.
Implication (if A then B) is represented using functions.
In particular, a function that transforms evidence for A into evidence for B is itself evidence that A implies B.
This is different from the usual description of implication, in which A → B
is shorthand for ¬A ∨ B
, but the two formulations are equivalent.
Because evidence for an "and" is a constructor, it can be used with pattern matching. For instance, a proof that A and B implies A or B is a function that pulls the evidence of A (or of B) out of the evidence for A and B, and then uses this evidence to produce evidence of A or B:
theorem andImpliesOr : A ∧ B → A ∨ B :=
fun andEvidence =>
match andEvidence with
 And.intro a b => Or.inl a
Connective  Lean Syntax  Evidence 

True  True  True.intro : True 
False  False  No evidence 
A and B  A ∧ B  And.intro : A → B → A ∧ B 
A or B  A ∨ B  Either Or.inl : A → A ∨ B or Or.inr : B → A ∨ B 
A implies B  A → B  A function that transforms evidence of A into evidence of B 
not A  ¬A  A function that would transform evidence of A into evidence of False 
The simp
tactic can prove theorems that use these connectives.
For example:
theorem onePlusOneAndLessThan : 1 + 1 = 2 ∨ 3 < 5 := by simp
theorem notTwoEqualFive : ¬(1 + 1 = 5) := by simp
theorem trueIsTrue : True := True.intro
theorem trueOrFalse : True ∨ False := by simp
theorem falseImpliesTrue : False → True := by simp
Evidence as Arguments
While simp
does a great job proving propositions that involve equalities and inequalities of specific numbers, it is not very good at proving statements that involve variables.
For instance, simp
can prove that 4 < 15
, but it can't easily tell that because x < 4
, it's also true that x < 15
.
Because index notation uses simp
behind the scenes to prove that array access is safe, it can require a bit of handholding.
One of the easiest ways to make indexing notation work well is to have the function that performs a lookup into a data structure take the required evidence of safety as an argument. For instance, a function that returns the third entry in a list is not generally safe because lists might contain zero, one, or two entries:
def third (xs : List α) : α := xs[2]
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 perfomed, 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
α : Type ?u.3872
xs : List α
⊢ 2 < List.length xs
However, the obligation to show that the list has at least three entries can be imposed on the caller by adding an argument that consists of evidence that the indexing operation is safe:
def third (xs : List α) (ok : xs.length > 2) : α := xs[2]
When the function is called on a concrete list, its length is known.
In these cases, by simp
can construct the evidence automatically:
#eval third woodlandCritters (by simp)
"snail"
Indexing Without Evidence
In cases where it's not practical to prove that an indexing operation is in bounds, there are other alternatives.
Adding an question mark results in an Option
, where the result is some
if the index is in bounds, and none
otherwise.
For example:
def thirdOption (xs : List α) : Option α := xs[2]?
#eval thirdOption woodlandCritters
some "snail"
#eval thirdOption ["only", "two"]
none
There is also a version that crashes the program when the index is out of bounds:
#eval woodlandCritters[1]!
"deer"
Be careful!
Because code that is run with #eval
runs in the context of the Lean compiler, selecting the wrong index can crash your IDE.
Messages You May Meet
In addition to the error that occurs when Lean is unable to find compiletime evidence that an indexing operation is safe, polymorphic functions that use unsafe indexing may produce the following message:
def unsafeThird (xs : List α) : α := xs[2]!
failed to synthesize instance
Inhabited α
This is due to a technical restriction that is part of keeping Lean usable as both a logic for proving theorems and a programming language. In particular, only programs whose types contain at least one value are allowed to crash. This is because a proposition in Lean is a kind of type that classifies evidence of its truth. False propositions have no such evidence. If a program with an empty type could crash, then that crashing program could be used as a kind of fake evidence for a false proposition.
Internally, Lean contains a table of types that are known to have at least one value.
This error is saying that some arbitrary type α
is not necessarily in that table.
The next chapter describes how to add to this table, and how to successfully write functions like unsafeThird
.
Adding whitespace between a list and the brackets used for lookup can cause another message:
#eval woodlandCritters [1]
function expected at
woodlandCritters
term has type
List String
Adding a space causes Lean to treat the expression as a function application, and the index as a list that contains a single number.
This error message results from having Lean attempt to treat woodlandCritters
as a function.
Exercises
 Prove the following theorems using
rfl
:2 + 3 = 5
,15  8 = 7
,"Hello, ".append "world" = "Hello, world"
,5 < 18
.  Prove the following theorems using
by simp
:2 + 3 = 5
,15  8 = 7
,"Hello, ".append "world" = "Hello, world"
,5 < 18
.  Write a function that looks up the fifth entry in a list. Pass the evidence that this lookup is safe as an argument to the function.
Overloading and Type Classes
In many languages, the builtin datatypes get special treatment.
For example, in C and Java, +
can be used to add float
s and int
s, but not arbitraryprecision numbers from a thirdparty library.
Similarly, numeric literals can be used directly for the builtin types, but not for userdefined number types.
Other languages provide an overloading mechanism for operators, where the same operator can be given a meaning for a new type.
In these languages, such as C++ and C#, a wide variety of builtin operators can be overloaded, and the compiler uses the type checker to select a particular implementation.
In addition to numeric literals and operators, many languages allow overloading of functions or methods. In C++, Java, C# and Kotlin, multiple implementations of a method are allowed, with differing numbers and types of arguments. The compiler uses the number of arguments and their types to determine which overload was intended.
Function and operator overloading has a key limitation: polymorphic functions can't restrict their type arguments to types for which a given overload exists. That is, there is no way to write a function that works for any type that has addition defined. Instead, this function must itself be overloaded for each type that has addition, resulting in many boilerplate definitions instead of a single polymorphic definition. Another consequence of this restriction is that some operators (such as equality in Java) end up being defined for every combination of arguments, even when it is not necessarily sensible to do so. If programmers are not very careful, this can lead to programs that crash at runtime or silently compute an incorrect result.
Lean implements overloading using a mechanism called type classes, pioneered in Haskell, that allows overloading of operators, functions, and literals in a manner that works well with polymorphism.
A type class describes a collection of overloadable operations.
To overload these operations for a new type, an instance is created that contains an implementation of each operation for the new type.
For example, a type class named Add
describes types that allow addition, and an instance of Add
for Nat
provides an implementation of addition for Nat
.
The terms class and instance can be confusing for those who are used to objectoriented languages, because they are not closely related to classes and instances in objectoriented languages. However, they do share common roots: in everyday language, the term "class" refers to a group that shares some common attributes. While classes in objectoriented programming certainly describe groups of objects with common attributes, the term additionally refers to a specific mechanism in a programming language for describing such a group. Type classes are also a means of describing types that share common attributes (namely, implementations of certain operations), but they don't really have anything else in common with classes as found in objectoriented programming. A Lean type class is much more analogous to a Java or C# interface. Similarly, instances of type classes describe how to implement a given interface for a type, while the term "instance" is used to describe values with a given type in objectoriented programming.
Positive Numbers
In some applications, only positive numbers make sense. For example, compilers and interpreters typically use oneindexed line and column numbers for source positions, and a datatype that represents only nonempty lists will never report a length of zero. Rather than relying on natural numbers, and littering the code with assertions that the number is not zero, it can be useful to design a datatype that represents only positive numbers.
One way to represent positive numbers is very similar to Nat
, except with one
as the base case instead of zero
:
inductive Pos : Type where
 one : Pos
 succ : Pos → Pos
This datatype represents exactly the intended set of values, but it is not very convenient to use. For example, numeric literals are rejected:
def seven : Pos := 7
failed to synthesize instance
OfNat Pos 7
Instead, the constructors must be used directly:
def seven : Pos :=
Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))
Similarly, addition and multiplication are not easy to use:
def fourteen : Pos := seven + seven
failed to synthesize instance
HAdd Pos Pos ?m.299
def fortyNine : Pos := seven * seven
failed to synthesize instance
HMul Pos Pos ?m.299
Each of these error messages begins with failed to synthesize instance
.
This indicates that the error is due to an overloaded operation that has not been implemented, and it describes the type class that must be implemented.
Classes and Instances
A type class consists of a name, some parameters, and a collection of methods. The parameters describe the types for which overloadable operations are being defined, and the methods are the names and type signatures of the overloadable operations. Once again, there is a terminology clash with objectoriented languages. In objectoriented programming, a method is essentially a function that is connected to a particular object in memory, with special access to the object's private state. Objects are interacted with via their methods. In Lean, the term "method" refers to an operation that has been declared to be overloadable, with no special connection to objects or values or private fields.
One way to overload addition is to define a type class named Plus
, with an addition method named plus
.
Once an instance of Plus
for Nat
has been defined, it becomes possible to add two Nat
s using Plus.plus
:
#eval Plus.plus 5 3
8
Adding more instances allows Plus.plus
to take more types of arguments.
In the following type class declaration, Plus
is the name of the class, α : Type
is the only argument, and plus : α → α → α
is the only method:
class Plus (α : Type) where
plus : α → α → α
This declaration says that there is a type class Plus
that overloads operations with respect to a type α
.
In particular, there is one overloaded operation called plus
that takes two α
s and returns an α
.
Type classes are first class, just as types are first class.
In particular, a type class is another kind of type.
The type of Plus
is Type → Type
, because it takes a type as an argument (α
) and results in a new type that describes the overloading of Plus
's operation for α
.
To overload plus
for a particular type, write an instance:
instance : Plus Nat where
plus := Nat.add
The colon after instance
indicates that Plus Nat
is indeed a type.
Each method of class Plus
should be assigned a value using :=
.
In this case, there is only one method: plus
.
By default, type class methods are defined in a namespace with the same name as the type class.
It can be convenient to open
the namespace so that users don't need to type the name of the class first.
Parentheses in an open
command indicate that only the indicated names from the namespace are to be made accessible:
open Plus (plus)
#eval plus 5 3
8
Defining an addition function for Pos
and an instance of Plus Pos
allows plus
to be used to add both Pos
and Nat
values:
def Pos.plus : Pos → Pos → Pos
 Pos.one, k => Pos.succ k
 Pos.succ n, k => Pos.succ (n.plus k)
instance : Plus Pos where
plus := Pos.plus
def fourteen : Pos := plus seven seven
Because there is not yet an instance of Plus Float
, attempting to add two floatingpoint numbers with plus
fails with a familiar message:
#eval plus 5.2 917.25861
failed to synthesize instance
Plus Float
These errors mean that Lean was unable to find an instance for a given type class.
Overloaded Addition
Lean's builtin addition operator is syntactic sugar for a type class called HAdd
, which flexibly allows the arguments to addition to have different types.
HAdd
is short for heterogeneous addition.
For example, an HAdd
instance can be written to allow a Nat
to be added to a Float
, resulting in a new Float
.
When a programmer writes x + y
, it is interpreted as meaning HAdd.hAdd x y
.
While an understanding of the full generality of HAdd
relies on features that are discussed in another section in this chapter, there is a simpler type class called Add
that does not allow the types of the arguments to be mixed.
The Lean libraries are set up so that an instance of Add
will be found when searching for an instance of HAdd
in which both arguments have the same type.
Defining an instance of Add Pos
allows Pos
values to use ordinary addition syntax:
instance : Add Pos where
add := Pos.plus
def fourteen : Pos := seven + seven
Conversion to Strings
Another useful builtin class is called ToString
.
Instances of ToString
provide a standard way of converting values from a given type into strings.
For example, a ToString
instance is used when a value occurs in an interpolated string, and it determines how the IO.println
function used at the beginning of the description of IO
will display a value.
For example, one way to convert a Pos
into a String
is to reveal its inner structure.
The function posToString
takes a Bool
that determines whether to parenthesize uses of Pos.succ
, which should be true
in the initial call to the function and false
in all recursive calls.
def posToString (atTop : Bool) (p : Pos) : String :=
let paren s := if atTop then s else "(" ++ s ++ ")"
match p with
 Pos.one => "Pos.one"
 Pos.succ n => paren s!"Pos.succ {posToString false n}"
Using this function for a ToString
instance:
instance : ToString Pos where
toString := posToString true
results in informative, yet overwhelming, output:
#eval s!"There are {seven}"
"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"
On the other hand, every positive number has a corresponding Nat
.
Converting it to a Nat
and then using the ToString Nat
instance (that is, the overloading of toString
for Nat
) is a quick way to generate much shorter output:
def Pos.toNat : Pos → Nat
 Pos.one => 1
 Pos.succ n => n.toNat + 1
instance : ToString Pos where
toString x := toString (x.toNat)
#eval s!"There are {seven}"
"There are 7"
When more than one instance is defined, the most recent takes precedence.
Additionally, if a type has a ToString
instance, then it can be used to display the result of #eval
even if the type in question was not defined with deriving Repr
, so #eval seven
outputs 7
.
Overloaded Multiplication
For multiplication, there is a type class called HMul
that allows mixed argument types, just like HAdd
.
Just as x + y
is interpreted as HAdd.hAdd x y
, x * y
is interpreted as HMul.hMul x y
.
For the common case of multiplication of two arguments with the same type, a Mul
instance suffices.
An instance of Mul
allows ordinary multiplication syntax to be used with Pos
:
def Pos.mul : Pos → Pos → Pos
 Pos.one, k => k
 Pos.succ n, k => n.mul k + k
instance : Mul Pos where
mul := Pos.mul
With this instance, multiplication works as expected:
#eval [seven * Pos.one,
seven * seven,
Pos.succ Pos.one * seven]
[7, 49, 14]
Literal Numbers
It is quite inconvenient to write out a sequence of constructors for positive numbers.
One way to work around the problem would be to provide a function to convert a Nat
into a Pos
.
However, this approach has downsides.
First off, because Pos
cannot represent 0
, the resulting function would either convert a Nat
to a bigger number, or it would return Option Nat
.
Neither is particularly convenient for users.
Secondly, the need to call the function explicitly would make programs that use positive numbers much less convenient to write than programs that use Nat
.
Having a tradeoff between precise types and convenient APIs means that the precise types become less useful.
In Lean, natural number literals are interpreted using a type class called OfNat
:
class OfNat (α : Type) (_ : Nat) where
ofNat : α
This type class takes two arguments: α
is the type for which a natural number is overloaded, and the unnamed Nat
argument is the actual literal number that was encountered in the program.
The method ofNat
is then used as the value of the numeric literal.
Because the class contains the Nat
argument, it becomes possible to define only instances for those values where the number makes sense.
OfNat
demonstrates that the arguments to type classes do not need to be types.
Because types in Lean are firstclass participants in the language that can be passed as arguments to functions and given definitions with def
and abbrev
, there is no barrier that prevents nontype arguments in positions where a lessflexible language could not permit them.
This flexibility allows overloaded operations to be provided for particular values as well as particular types.
For example, a sum type that represents natural numbers less than four can be defined as follows:
inductive LT4 where
 zero
 one
 two
 three
deriving Repr
While it would not make sense to allow any literal number to be used for this type, numbers less than four clearly make sense:
instance : OfNat LT4 0 where
ofNat := LT4.zero
instance : OfNat LT4 1 where
ofNat := LT4.one
instance : OfNat LT4 2 where
ofNat := LT4.two
instance : OfNat LT4 3 where
ofNat := LT4.three
With these instances, the following examples work:
#eval (3 : LT4)
LT4.three
#eval (0 : LT4)
LT4.zero
On the other hand, outofbounds literals are still not allowed:
#eval (4 : LT4)
failed to synthesize instance
OfNat LT4 4
For Pos
, the OfNat
instance should work for any Nat
other than Nat.zero
.
Another way to phrase this is to say that for all natural numbers n
, the instance should work for n + 1
.
Just as names like α
automatically become implicit arguments to functions that Lean fills out on its own, instances can take automatic implicit arguments.
In this instance, the argument n
stands for any Nat
, and the instance is defined for a Nat
that's one greater:
instance : OfNat Pos (n + 1) where
ofNat :=
let rec natPlusOne : Nat → Pos
 0 => Pos.one
 k + 1 => Pos.succ (natPlusOne k)
natPlusOne n
Because n
stands for a Nat
that's one less than what the user wrote, the helper function natPlusOne
returns a Pos
that's one greater than its argument.
This makes it possible to use natural number literals for positive numbers, but not for zero:
def eight : Pos := 8
def zero : Pos := 0
failed to synthesize instance
OfNat Pos 0
Exercises
Another Representation
An alternative way to represent a positive number is as the successor of some Nat
.
Replace the definition of Pos
with a structure whose constructor is named succ
that contains a Nat
:
structure Pos where
succ ::
pred : Nat
Define instances of Add
, Mul
, ToString
, and OfNat
that allow this version of Pos
to be used conveniently.
Even Numbers
Define a datatype that represents only even numbers. Define instances of Add
, Mul
, and ToString
that allow it to be used conveniently. OfNat
requires a feature that is introduced in the next section.
HTTP Requests
An HTTP request begins with an identification of a HTTP method, such as GET
or POST
, along with a URI and an HTTP version.
Define an inductive type that represents an interesting subset of the HTTP methods, and a structure that represents HTTP responses.
Responses should have a ToString
instance that makes it possible to debug them.
Use a type class to associate different IO
actions with each HTTP method, and write a test harness as an IO
action that calls each method and prints the result.
Type Classes and Polymorphism
It can be useful to write functions that work for any overloading of a given function.
For instance, IO.println
works for any type that has an instance of ToString
.
This is indicated using square brackets around the required instance: the type of IO.println
is {α : Type} → [ToString α] → α → IO Unit
.
This type says that IO.println
accepts an argument of type α
, which Lean should determine automatically, and that there must be a ToString
instance available for α
.
It returns an IO
action.
Checking Polymorphic Functions' Types
Checking the type of a function that takes implicit arguments or uses type classes requires the use of some additional syntax. Simply writing
#check IO.println
yields a type with metavariables:
IO.println : ?m.3611 → IO Unit
This is because Lean does its best to discover implicit arguments, and the presence of metavariables indicates that it did not yet discover enough type information to do so.
To understand the signature of a function, this feature can be suppressed with an atsign (@
) before the function's name:
#check @IO.println
@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit
In this output, the instance itself has been given the name inst
.
Additionally, there is a u_1
after Type
, which uses a feature of Lean that has not yet been introduced.
For now, ignore these parameters to Type
.
Defining Polymorphic Functions with Instance Implicits
A function that sums all entries in a list needs two instances: Add
allows the entries to be added, and an OfNat
instance for 0
provides a sensible value to return for the empty list:
def List.sum [Add α] [OfNat α 0] : List α → α
 [] => 0
 x :: xs => x + xs.sum
This function can be used for a list of Nat
s:
def fourNats : List Nat := [1, 2, 3, 4]
#eval fourNats.sum
10
but not for a list of Pos
numbers:
def fourPos : List Pos := [1, 2, 3, 4]
#eval fourPos.sum
failed to synthesize instance
OfNat Pos 0
Specifications of required instances in square brackets are called instance implicits. Behind the scenes, every type class defines a structure that has a field for each overloaded operation. Instances are values of that structure type, with each field containing an implementation. At a call site, Lean is responsible for finding an instance value to pass for each instance implicit argument. The most important difference between ordinary implicit arguments and instance implicits is the strategy that Lean uses to find an argument value. In the case of ordinary implicit arguments, Lean uses a technique called unification to find a single unique argument value that would allow the program to pass the type checker. This process relies only on the specific types involved in the function's definition and the call site. For instance implicits, Lean instead consults a builtin table of instance values.
Just as the OfNat
instance for Pos
took a natural number n
as an automatic implicit argument, instances may also take instance implicit arguments themselves.
The section on polymorphism presented a polymorphic point type:
structure PPoint (α : Type) where
x : α
y : α
deriving Repr
Addition of points should add the underlying x
and y
fields.
Thus, an Add
instance for PPoint
requires an Add
instance for whatever type these fields have.
In other words, the Add
instance for PPoint
requires a further Add
instance for α
:
instance [Add α] : Add (PPoint α) where
add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }
When Lean encounters an addition of two points, it searches for and finds this instance.
It then performs a further search for the Add α
instance.
The instance values that are constructed in this way are values of the type class's structure type.
A successful recursive instance search results in a structure value that has a reference to another structure value.
An instance of Add (PPoint Nat)
contains a reference to the instance of Add Nat
that was found.
This recursive search process means that type classes offer significantly more power than plain overloaded functions. A library of polymorphic instances is a set of code building blocks that the compiler will assemble on its own, given nothing but the desired type. Polymorphic functions that take instance arguments are latent requests to the type class mechanism to assemble helper functions behind the scenes. The API's clients are freed from the burden of plumbing together all of the necessary parts by hand.
Methods and Implicit Arguments
The type of @OfNat.ofNat
may be surprising.
It is {α : Type} → (n : Nat) → [OfNat α n] → α
, in which the Nat
argument n
occurs as an explicit function argument.
In the declaration of the method, however, ofNat
simply has type α
.
This seeming discrepancy is because declaring a type class really results in the following:
 A structure type to contain the implementation of each overloaded operation
 A namespace with the same name as the class
 For each method, a function in the class's namespace that retrieves its implementation from an instance
This is analogous to the way that declaring a new structure also declares accessor functions. The primary difference is that a structure's accessors take the structure value as an explicit argument, while the type class methods take the instance value as an instance implicit to be found automatically by Lean.
In order for Lean to find an instance, its arguments must be available.
This means that each argument to the type class must be an argument to the method that occurs before the instance.
It is most convenient when these arguments are implicit, because Lean does the work of discovering their values.
For example, @Add.add
has the type {α : Type} → [Add α] → α → α → α
.
In this case, the type argument α
can be implicit because the arguments to Add.add
provide information about which type the user intended.
This type can then be used to search for the Add
instance.
In the case of ofNat
, however, the particular Nat
literal to be decoded does not appear as part of any other argument.
This means that Lean would have no information to use when attempting to figure out the implicit argument n
.
The result would be a very inconvenient API.
Thus, in these cases, Lean uses an explicit argument for the class's method.
Exercises
Even Number Literals
Write an instance of OfNat
for the even number datatype from the previous section's exercises that uses recursive instance search.
Controlling Instance Search
An instance of the Add
class is sufficient to allow two expressions with type Pos
to be conveniently added, producing another Pos
.
However, in many cases, it can be useful to be more flexible and allow heterogeneous operator overloading, where the arguments may have different types.
For example, adding a Nat
to a Pos
or a Pos
to a Nat
will always yield a Pos
:
def addNatPos : Nat → Pos → Pos
 0, p => p
 n + 1, p => Pos.succ (addNatPos n p)
def addPosNat : Pos → Nat → Pos
 p, 0 => p
 p, n + 1 => Pos.succ (addPosNat p n)
These functions allow natural numbers to be added to positive numbers, but they cannot be used with the Add
type class, which expects both arguments to add
to have the same type.
Heterogeneous Overloadings
As mentioned in the section on overloaded addition, Lean provides a type class called HAdd
for overloading addition heterogeneously.
The HAdd
class takes three type parameters: the two argument types and the return type.
Instances of HAdd Nat Pos Pos
and HAdd Pos Nat Pos
allow ordinary addition notation to be used to mix the types:
instance : HAdd Nat Pos Pos where
hAdd := addNatPos
instance : HAdd Pos Nat Pos where
hAdd := addPosNat
Given the above two instances, the following examples work:
#eval (3 : Pos) + (5 : Nat)
8
#eval (3 : Nat) + (5 : Pos)
8
The definition of the HAdd
type class is very much like the following definition of HPlus
with the corresponding instances:
class HPlus (α : Type) (β : Type) (γ : Type) where
hPlus : α → β → γ
instance : HPlus Nat Pos Pos where
hPlus := addNatPos
instance : HPlus Pos Nat Pos where
hPlus := addPosNat
However, instances of HPlus
are significantly less useful than instances of HAdd
.
When attempting to use these instances with #eval
, an error occurs:
#eval HPlus.hPlus (3 : Pos) (5 : Nat)
typeclass instance problem is stuck, it is often due to metavariables
HPlus Pos Nat ?m.7154
This happens because there is a metavariable in the type, and Lean has no way to solve it.
As discussed in the initial description of polymorphism, metavariables represent unknown parts of a program that could not be inferred.
When an expression is written following #eval
, Lean attempts to determine its type automatically.
In this case, it could not.
Because the third type parameter for HPlus
was unknown, Lean couldn't carry out type class instance search, but instance search is the only way that Lean could determine the expression's type.
That is, the HPlus Pos Nat Pos
instance can only apply if the expression should have type Pos
, but there's nothing in the program other than the instance itself to indicate that it should have this type.
One solution to the problem is to ensure that all three types are available by adding a type annotation to the whole expression:
#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)
8
However, this solution is not very convenient for users of the positive number library.
Output Parameters
This problem can also be solved by declaring γ
to be an output parameter.
Most type class parameters are inputs to the search algorithm: they are used to select an instance.
For example, in an OfNat
instance, both the type and the natural number are used to select a particular interpretation of a natural number literal.
However, in some cases, it can be convenient to start the search process even when some of the type parameters are not yet known, and use the instances that are discovered in the search to determine values for metavariables.
The parameters that aren't needed to start instance search are outputs of the process, which is declared with the outParam
modifier:
class HPlus (α : Type) (β : Type) (γ : outParam Type) where
hPlus : α → β → γ
With this output parameter, type class instance search is able to select an instance without knowing γ
in advance.
For instance:
#eval HPlus.hPlus (3 : Pos) (5 : Nat)
8
It might be helpful to think of output parameters as defining a kind of function. Any given instance of a type class that has one or more output parameters provides Lean with instructions for determining the outputs from the inputs. The process of searching for an instance, possibly recursively, ends up being more powerful than mere overloading. Output parameters can determine other types in the program, and instance search can assemble a collection of underlying instances into a program that has this type.
Default Instances
Deciding whether a parameter is an input or an output controls the circumstances under which Lean will initiate type class search. In particular, type class search does not occur until all inputs are known. However, in some cases, output parameters are not enough, and instance search should also occur when some inputs are unknown. This is a bit like default values for optional function arguments in Python or Kotlin, except default types are being selected.
Default instances are instances that are available for instance search even when not all their inputs are known. When one of these instances can be used, it will be used. This can cause programs to successfully type check, rather than failing with errors related to unknown types and metavariables. On the other hand, default instances can make instance selection less predictable. In particular, if an undesired default instance is selected, then an expression may have a different type than expected, which can cause confusing type errors to occur elsewhere in the program. Be selective about where default instances are used!
One example of where default instances can be useful is an instance of HPlus
that can be derived from an Add
instance.
In other words, ordinary addition is a special case of heterogeneous addition in which all three types happen to be the same.
This can be implemented using the following instance:
instance [Add α] : HPlus α α α where
hPlus := Add.add
With this instance, hPlus
can be used for any addable type, like Nat
:
#eval HPlus.hPlus (3 : Pos) (5 : Nat)
8
However, this instance will only be used in situations where the types of both arguments are known. For example,
#check HPlus.hPlus (5 : Nat) (3 : Nat)
yields the type
HPlus.hPlus 5 3 : Nat
as expected, but
#check HPlus.hPlus (5 : Nat)
yields a type that contains two metavariables, one for the remaining argument and one for the return type:
HPlus.hPlus 5 : ?m.7319 → ?m.7321
In the vast majority of cases, when someone supplies one argument to addition, the other argument will have the same type.
To make this instance into a default instance, apply the default_instance
attribute:
@[default_instance]
instance [Add α] : HPlus α α α where
hPlus := Add.add
With this default instance, the example has a more useful type:
#check HPlus.hPlus (5 : Nat)
yields
HPlus.hPlus 5 : Nat → Nat
Each operator that exists in overloadable heterogeneous and homogeneous versions follows the pattern of a default instance that allows the homogeneous version to be used in contexts where the heterogeneous is expected. The infix operator is replaced with a call to the heterogeneous version, and the homogeneous default instance is selected when possible.
Similarly, simply writing 5
gives a Nat
rather than a type with a metavariable that is waiting for more information in order to select an OfNat
instance.
This is because the OfNat
instance for Nat
is a default instance.
Default instances can also be assigned priorities that affect which will be chosen in situations where more than one might apply. For more information on default instance priorities, please consult the Lean manual.
Exercises
Define an instance of HMul (PPoint α) α (PPoint α)
that multiplies both projections by the scalar.
It should work for any type α
for which there is a Mul α
instance.
For example,
#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0
should yield
{ x := 5.000000, y := 7.400000 }
Arrays and Indexing
The Interlude describes how to use indexing notation in order to look up entries in a list by their position. This syntax is also governed by a type class, and it can be used for a variety of different types.
Arrays
For instance, Lean arrays are much more efficient than linked lists for most purposes.
In Lean, the type Array α
is a dynamicallysized array holding values of type α
, much like a Java ArrayList
, a C++ std::vector
, or a Rust Vec
.
Unlike List
, which has a pointer indirection on each use of the cons
constructor, arrays occupy a contiguous region of memory, which is much better for processor caches.
Also, looking up a value in an array takes constant time, while lookup in a linked list takes time proportional to the index being accessed.
In pure functional languages like Lean, it is not possible to mutate a given position in a data structure. Instead, a copy is made that has the desired modifications. When using an array, the Lean compiler and runtime contain an optimizations that can allow modifications to be implemented as mutations behind the scenes when there is only a single unique reference to an array, while a list would require copies of all prior nodes to be made.
Arrays are written similarly to lists, but with a leading #
:
def northernTrees : Array String :=
#["beech", "birch", "elm", "oak"]
The number of values in an array can be found using Array.size
.
For instance, northernTrees.size
evaluates to 4
.
For indices that are smaller than an array's size, indexing notation can be used to find the corresponding value, just as with lists.
That is, northernTrees[2]
evaluates to "elm"
.
Similarly, the compiler requires a proof that an index is in bounds, and attempting to look up a value outside the bounds of the array results in a compiletime error, just as with lists.
For instance, northernTrees[8]
results in:
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 perfomed, 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
⊢ 8 < Array.size northernTrees
NonEmpty Lists
A datatype that represents nonempty lists can be defined as a structure with a field for the head of the list and a field for the tail, which is an ordinary, potentially empty list:
structure NonEmptyList (α : Type) : Type where
head : α
tail : List α
For example, the nonempty list idahoSpiders
(which contains some spider species native to the US state of Idaho) consists of "Banded Garden Spider"
followed by four other spiders, for a total of five spiders.
Looking up the value at a specific index in this list with a recursive function should consider three possibilities:
 The index is
0
, in which case the head of the list should be returned.  The index is
n + 1
and the tail is empty, in which case the index is out of bounds.  The index is
n + 1
and the tail is nonempty, in which case the function can be called recursively on the tail andn
.
For example, a lookup function that returns an Option
can be written as follows:
def NonEmptyList.get? : NonEmptyList α → Nat → Option α
 xs, 0 => some xs.head
 {head := _, tail := []}, _ + 1 => none
 {head := _, tail := h :: t}, n + 1 => get? {head := h, tail := t} n
Each case in the pattern match corresponds to one of the possibilities above.
The recursive call to get?
does not require a NonEmptyList
namespace qualifier because the body of the definition is implicitly in the definition's namespace.
Another way to write this function uses get?
for lists when the index is greater than zero:
def NonEmptyList.get? : NonEmptyList α → Nat → Option α
 xs, 0 => some xs.head
 xs, n + 1 => xs.tail.get? n
If the list contains one entry, then only 0
is a valid index.
If it contains two entries, then both 0
and 1
are valid indices.
If it contains three entries, then 0
, 1
, and 2
are valid indices.
In other words, the valid indices into a nonempty list are natural numbers that are strictly less than the length of the list, which are less than or equal to the length of the tail.
The definition of what it means for an index to be in bounds should be written as an abbrev
because the tactics used to find evidence that indices are acceptable are able to solve inequalities of numbers, but they don't know anything about the name NonEmptyList.inBounds
:
abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop :=
i ≤ xs.tail.length
This function returns a proposition that might be true or false.
For instance, 2
is in bounds for idahoSpiders
, while 5
is not:
theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp
theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp
The logical negation operator has a very low precedence, which means that ¬idahoSpiders.inBounds 5
is equivalent to ¬(idahoSpiders.inBounds 5)
.
This fact can be used to write a lookup function that requires evidence that the index is valid, and thus need not return Option
, by delegating to the version for lists that checks the evidence at compile time:
def NonEmptyList.get (xs : NonEmptyList α) (i : Nat) (ok : xs.inBounds i) : α :=
match i with
 0 => xs.head
 n + 1 => xs.tail[n]
It is, of course, possible to write this function to use the evidence directly, rather than delegating to a standard library function that happens to be able to use the same evidence. This requires techniques for working with proofs and propositions that are described later in this book.
Overloading Indexing
Indexing notation for a collection type can be overloaded by defining an instance of the GetElem
type class.
For the sake of flexiblity, GetElem
has four parameters:
 The type of the collection
 The type of the index
 The type of elements that are extracted from the collection
 A function that determines what counts as evidence that the index is in bounds
The element type and the evidence function are both output parameters.
GetElem
has a single method, getElem
, which takes a collection value, an index value, and evidence that the index is in bounds as arguments, and returns an element:
class GetElem (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where
getElem : (c : coll) → (i : idx) → inBounds c i → item
In the case of NonEmptyList α
, these parameters are:
 The collection is
NonEmptyList α
 Indices have type
Nat
 The type of elements is
α
 An index is in bounds if it is less than or equal to the length of the tail
In fact, the GetElem
instance can delegate directly to NonEmptyList.get
:
instance : GetElem (NonEmptyList α) Nat α NonEmptyList.inBounds where
getElem := NonEmptyList.get
With this instance, NonEmptyList
becomes just as convenient to use as List
.
Evaluating idahoSpiders[0]
yields "Banded Garden Spider"
, while idahoSpiders[9]
leads to the compiletime error:
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 perfomed, 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
⊢ NonEmptyList.inBounds idahoSpiders 9
Because both the collection type and the index type are input parameters to the GetElem
type class, new types can be used to index into existing collections.
The positive number type Pos
is a perfectly reasonable index into a List
, with the caveat that it cannot point at the first entry.
The follow instance of GetElem
allows Pos
to be used just as conveniently as Nat
to find a list entry:
instance : GetElem (List α) Pos α (fun list n => list.length > n.toNat) where
getElem (xs : List α) (i : Pos) ok := xs[i.toNat]
Indexing can also make sense for nonnumeric indices.
For example, Bool
can be used to select between the fields in a point, with false
corresponding to x
and true
corresponding to y
:
instance : GetElem (PPoint α) Bool α (fun _ _ => True) where
getElem (p : PPoint α) (i : Bool) _ :=
if not i then p.x else p.y
In this case, both Booleans are valid indices.
Because every possible Bool
is in bounds, the evidence is simply the true proposition True
.
Standard Classes
This section presents a variety of operators and functions that can be overloaded using type classes in Lean.
Each operator or function corresponds to a method of a type class.
Unlike C++, infix operators in Lean are defined as abbreviations for named functions; this means that overloading them for new types is not done using the operator itself, but rather refers to a name such as HAdd.hAdd
.
Arithmetic
Most arithmetic operators are available in a heterogeneous form, where the arguments may have different type and an output parameter decides the type of the resulting expression.
For each heterogeneous operator, there is a corresponding homogeneous version that can found by removing the letter h
, so that HAdd.hAdd
becomes Add.add
.
The following arithmetic operators are overloaded:
Expression  Desugaring  Class Name 

x + y  HAdd.hAdd x y  HAdd 
x  y  HSub.hSub x y  HSub 
x * y  HMul.hMul x y  HMul 
x / y  HDiv.hDiv x y  HDiv 
x % y  HMod.hMod x y  HMod 
x ^ y  HPow.hPow x y  HPow 
( x)  Neg.neg x  Neg 
Bitwise Operators
Lean contains a number of standard bitwise operators that are overloaded using type classes.
There are instances for fixedwidth types such as UInt8
, UInt16
, UInt32
, UInt64
, and USize
.
The latter is the size of words on the current platform, typically 32 or 64 bits.
The following bitwise operators are overloaded:
Expression  Desugaring  Class Name 

x &&& y  HAnd.hAnd x y  HAnd 
x  y  HOr.hOr x y  HOr 
x ^^^ y  HXor.hXor x y  HXor 
~~~ x  Complement.complement x  Complement 
x >>> y  HShiftRight.hShiftRight x y  HShiftRight 
x <<< y  HShiftLeft.hShiftLeft x y  HShiftLeft 
Because the names And
and Or
are already taken as the names of logical connectives, the homogeneous versions of HAnd
and HOr
are called AndOp
and OrOp
rather than And
and Or
.
Equality and Ordering
Testing equality of two values typically uses the BEq
class, which is short for "Boolean equality".
Due to Lean's use as a theorem prover, there are really two kinds of equality operators in Lean:
 Boolean equality is the same kind of equality that is found in other programming languages. It is a function that takes two values and returns a
Bool
. Boolean equality is written with two equals signs, just as in Python and C#. Because Lean is a pure functional language, there's no separate notions of reference vs value equality—pointers cannot be observed directly.  Propositional equality is the mathematical statement that two things are equal. Propositional equality is not a function; rather, it is a mathematical statement that admits proof. It is written with a single equals sign. A statement of propositional equality is like a type that classifies evidence of this equality.
Both notions of equality are important, and used for different purposes.
Boolean equality is useful in programs, when a decision needs to be made about whether two values are equal.
For example, "Octopus" == "Cuttlefish"
evaluates to false
, and "Octopodes" == "Octo".append "podes"
evaluates to true
.
Some values, such as functions, cannot be checked for equality.
For example, (fun (x : Nat) => 1 + x) == (Nat.succ ·)
yields the error:
failed to synthesize instance
BEq (Nat → Nat)
As this message indicates, ==
is overloaded using a type class.
The expression x == y
is actually shorthand for BEq.beq x y
.
Propositional equality is a mathematical statement rather than an invocation of a program.
Because propositions are like types that describe evidence for some statement, propositional equality has more in common with types like String
and Nat → List Int
than it does with Boolean equality.
This means that it can't automatically be checked.
However, the equality of any two expressions can be stated in Lean, so long as they have the same type.
The statement (fun (x : Nat) => 1 + x) = (Nat.succ ·)
is a perfectly reasonable statement.
From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a twoline proof to convince Lean of this fact.
Generally speaking, when using Lean as a programming language, it's easiest to stick to Boolean functions rather than propositions.
However, as the names true
and false
for Bool
's constructors suggest, this difference is sometimes blurred.
Some propositions are decidable, which means that they can be checked just like a Boolean function.
The function that checks whether the proposition is true or false is called a decision procedure, and it returns evidence of the truth or falsity of the proposition.
Some examples of decidable propositions include equality and inequality of natural numbers, equality of strings, and "ands" and "ors" of propositions that are themselves decidable.
In Lean, if
works with decidable propositions.
For example, 2 < 4
is a proposition:
#check 2 < 4
2 < 4 : Prop
Nonetheless, it is perfectly acceptable to write it as the condition in an if
.
For example, if 2 < 4 then 1 else 2
has type Nat
and evaluates to 1
.
Not all propositions are decidable.
If they were, then computers would be able to prove any true proposition just by running the decision procedure, and mathematicians would be out of a job.
More specifically, decidable propositions have an instance of the Decidable
type class which has a method that is the decision procedure.
Trying to use a proposition that isn't decidable as if it were a Bool
results in a failure to find the Decidable
instance.
For example, if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no"
results in:
failed to synthesize instance
Decidable ((fun x => 1 + x) = fun x => Nat.succ x)
The following propositions, that are usually decidable, are overloaded with type classes:
Expression  Desugaring  Class Name 

x < y  LT.lt x y  LT 
x ≤ y  LE.le x y  LE 
x > y  LT.lt y x  LT 
x ≥ y  LE.le y x  LE 
Because defining new propositions hasn't yet been demonstrated, it may be difficult to define new instances of LT
and LE
.
Additionally, comparing values using <
, ==
, and >
can be inefficient.
Checking first whether one value is less than another, and then whether they are equal, can require two traversals over large data structures.
To solve this problem, Java and C# have standard compareTo
and CompareTo
methods (respectively) that can be overridden by a class in order to implement all three operations at the same time.
These methods return a negative integer if the receiver is less than the argument, zero if they are equal, and a positive integer if the receiver is greater than the argument.
Rather than overload the meaning of integers, Lean has a builtin inductive type that describes these three possibilities:
inductive Ordering where
 lt
 eq
 gt
The Ord
type class can be overloaded to produce these comparisons.
For Pos
, an implementation can be:
def Pos.comp : Pos → Pos → Ordering
 Pos.one, Pos.one => Ordering.eq
 Pos.one, Pos.succ _ => Ordering.lt
 Pos.succ _, Pos.one => Ordering.gt
 Pos.succ n, Pos.succ k => comp n k
instance : Ord Pos where
compare := Pos.comp
In situations where compareTo
would be the right approach in Java, use Ord.compare
in Lean.
Hashing
Java and C# have hashCode
and GetHashCode
methods, respectively, that compute a hash of a value for use in data structures such as hash tables.
The Lean equivalent is a type class called Hashable
:
class Hashable (α : Type) where
hash : α → UInt64
If two values are considered equal according to a BEq
instance for their type, then they should have the same hashes.
In other words, if x == y
then hash x == hash y
.
If x ≠ y
, then hash x
won't necessarily differ from hash y
(after all, there are infinitely more Nat
values than there are UInt64
values), but data structures built on hashing will have better performance if unequal values are likely to have unequal hashes.
This is the same expectation as in Java and C#.
The standard library contains a function mixHash
with type UInt64 → UInt64 → UInt64
that can be used to combine hashes for different fields for a constructor.
A reasonable hash function for an inductive datatype can be written by assigning a unique number to each constructor, and then mixing that number with the hashes of each field.
For example, a Hashable
instance for Pos
can be written:
def hashPos : Pos → UInt64
 Pos.one => 0
 Pos.succ n => mixHash 1 (hashPos n)
instance : Hashable Pos where
hash := hashPos
Hashable
instances for polymorphic types can use recursive instance search.
Hashing a NonEmptyList α
is only possible when α
can be hashed:
instance [Hashable α] : Hashable (NonEmptyList α) where
hash xs := mixHash (hash xs.head) (hash xs.tail)
Binary trees use both recursion and recursive instance search in the implementations of BEq
and Hashable
:
inductive BinTree (α : Type) where
 leaf : BinTree α
 branch : BinTree α → α → BinTree α → BinTree α
def eqBinTree [BEq α] : BinTree α → BinTree α → Bool
 BinTree.leaf, BinTree.leaf =>
true
 BinTree.branch l x r, BinTree.branch l2 x2 r2 =>
x == x2 && eqBinTree l l2 && eqBinTree r r2
 _, _ =>
false
instance [BEq α] : BEq (BinTree α) where
beq := eqBinTree
def hashBinTree [Hashable α] : BinTree α → UInt64
 BinTree.leaf =>
0
 BinTree.branch left x right =>
mixHash 1 (mixHash (hashBinTree left) (mixHash (hash x) (hashBinTree right)))
instance [Hashable α] : Hashable (BinTree α) where
hash := hashBinTree
Deriving Standard Classes
Instance of classes like BEq
and Hashable
are often quite tedious to implement by hand.
Lean includes a feature called instance deriving that allows the compiler to automatically construct wellbehaved instances of many type classes.
In fact, the deriving Repr
phrase in the definition of Point
in the section on structures is an example of instance deriving.
Instances can be derived in two ways.
The first can be used when defining a structure or inductive type.
In this case, add deriving
to the end of the type declaration followed by the names of the classes for which instances should be derived.
For a type that is already defined, a standalone deriving
command can be used.
Write deriving instance C1, C2, ... for T
to deriving instances of C1, C2, ...
for the type T
after the fact.
BEq
and Hashable
instances can be derived for Pos
and NonEmptyList
using a very small amount of code:
deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable, Repr for NonEmptyList
Instance can be derived for at least the following classes:
Inhabited
BEq
Repr
Hashable
Ord
In some cases, however, the derived Ord
instance may not produce precisely the ordering desired in an application.
When this is the case, it's fine to write an Ord
instance by hand.
The collection of classes for which instances can be derived can be extended by advanced users of Lean.
Aside from the clear advantages in programmer productivity and code readability, deriving instances also makes code easier to maintain, because the instances are updated as the definitions of types evolve. Changesets involving updates to datatypes are easier to read without line after line of formulaic modifications to equality tests and hash computation.
Appending
Many datatypes have some sort of append operator.
In Lean, appending two values is overloaded with the type class HAppend
, which is a heterogeneous operation like that used for arithmetic operations:
class HAppend (α : Type) (β : Type) (γ : outParam Type) where
hAppend : α → β → γ
The syntax xs ++ ys
desugars to HAppend.hAppend xs ys
.
For homogeneous cases, it's enough to implement an instance of Append
, which follows the usual pattern:
instance : Append (NonEmptyList α) where
append xs ys :=
{ head := xs.head, tail := xs.tail ++ ys.head :: ys.tail }
After defining the above instance,
#eval idahoSpiders ++ idahoSpiders
has the following output:
{ head := "Banded Garden Spider",
tail := ["Longlegged Sac Spider",
"Wolf Spider",
"Hobo Spider",
"Catfaced Spider",
"Banded Garden Spider",
"Longlegged Sac Spider",
"Wolf Spider",
"Hobo Spider",
"Catfaced Spider"] }
Similarly, a definition of HAppend
allows nonempty lists to be appended to ordinary lists:
instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
hAppend xs ys :=
{ head := xs.head, tail := xs.tail ++ ys }
With this instance available,
#eval idahoSpiders ++ ["Trapdoor Spider"]
results in
{ head := "Banded Garden Spider",
tail := ["Longlegged Sac Spider", "Wolf Spider", "Hobo Spider", "Catfaced Spider", "Trapdoor Spider"] }
Functors
A polymorphic type is a functor if it has an overload for a function named map
that transforms every element contained in it by a function.
While most languages use this terminology, C#'s equivalent to map
is called System.Linq.Enumerable.Select
.
For example, mapping a function over a list constructs a new list in which each entry from the starting list has been replaced by the result of the function on that entry.
Mapping a function f
over an Option
leaves none
untouched, and replaces some x
with some (f x)
.
Here are some examples of functors and how their Functor
instances overload map
:
Functor.map (· + 5) [1, 2, 3]
evaluates to[6, 7, 8]
Functor.map toString (some (List.cons 5 List.nil))
evaluates tosome "[5]"
Functor.map List.reverse [[1, 2, 3], [4, 5, 6]]
evaluates to[[3, 2, 1], [6, 5, 4]]
Because Functor.map
is a bit of a long name for this common operation, Lean also provides an infix operator for mapping a function, namely <$>
.
The prior examples can be rewritten as follows:
(· + 5) <$> [1, 2, 3]
evaluates to[6, 7, 8]
toString <$> (some (List.cons 5 List.nil))
evaluates tosome "[5]"
List.reverse <$> [[1, 2, 3], [4, 5, 6]]
evaluates to[[3, 2, 1], [6, 5, 4]]
An instance of Functor
for NonEmptyList
requires specifying the map
function.
instance : Functor NonEmptyList where
map f xs := { head := f xs.head, tail := f <$> xs.tail }
Here, map
uses the Functor
instance for List
to map the function over the tail.
This instance is defined for NonEmptyList
rather than for NonEmptyList α
because the argument type α
plays no role in resolving the type class.
A NonEmptyList
can have a function mapped over it no matter what the type of entries is.
If α
were a parameter to the class, then it would be possible to make versions of Functor
that only worked for NonEmptyList Nat
, but part of being a functor is that map
works for any entry type.
Here is an instance of Functor
for PPoint
:
instance : Functor PPoint where
map f p := { x := f p.x, y := f p.y }
In this case, f
has been applied to both x
and y
.
Even when the type contained in a functor is itself a functor, mapping a function only goes down one layer.
That is, when using map
on a NonEmptyList (PPoint Nat)
, the function being mapped should take PPoint Nat
as its argument rather than Nat
.
The definition of the Functor
class uses one more language feature that has not yet been discussed: default method definitions.
Normally, a class will specify some minimal set of overloadable operations that make sense together, and then use polymorphic functions with instance implicit arguments that build on the overloaded operations to provide a larger library of features.
For example, the function concat
can concatenate any nonempty list whose entries are appendable:
def concat [Append α] (xs : NonEmptyList α) : α :=
let rec catList (start : α) : List α → α
 [] => start
 (z :: zs) => catList (start ++ z) zs
catList xs.head xs.tail
However, for some classes, there are operations that can be more efficiently implemented with knowledge of the internals of a datatype.
In these cases, a default method definition can be provided.
A default method definition provides a default implementation of a method in terms of the other methods.
However, instance implementors may choose to override this default with something more efficient.
Default method definitions contain :=
in a class
definition.
In the case of Functor
, some types have a more efficient way of implementing map
when the function being mapped ignores its argument.
Functions that ignore their arguments are called constant functions because they always return the same value.
Here is the definition of Functor
, in which mapConst
has a default implementation:
class Functor (f : Type → Type) where
map : {α β : Type} → (α → β) → f α → f β
mapConst {α β : Type} (x : α) (coll : f β) : f α :=
map (fun _ => x) coll
Just as a Hashable
instance that doesn't respect BEq
is buggy, a Functor
instance that moves around the data as it maps the function is also buggy.
For example, a buggy Functor
instance for List
might throw away its argument and always return the empty list, or it might reverse the list.
A bad instance for PPoint
might place f x
in both the x
and the y
fields.
Specifically, Functor
instances should follow two rules:
 Mapping the identity function should result in the original argument.
 Mapping two composed functions should have the same effect as composing their mapping.
More formally, the first rule says that id <$> x
equals x
.
The second rule says that map (fun y => f (g y)) x
equals map f (map g x)
.
These rules prevent implementations of map
that move the data around or delete some of it.
Exercises
 Write an instance of
HAppend (List α) (NonEmptyList α) (NonEmptyList α)
and test it.  Implement a
Functor
instance for the binary tree datatype.
Coercions
In mathematics, it is common to use the same symbol to stand for different aspects of some object in different contexts.
For example, if a ring is referred to in a context where a set is expected, then it is understood that the ring's underlying set is what's intended.
In programming languages, it is common to have rules to automatically translate values of one type into values of another type.
For instance, Java allows a byte
to be automatically promoted to an int
, and Kotlin allows a nonnullable type to be used in a context that expects a nullable version of the type.
In Lean, both purposes are served by a mechanism called coercions. When Lean encounters an expression of one type in a context that expects a different type, it will attempt to coerce the expression before reporting a type error. Unlike Java, C, and Kotlin, the coercions are extensible by defining instances of type classes.
Positive Numbers
For example, every positive number corresponds to a natural number.
The function Pos.toNat
that was defined earlier converts a Pos
to the corresponding Nat
:
def Pos.toNat : Pos → Nat
 Pos.one => 1
 Pos.succ n => n.toNat + 1
The function List.drop
, with type {α : Type} → Nat → List α → List α
, removes a prefix of a list.
Applying List.drop
to a Pos
, however, leads to a type error:
[1, 2, 3, 4].drop (2 : Pos)
application type mismatch
List.drop 2
argument
2
has type
Pos : Type
but is expected to have type
Nat : Type
Because the author of List.drop
did not make it a method of a type class, it can't be overridden by defining a new instance.
The type class Coe
describes overloaded ways of coercing from one type to another:
class Coe (α : Type) (β : Type) where
coe : α → β
An instance of Coe Pos Nat
is enough to allow the prior code to work:
instance : Coe Pos Nat where
coe x := x.toNat
#eval [1, 2, 3, 4].drop (2 : Pos)
[3, 4]
Using #check
shows the result of the instance search that was used behind the scenes:
#check [1, 2, 3, 4].drop (2 : Pos)
List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat
Chaining Coercions
When searching for coercions, Lean will attempt to assemble a coercion out of a chain of smaller coercions.
For example, there is already a coercion from Nat
to Int
.
Because of that instance, combined with the Coe Pos Nat
instance, the following code is accepted:
def oneInt : Int := Pos.one
This definition uses two coercions: from Pos
to Nat
, and then from Nat
to Int
.
The Lean compiler does not get stuck in the presence of circular coercions.
For example, even if two types A
and B
can be coerced to one another, their mutual coercions can be used to find a path:
inductive A where
 a
inductive B where
 b
instance : Coe A B where
coe _ := B.b
instance : Coe B A where
coe _ := A.a
instance : Coe Unit A where
coe _ := A.a
def coercedToB : B := Unit.unit
Some coercions, however, should only be applied once.
The Option
type can be used similarly to nullable types in C# and Kotlin: the none
constructor represents the absence of a value.
The Lean standard library defines a coercion from any type α
to Option α
that wraps the value in in some
.
This allows option types to be used in manner even more similar to nullable types, because some
can be omitted.
For instance, the function List.getLast?
that finds the last entry in a list can be written without a some
around the return value x
:
def List.last? : List α → Option α
 [] => none
 [x] => x
 _ :: x :: xs => last? (x :: xs)
Instance search finds the coercion, and inserts a call to coe
, which wraps the argument in some
.
However, rather than defining a Coe α (Option α)
instance, the library defines an instance of a class called CoeTail
.
Unlike Coe
, CoeTail
is consulted only as the last step in a sequence of coercions, and it is used at most once:
instance : CoeTail α (Option α) where
coe x := some x
This means that the following definition is rejected, as it would require multiple uses of the coercion:
def perhapsPerhapsPerhaps : Option (Option (Option String)) :=
"Please don't tell me"
type mismatch
"Please don't tell me"
has type
String : Type
but is expected to have type
Option (Option (Option String)) : Type
Similarly, there is a CoeHead
class that is used at most once at the beginning of a chain of coercions.
NonEmpty Lists and Dependent Coercions
An instance of Coe α β
makes sense when the type β
has a value that can represent each value from the type α
.
Coercing from Nat
to Int
makes sense, because the type Int
contains all the natural numbers.
Similarly, a coercion from nonempty lists to ordinary lists makes sense because the List
type can represent every nonempty list:
instance : Coe (NonEmptyList α) (List α) where
coe
 { head := x, tail := xs } => x :: xs
This allows nonempty lists to be used with the entire List
API.
On the other hand, it is impossible to write an instance of Coe (List α) (NonEmptyList α)
, because there's no nonempty list that can represent the empty list.
This limitation can be worked around by using another version of coercions, which are called dependent coercions.
Dependent coercions can be used when the ability to coerce from one type to another depends on which particular value is being coerced.
Just as the OfNat
type class takes the particular Nat
being overloaded as a parameter, dependent coercion takes the value being coerced as a parameter:
class CoeDep (α : Type) (x : α) (β : Type) where
coe : β
This is a chance to select only certain values, either by imposing further type class constraints on the value or by writing certain constructors directly.
For example, any List
that is not actually empty can be coerced to a NonEmptyList
:
instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
coe := { head := x, tail := xs }
Coercing to Types
In mathematics, it is common to have a concept that consists of a set equipped with additional structure. For example, a monoid is some set S, an element s of S, and an associative binary operator on S, such that s is neutral on the left and right of the operator. S is referred to as the "carrier set" of the monoid. The natural numbers with zero and addition form a monoid, because addition is associative and adding zero to any number is the identity. Similarly, the natural numbers with one and multiplication also form a monoid. Monoids are also widely used in functional programming: lists, the empty list, and the append operator form a monoid, as do strings, the empty string, and string append:
structure Monoid where
Carrier : Type
neutral : Carrier
op : Carrier → Carrier → Carrier
def natMulMonoid : Monoid :=
{ Carrier := Nat, neutral := 1, op := (· * ·) }
def natAddMonoid : Monoid :=
{ Carrier := Nat, neutral := 0, op := (· + ·) }
def stringMonoid : Monoid :=
{ Carrier := String, neutral := "", op := String.append }
def listMonoid (α : Type) : Monoid :=
{ Carrier := List α, neutral := [], op := List.append }
Given a monoid, it is possible to write the foldMap
function that, in a single pass, transforms the entries in a list into a monoid's carrier set and then combines them using the monoid's operator.
Because monoids have a neutral element, there is a natural result to return when the list is empty, and because the operator is associative, clients of the function don't have to care whether the recursive function combines elements from left to right or from right to left.
def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
let rec go (soFar : M.Carrier) : List α → M.Carrier
 [] => soFar
 y :: ys => go (M.op soFar (f y)) ys
go M.neutral xs
Even though a monoid consists of three separate pieces of information, it is common to just refer to the monoid's name in order to refer to its set. Instead of saying "Let A be a monoid and let x and y be elements of its carrier set", it is common to say "Let A be a monoid and let x and y be elements of A". This practice can be encoded in Lean by defining a new kind of coercion, from the monoid to its carrier set.
The CoeSort
class is just like the Coe
class, with the exception that the target of the coercion must be a sort, namely Type
or Prop
.
The term sort in Lean refers to these types that classify other types—Type
classifies types that themselves classify data, and Prop
classifies propositions that themselves classify evidence of their truth.
Just as Coe
is checked when a type mismatch occurs, CoeSort
is used when something other than a sort is provided in a context where a sort would be expected.
The coercion from a monoid into its carrier set extracts the carrier:
instance : CoeSort Monoid Type where
coe m := m.Carrier
With this coercion, the type signatures become less bureaucratic:
def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
let rec go (soFar : M) : List α → M
 [] => soFar
 y :: ys => go (M.op soFar (f y)) ys
go M.neutral xs
Another useful example of CoeSort
is used to bridge the gap between Bool
and Prop
.
As discussed in the section on ordering and equality, Lean's if
expression expects the condition to be a decidable proposition rather than a Bool
.
Programs typically need to be able to branch based on Boolean values, however.
Rather than have two kinds of if
expression, the Lean standard library defines a coercion from Bool
to the proposition that the Bool
in question is equal to true
:
instance : CoeSort Bool Prop where
coe b := b = true
In this case, the sort in question is Prop
rather than Type
.
Coercing to Functions
Many datatypes that occur regularly in programming consist of a function along with some extra information about it.
For example, a function might be accompanied by a name to show in logs or by some configuration data.
Additionally, putting a type in a field of a structure, similarly to the Monoid
example, can make sense in contexts where there are more than one way to implement an operation and more manual control is needed than type classes would allow.
For example, the specific details of values emitted by a JSON serializer may be important because another application expects a particular format.
Sometimes, the function itself may be derivable from just the configuration data.
A type class called CoeFun
can transform values from nonfunction types to function types.
CoeFun
has two parameters: the first is the type whose values should be transformed into functions, and the second is an output parameter that determines exactly which function type is being targeted.
class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where
coe : (x : α) → makeFunctionType x
The second parameter is itself a function that computes a type. In Lean, types are firstclass and can be passed to functions or returned from them, just like anything else.
For example, a function that adds a constant amount to its argument can be represented as a wrapper around the amount to add, rather than by defining an actual function:
structure Adder where
howMuch : Nat
A function that adds five to its argument has a 5
in the howMuch
field:
def add5 : Adder := ⟨5⟩
This Adder
type is not a function, and applying it to an argument results in an error:
#eval add5 3
function expected at
add5
term has type
Adder
Defining a CoeFun
instance causes Lean to transform the adder into a function with type Nat → Nat
:
instance : CoeFun Adder (fun _ => Nat → Nat) where
coe a := (· + a.howMuch)
#eval add5 3
8
Because all Adder
s should be transformed into Nat → Nat
functions, the argument to CoeFun
's second parameter was ignored.
When the value itself is needed to determine the right function type, then CoeFun
's second parameter is no longer ignored.
For example, given the following representation of JSON values:
inductive JSON where
 true : JSON
 false : JSON
 null : JSON
 string : String → JSON
 number : Float → JSON
 object : List (String × JSON) → JSON
 array : List JSON → JSON
deriving Repr
a JSON serializer is a structure that tracks the type it knows how to serialize along with the serialization code itself:
structure Serializer where
Contents : Type
serialize : Contents → JSON
A serializer for strings need only wrap the provided string in the JSON.string
constructor:
def Str : Serializer :=
{ Contents := String,
serialize := JSON.string
}
Viewing JSON serializers as functions that serialize their argument requires extracting the inner type of serializable data:
instance : CoeFun Serializer (fun s => s.Contents → JSON) where
coe s := s.serialize
Given this instance, a serializer can be applied directly to an argument:
def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
JSON.object [
("title", JSON.string title),
("status", JSON.number 200),
("record", R record)
]
The serializer can be passed directly to buildResponse
:
#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"
JSON.object
[("title", JSON.string "Functional Programming in Lean"),
("status", JSON.number 200.000000),
("record", JSON.string "Programming is fun!")]
Aside: JSON as a String
It can be a bit difficult to understand JSON when encoded as Lean objects.
To help make sure that the serialized response was what was expected, it can be convenient to write a simple converter from JSON
to String
.
The first step is to simplify the display of numbers.
JSON
doesn't distinguish between integers and floating point numbers, and the type Float
is used to represent both.
In Lean, Float.toString
includes a number of trailing zeros:
#eval (5 : Float).toString
"5.000000"
The solution is to write a little function that cleans up the presentation by dropping all trailing zeros, followed by a trailing decimal point:
def dropDecimals (numString : String) : String :=
if numString.contains '.' then
let noTrailingZeros := numString.dropRightWhile (· == '0')
noTrailingZeros.dropRightWhile (· == '.')
else numString
With this definition, #eval dropDecimals (5 : Float).toString
yields "5"
, and #eval dropDecimals (5.2 : Float).toString
yields "5.2"
.
The next step is to define a helper function to append a list of strings with a separator in between them:
def String.separate (sep : String) (strings : List String) : String :=
match strings with
 [] => ""
 x :: xs => String.join (x :: xs.map (sep ++ ·))
This function is useful to account for commaseparated elements in JSON arrays and objects.
#eval ", ".separate ["1", "2"]
yields "1, 2"
, #eval ", ".separate ["1"]
yields "1"
, and #eval ", ".separate []
yields ""
.
Finally, a string escaping procedure is needed for JSON strings, so that the Lean string containing "Hello!"
can be output as "\"Hello!\""
.
Happily, Lean contains a function for escaping JSON strings already, called Lean.Json.escape
.
The function that emits a string from a JSON
value is declared partial
because Lean cannot see that it terminates.
This is because recursive calls to asString
occur in functions that are being applied by List.map
, and this pattern of recursion is complicated enough that Lean cannot see that the recursive calls are actually being performed on smaller values.
In an application that just needs to produce JSON strings and doesn't need to mathematically reason about the process, having the function be partial
is not likely to cause problems.
partial def JSON.asString (val : JSON) : String :=
match val with
 true => "true"
 false => "false"
 null => "null"
 string s => "\"" ++ Lean.Json.escape s ++ "\""
 number n => dropDecimals n.toString
 object members =>
let memberToString mem :=
"\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
"{" ++ ", ".separate (members.map memberToString) ++ "}"
 array elements =>
"[" ++ ", ".separate (elements.map asString) ++ "]"
With this definition, the output of serialization is easier to read:
#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString
"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"
Messages You May Meet
Natural number literals are overloaded with the OfNat
type class.
Because coercions fire in cases where types don't match, rather than in cases of missing instances, a missing OfNat
instance for a type does not cause a coercion from Nat
to be applied:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
392
failed to synthesize instance
OfNat (Option (Option (Option Nat))) 392
Design Considerations
Coercions are a powerful tool that should be used responsibly. On the one hand, they can allow an API to naturally follow the everyday rules of the domain being modeled. This can be the difference between a bureaucratic mess of manual conversion functions and a clear program. As Abelson and Sussman wrote in the preface to Structure and Interpretation of Computer Programs (MIT Press, 1996),
Programs must be written for people to read, and only incidentally for machines to execute.
Coercions, used wisely, are a valuable means of achieving readable code that can serve as the basis for communication with domain experts. APIs that rely heavily on coercions have a number of important limitations, however. Think carefully about these limitations before using coercions in your own libraries.
First off, coercions are only applied in contexts where enough type information is available for Lean to know all of the types involved, because there are no output parameters in the coercion type classes. This means that a return type annotation on a function can be the difference between a type error and a successfully applied coercion. For example, the coercion from nonempty lists to lists makes the following program work:
def lastSpider : Option String :=
List.getLast? idahoSpiders
On the other hand, if the type annotation is omitted, then the result type is unknown, so Lean is unable to find the coercion:
def lastSpider :=
List.getLast? idahoSpiders
application type mismatch
List.getLast? idahoSpiders
argument
idahoSpiders
has type
NonEmptyList String : Type
but is expected to have type
List ?m.32938 : Type ?u.32936
More generally, when a coercion is not applied for some reason, the user receives the original type error, which can make it difficult to debug chains of coercions.
Finally, coercions are not applied in the context of field accessor notation. This means that there is still an important difference between expressions that need to be coerced and those that don't, and this difference is visible to users of your API.
Additional Conveniences
Constructor Syntax for Instances
Behind the scenes, type classes are structure types and instances are values of these types.
The only differences are that Lean stores additional information about type classes, such as which parameters are output parameters, and that instances are registered for searching.
While values that have structure types are typically defined using either ⟨...⟩
syntax or with braces and fields, and instances are typically defined using where
, both syntaxes work for both kinds of definition.
For example, a forestry application might represent trees as follows:
structure Tree : Type where
latinName : String
commonNames : List String
def oak : Tree :=
⟨"Quercus robur", ["common oak", "European oak"]⟩
def birch : Tree :=
{ latinName := "Betula pendula",
commonNames := ["silver birch", "warty birch"]
}
def beech : Tree where
latinName := "Fagus sylvatica"
commonNames := ["European beech", "common beech"]
All three syntaxes are equivalent.
Similarly, type class instances can be defined using all three syntaxes:
class Display (α : Type) where
displayName : α → String
instance : Display Tree :=
⟨Tree.latinName⟩
instance : Display Tree :=
{ displayName := Tree.latinName }
instance : Display Tree where
displayName t := t.latinName
Generally speaking, the where
syntax should be used for instances, and the curlybrace syntax should be used for structures.
The ⟨...⟩
syntax can be useful when emphasizing that a structure type is very much like a tuple in which the fields happen to be named, but the names are not important at the moment.
However, there are situations where it can make sense to use other alternatives.
In particular, a library might provide a function that constructs an instance value.
Placing a call to this function after :=
in an instance declaration is the easiest way to use such a function.
Examples
When experimenting with Lean code, definitions can be more convenient to use than #eval
or #check
commands.
First off, definitions don't produce any output, which can help keep the reader's focus on the most interesting output.
Secondly, it's easiest to write most Lean programs by starting with a type signature, allowing Lean to provide more assistance and better error messages while writing the program itself.
On the other hand, #eval
and #check
are easiest to use in contexts where Lean is able to determine the type from the provided expression.
Thirdly, #eval
cannot be used with expressions whose types don't have ToString
or Repr
instances, such as functions.
Finally, multistep do
blocks, let
expressions, and other syntactic forms that take multiple lines are particularly difficult to write with a type annotation in #eval
or #check
, simply because the required parenthesization can be difficult to predict.
To work around these issues, Lean supports the explicit indication of examples in a source file. An example is like a definition without a name. For instance, a nonempty list of birds commonly found in Copenhagen's green spaces can be written:
example : NonEmptyList String :=
{ head := "Sparrow",
tail := ["Duck", "Swan", "Magpie", "Eurasian coot", "Crow"]
}
Examples may create define functions by accepting arguments:
example (n : Nat) (k : Nat) : Bool :=
n + k == k + n
While this creates a function behind the scenes, this function has no name and cannot be called.
Nonetheless, this is useful for demonstrating how a library can be used with arbitrary or unknown values of some given type.
In source files, example
declarations are best paired with comments that explain how the example illustrates the concepts of the library.
Summary
Type Classes and Overloading
Type classes are Lean's mechanism for overloading functions and operators. A polymorphic function can be used with multiple types, but it behaves in the same manner no matter which type it is used with. For example, a polymorphic function that appends two lists can be used no matter the type of the entries in the list, but it is unable to have different behavior depending on which particular type is found. An operation that is overloaded with type classes, on the other hand, can also be used with multiple types. However, each type requires its own implementation of the overloaded operation. This means that the behavior can vary based on which type is provided.
A type class has a name, parameters, and a body that consists of a number of names with types. The name is a way to refer to the overloaded operations, the parameters determine which aspects of the definitions can be overloaded, and the body provides the names and type signatures of the overloadable operations. Each overloadable operation is called a method of the type class. Type classes may provide default implementations of some methods in terms of the others, freeing implementors from defining each overload by hand when it is not needed.
An instance of a type class provides implementations of the methods for given parameters. Instances may be polymorphic, in which case they can work for a variety of parameters, and they may optionally provide more specific implementations of default methods in cases where a more efficient version exists for some particular type.
Type class parameters are either input parameters (the default), or output parameters (indicated by an outParam
modifier).
Lean will not begin searching for an instance until all input parameters are no longer metavariables, while output parameters may be solved while searching for instances.
Parameters to a type class need not be types—they may also be ordinary values.
The OfNat
type class, used to overload natural number literals, takes the overloaded Nat
itself as a parameter, which allows instances to restrict the allowed numbers.
Instances may be marked with a @[default_instance]
attribute.
When an instance is a default instance, then it will be chosen as a fallback when Lean would otherwise fail to find an instance due to the presence of metavariables in the type.
Type Classes for Common Syntax
Most infix operators in Lean are overridden with a type class.
For instance, the addition operator corresponds to a type class called Add
.
Most of these operators have a corresponding heterogeneous version, in which the two arguments need not have the same type.
These heterogenous operators are overloaded using a version of the class whose name starts with H
, such as HAdd
.
Indexing syntax is overloaded using a type class called GetElem
, which involves proofs.
GetElem
has two output parameters, which are the type of elements to be extracted from the collection and a function that can be used to determine what counts as evidence that the index value is in bounds for the collection.
This evidence is described by a proposition, and Lean attempts to prove this proposition when array indexing is used.
When Lean is unable to check that list or array access operations are in bounds at compile time, the check can be deferred to run time by appending a ?
to the indexing operation.
Functors
A functor is a polymorphic type that supports a mapping operation. This mapping operation transforms all elements "in place", changing no other structure. For instance, lists are functors and the mapping operation may neither drop, duplicate, nor mix up entries in the list.
While functors are defined by having map
, the Functor
type class in Lean contains an additional default method that is responsible for mapping the constant function over a value, replacing all values whose type are given by polymorphic type variable with the same new value.
For some functors, this can be done more efficiently than traversing the entire structure.
Deriving Instances
Many type classes have very standard implementations.
For instance, the Boolean equality class BEq
is usually implemented by first checking whether both arguments are built with the same constructor, and then checking whether all their arguments are equal.
Instances for these classes can be created automatically.
When defining an inductive type or a structure, a deriving
clause at the end of the declaration will cause instances to be created automatically.
Additionally, the deriving instance ... for ...
command can be used outside of the definition of a datatype to cause an instance to be generated.
Because each class for which instances can be derived requires special handling, not all classes are derivable.
Coercions
Coercions allow Lean to recover from what would normally be a compiletime error by inserting a call to a function that transforms data from one type to another.
For example, the coercion from any type α
to the type Option α
allows values to be written directly, rather than with the some
constructor, making Option
work more like nullable types from objectoriented languages.
There are multiple kinds of coercion.
They can recover from different kinds of errors, and they are represented by their own type classes.
The Coe
class is used to recover from type errors.
When Lean has an expression of type α
in a context that expects something with type β
, Lean first attempts to string together a chain of coercions that can transform α
s into β
s, and only displays the error when this cannot be done.
The CoeDep
class takes the specific value being coerced as an extra parameter, allowing either further type class search to be done on the value or allowing constructors to be used in the instance to limit the scope of the conversion.
The CoeFun
class intercepts what would otherwise be a "not a function" error when compiling a function application, and allows the value in the function position to be transformed into an actual function if possible.
Monads
In C# and Kotlin, the ?.
operator is a way to look up a property or call a method on a potentiallynull value.
If the reciever is null
, the whole expression is null.
Otherwise, the underlying nonnull
value receives the call.
Uses of ?.
can be chained, in which case the first null
result terminates the chain of lookups.
In Lean, pattern matching can be used to chain checks for null. Getting the first entry from a list can just use the optional indexing notation:
def first (xs : List α) : Option α :=
xs[0]?
The result must be an Option
because empty lists have no first entry.
Extracting the first and third entries requires a check that each is not none
:
def firstThird (xs : List α) : Option (α × α) :=
match xs[0]? with
 none => none
 some first =>
match xs[2]? with
 none => none
 some third =>
some (first, third)
Similarly, extracting the first, third, and fifth entries requires more checks that the values are not none
:
def firstThirdFifth (xs : List α) : Option (α × α × α) :=
match xs[0]? with
 none => none
 some first =>
match xs[2]? with
 none => none
 some third =>
match xs[4]? with
 none => none
 some fifth =>
some (first, third, fifth)
And adding the seventh entry to this sequence begins to become quite unmanageable:
def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
match xs[0]? with
 none => none
 some first =>
match xs[2]? with
 none => none
 some third =>
match xs[4]? with
 none => none
 some fifth =>
match xs[6]? with
 none => none
 some seventh =>
some (first, third, fifth, seventh)
Checking for none
: Don't Repeat Yourself
The fundamental problem with this code is that it addresses two concerns: extracting the numbers and checking that all of them are present, but the second concern is addressed by copying and pasting the code that handles the none
case.
It is often good style to lift a repetitive segment into a helper function:
def andThen (opt : Option α) (next : α → Option β) : Option β :=
match opt with
 none => none
 some x => next x
This helper, which is used similarly to ?.
in C# and Kotlin, takes care of propagating none
values.
It takes two arguments: an optional value and a function to apply when the value is not none
.
If the first argument is none
, then the helper returns none
.
If the first argument is not none
, then the function is applied to the contents of the some
constructor.
Now, firstThird
can be rewritten to use andThen
instead of pattern matching:
def firstThird (xs : List α) : Option (α × α) :=
andThen xs[0]? fun first =>
andThen xs[2]? fun third =>
some (first, third)
In Lean, functions don't need to be enclosed in parentheses when passed as arguments. The following equivalent definition uses more parentheses and indents the bodies of functions:
def firstThird (xs : List α) : Option (α × α) :=
andThen xs[0]? (fun first =>
andThen xs[2]? (fun third =>
some (first, third)))
The andThen
helper provides a sort of "pipeline" through which values flow, and the version with the somewhat unusual indentation is more suggestive of this fact.
Improving the syntax used to write andThen
can make these computations even easier to understand.
Infix Operators
In Lean, infix operators can be declared using the infix
, infixl
, and infixr
commands, which create (respectively) nonassociative, leftassociative, and rightassociative operators.
When used multiple times in a row, a left associative operator stacks up the opening parentheses on the left side of the expression.
The addition operator +
is left associative, so w + x + y + z
is equivalent to (((w + x) + y) + z)
.
The exponentiation operator ^
is right associative, so w ^ x ^ y ^ z
is equivalent to (w ^ (x ^ (y ^ z)))
.
Comparison operators such as <
are nonassociative, so x < y < z
is a syntax error and requires manual parentheses.
The following declaration makes andThen
into an infix operator:
infixl:55 " ~~> " => andThen
The number following the colon declares the precedence of the new infix operator.
In ordinary mathematical notation, x + y * z
is equivalent to x + (y * z)
even though both +
and *
are left associative.
In Lean, +
has precedence 65 and *
has precedence 70.
Higherprecedence operators are applied before lowerprecedence operators.
According to the declaration of ~~>
, both +
and *
have higher precedence, and thus apply first.
Typically, figuring out the most convenient precedences for a group of operators requires some experimentation and a large collection of examples.
Following the new infix operator is a double arrow =>
, which specifies the named function to be used for the infix operator.
Lean's standard library uses this feature to define +
and *
as infix operators that point at HAdd.hAdd
and HMul.hMul
, respectively, allowing type classes to be used to overloading the infix operators.
Here, however, andThen
is just an ordinary function.
Having defined an infix operator for andThen
, firstThird
can be rewritten in a way that brings the "pipeline" feeling of none
checks front and center:
def firstThirdInfix (xs : List α) : Option (α × α) :=
xs[0]? ~~> fun first =>
xs[2]? ~~> fun third =>
some (first, third)
This style is much more concise when writing larger functions:
def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
xs[0]? ~~> fun first =>
xs[2]? ~~> fun third =>
xs[4]? ~~> fun fifth =>
xs[6]? ~~> fun seventh =>
some (first, third, fifth, seventh)
Propagating Error Messages
Pure functional languages such as Lean have no builtin exception mechanism for error handling, because throwing or catching an exception is outside of the stepbystep evaluation model for expressions.
However, functional programs certainly need to handle errors.
In the case of firstThirdFifthSeventh
, it is likely relevant for a user to know just how long the list was and where the lookup failed.
This is typically accomplished by defining a datatype that can be either an error or a result, and translating functions with exceptions into functions that return this datatype:
inductive Except (ε : Type) (α : Type) where
 error : ε → Except ε α
 ok : α → Except ε α
deriving BEq, Hashable, Repr
The type variable ε
stands for the type of errors that can be produced by the function.
Callers are expected to handle both errors and successes, which makes the type variable ε
play a role that is a bit like that of a list of checked exceptions in Java.
Similarly to Option
, Except
can be used to indicate a failure to find an entry in a list.
In this case, the error type is a String
:
def get (xs : List α) (i : Nat) : Except String α :=
match xs[i]? with
 none => Except.error s!"Index {i} not found (maximum is {xs.length  1})"
 some x => Except.ok x
Looking up an inbounds value yields an Except.ok
:
def ediblePlants : List String :=
["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]
#eval get ediblePlants 2
Except.ok "sea buckthorn"
Looking up an outofbounds value yields an Except.failure
:
#eval get ediblePlants 4
Except.error "Index 4 not found (maximum is 3)"
A single list lookup can conveniently return a value or an error:
def first (xs : List α) : Except String α :=
get xs 0
However, performing two list lookups requires handling potential failures:
def firstThird (xs : List α) : Except String (α × α) :=
match get xs 0 with
 Except.error msg => Except.error msg
 Except.ok first =>
match get xs 2 with
 Except.error msg => Except.error msg
 Except.ok third =>
Except.ok (first, third)
Adding another list lookup to the function requires still more error handling:
def firstThirdFifth (xs : List α) : Except String (α × α × α) :=
match get xs 0 with
 Except.error msg => Except.error msg
 Except.ok first =>
match get xs 2 with
 Except.error msg => Except.error msg
 Except.ok third =>
match get xs 4 with
 Except.error msg => Except.error msg
 Except.ok fifth =>
Except.ok (first, third, fifth)
And one more list lookup begins to become quite unmanageable:
def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
match get xs 0 with
 Except.error msg => Except.error msg
 Except.ok first =>
match get xs 2 with
 Except.error msg => Except.error msg
 Except.ok third =>
match get xs 4 with
 Except.error msg => Except.error msg
 Except.ok fifth =>
match get xs 6 with
 Except.error msg => Except.error msg
 Except.ok seventh =>
Except.ok (first, third, fifth, seventh)
Once again, a common pattern can be factored out into a helper.
Each step through the function checks for an error, and only proceeds with the rest of the computation if the result was a success.
A new version of andThen
can be defined for Except
:
def andThen (attempt : Except e α) (next : α → Except e β) : Except e β :=
match attempt with
 Except.error msg => Except.error msg
 Except.ok x => next x
Just as with Option
, this version of andThen
allows a more concise definition of firstThird
:
def firstThird' (xs : List α) : Except String (α × α) :=
andThen (get xs 0) fun first =>
andThen (get xs 2) fun third =>
Except.ok (first, third)
In both the Option
and Except
case, there are two repeating patterns: there is the checking of intermediate results at each step, which has been factored out into andThen
, and there is the final successful result, which is some
or Except.ok
, respectively.
For the sake of convenience, success can be factored out into a helper called ok
:
def ok (x : α) : Except ε α := Except.ok x
Similarly, failure can be factored out into a helper called fail
:
def fail (err : ε) : Except ε α := Except.error err
Using ok
and fail
makes get
a little more readable:
def get (xs : List α) (i : Nat) : Except String α :=
match xs[i]? with
 none => fail s!"Index {i} not found (maximum is {xs.length  1})"
 some x => ok x
After adding the infix declaration for andThen
, firstThird
can be just as concise as the version that returns an Option
:
infixl:55 " ~~> " => andThen
def firstThird (xs : List α) : Except String (α × α) :=
get xs 0 ~~> fun first =>
get xs 2 ~~> fun third =>
ok (first, third)
The technique scales similarly to larger functions:
def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
get xs 0 ~~> fun first =>
get xs 2 ~~> fun third =>
get xs 4 ~~> fun fifth =>
get xs 6 ~~> fun seventh =>
ok (first, third, fifth, seventh)
Logging
A number is even if dividing it by 2 leaves no remainder:
def isEven (i : Int) : Bool :=
i % 2 == 0
The function sumAndFindEvens
computes the sum of a list while remembering the even numbers encountered along the way:
def sumAndFindEvens : List Int → List Int × Int
 [] => ([], 0)
 i :: is =>
let (moreEven, sum) := sumAndFindEvens is
(if isEven i then i :: moreEven else moreEven, sum + i)
This function is a simplified example of a common pattern.
Many programs need to traverse a data structure once, while both computing a main result and accumulating some kind of tertiary extra result.
One example of this is logging: a program that is an IO
action can always log to a file on disk, but because the disk is outside of the mathematical world of Lean functions, it becomes much more difficult to prove things about logs based on IO
.
Another example is a function that computes the sum of all the nodes in a tree with a preorder traversal, while simultaneously recording each nodes visited:
def preorderSum : BinTree Int → List Int × Int
 BinTree.leaf => ([], 0)
 BinTree.branch l x r =>
let (leftVisited, leftSum) := preorderSum l
let (hereVisited, hereSum) := ([x], x)
let (rightVisited, rightSum) := preorderSum r
(leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)
Both sumAndFindEvens
and preorderSum
have a common repetitive structure.
Each step of computation returns a pair that consists of a list of data that have been saved along with the primary result.
The lists are then appended, and the primary result is computed and paired with the appended lists.
The common structure becomes more apparent with a small rewrite of sumAndFindEvens
that more cleanly separates the concerns of saving even numbers and computing the sum:
def sumAndFindEvens : List Int → List Int × Int
 [] => ([], 0)
 i :: is =>
let (moreEven, sum) := sumAndFindEvens is
let (evenHere, ⟨⟩) := (if isEven i then [i] else [], Unit.unit)
(evenHere ++ moreEven, sum + i)
For the sake of clarity, a pair that consists of an accumulated result together with a value can be given its own name:
structure WithLog (logged : Type) (α : Type) where
log : List logged
val : α
Similarly, the process of saving a list of accumulated results while passing a value on to the next step of a computation can be factored out into a helper, once again named andThen
:
def andThen (result : WithLog α β) (next : β → WithLog α γ) : WithLog α γ :=
let {log := thisOut, val := thisRes} := result
let {log := nextOut, val := nextRes} := next thisRes
{log := thisOut ++ nextOut, val := nextRes}
In the case of errors, ok
represents an operation that always succeeds.
Here, however, it is an operation that simply returns a value without logging anything:
def ok (x : β) : WithLog α β := {log := [], val := x}
Just as Except
provides fail
as a possibility, WithLog
should allow items to be added to a log.
This has no interesting return value associated with it, so it returns Unit
:
def save (data : α) : WithLog α Unit :=
{log := [data], val := ⟨⟩}
WithLog
, andThen
, ok
, and save
can be used to separate the logging concern from the summing concern in both programs:
def sumAndFindEvens : List Int → WithLog Int Int
 [] => ok 0
 i :: is =>
andThen (if isEven i then save i else ok ⟨⟩) fun ⟨⟩ =>
andThen (sumAndFindEvens is) fun sum =>
ok (i + sum)
def preorderSum : BinTree Int → WithLog Int Int
 BinTree.leaf => ok 0
 BinTree.branch l x r =>
andThen (preorderSum l) fun leftSum =>
andThen (save x) fun ⟨⟩ =>
andThen (preorderSum r) fun rightSum =>
ok (leftSum + x + rightSum)
And, once again, the infix operator helps put focus on the correct steps:
infixl:55 " ~~> " => andThen
def sumAndFindEvens : List Int → WithLog Int Int
 [] => ok 0
 i :: is =>
(if isEven i then save i else ok ⟨⟩) ~~> fun ⟨⟩ =>
sumAndFindEvens is ~~> fun sum =>
ok (i + sum)
def preorderSum : BinTree Int → WithLog Int Int
 BinTree.leaf => ok 0
 BinTree.branch l x r =>
preorderSum l ~~> fun leftSum =>
save x ~~> fun ⟨⟩ =>
preorderSum r ~~> fun rightSum =>
ok (leftSum + x + rightSum)
Numbering Tree Nodes
A preorder numbering of a tree associates each data point in the tree with the step it would be visited at in a preorder traversal of the tree.
For example, consider aTree
:
open BinTree in
def aTree :=
branch
(branch
(branch leaf "a" (branch leaf "b" leaf))
"c"
leaf)
"d"
(branch leaf "e" leaf)
Its preorder numbering is:
BinTree.branch
(BinTree.branch
(BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
(2, "c")
(BinTree.leaf))
(3, "d")
(BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))
Trees are most naturally processed with recursive functions, but the usual pattern of recursion on trees makes it difficult to compute a preorder numbering. This is because the nodes in the right subtree should be numbered starting from the highest number assigned in the left subtree. In an imperative language, this issue can be worked around by using a mutable variable that contains the next number to be assigned. The following Python program computes a preorder numbering using a mutable variable:
class Branch:
def __init__(self, value, left=None, right=None):
self.left = left
self.value = value
self.right = right
def __repr__(self):
return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'
def number(tree):
num = 0
def helper(t):
nonlocal num
if t is None:
return None
else:
new_left = helper(t.left)
new_value = (num, t.value)
num += 1
new_right = helper(t.right)
return Branch(left=new_left, value=new_value, right=new_right)
return helper(tree)
The numbering of the Python equivalent of aTree
is:
a_tree = Branch("d",
left=Branch("c",
left=Branch("a", left=None, right=Branch("b")),
right=None),
right=Branch("e"))
and its numbering is:
>>> number(a_tree)
Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))
Even though Lean does not have mutable variables, a workaround exists. From the point of view of the rest of the world, the mutable variable can be thought of as having two relevant aspects: its value when the function is called, and its value when the function returns. In other words, a function that uses a mutable variable can be seen as a function that takes the mutable variable's starting value as an argument, returning a pair of the variable's final value and the function's result. This final value can then be passed as an argument to the next step.
Just as the Python example uses an outer function that establishes a mutable variable and an inner helper function that changes the variable, a Lean version of the function uses an outer function that provides the variable's starting value and explicitly returns the function's result along with an inner helper function that threads the variable's value while computing the numbered tree:
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α))
 BinTree.leaf => (n, BinTree.leaf)
 BinTree.branch left x right =>
let (k, numberedLeft) := helper n left
let (i, numberedRight) := helper (k + 1) right
(i, BinTree.branch numberedLeft (k, x) numberedRight)
(helper 0 t).snd
This code, like the none
propagating Option
code, the error
propagating Except
code, and the logaccumulating WithLog
code, commingles two concerns: propagating the value of the counter, and actually traversing the tree to find the result.
Just as in those cases, an andThen
helper can be defined to propagate state from one step of a computation to another.
The first step is to give a name to the pattern of taking an input state as an argument and returning an output state together with a value:
def State (σ : Type) (α : Type) : Type :=
σ → (σ × α)
In the case of State
, ok
is a function that returns the input state unchanged, along with the provided value:
def ok (x : α) : State σ α :=
fun s => (s, x)
When working with a mutable variable, there are two fundamental operations: reading the value and replacing it with a new one. Reading the current value is accomplished with a function that places the input state unmodified into the output state, and also places it into the value field:
def get : State σ σ :=
fun s => (s, s)
Writing a new value consists of ignoring the input state, and placing the provided new value into the output state:
def set (s : σ) : State σ Unit :=
fun _ => (s, ⟨⟩)
Finally, two computations that use state can be sequence by finding both the output state and return value of the first function, then passing them both into the next function:
def andThen (first : State σ α) (next : α → State σ β) : State σ β :=
fun s =>
let (s', x) := first s
next x s'
infixl:55 " ~~> " => andThen
Using State
and its helpers, local mutable state can be simulated:
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
 BinTree.leaf => ok BinTree.leaf
 BinTree.branch left x right =>
helper left ~~> fun numberedLeft =>
get ~~> fun n =>
set (n + 1) ~~> fun ⟨⟩ =>
helper right ~~> fun numberedRight =>
ok (BinTree.branch numberedLeft (n, x) numberedRight)
(helper t 0).snd
Because State
simulates only a single local variable, get
and set
don't need to refer to any particular variable name.
Monads: A Functional Design Pattern
Each of these examples has consisted of:
 A polymorphic type, such as
Option
,Except ε
,WithLog logged
, orState σ
 An operator
andThen
that takes care of some repetitive aspect of sequencing programs that have this type  An operator
ok
that is (in some sense) the most boring way to use the type  A collection of other operations, such as
none
,fail
,save
, andget
, that name ways of using the type
This style of API is called a monad.
While the idea of monads is derived from a branch of mathematics called category theory, no understanding of category theory is needed in order to use them for programming.
The key idea of monads is that each monad encodes a particular kind of side effect using the tools provided by the pure functional language Lean.
For example, Option
represents programs that can fail by returning none
, Except
represents programs that can throw exceptions, WithLog
represents programs that accumulate a log while running, and State
represents programs with a single mutable variable.
The Monad Type Class
Rather than having to import an operator like ok
or andThen
for each type that is a monad, the Lean standard library contains a type class that allow them to be overloaded, so that the same operators can be used for any monad.
Monads have two operations, which are the equivalent of ok
and andThen
:
class Monad (m : Type → Type) where
pure : α → m α
bind : m α → (α → m β) → m β
This definition is slightly simplified. The actual definition in the Lean library is somewhat more involved, and will be presented later.
The Monad
instances for Option
and Except
can be created by adapting the definitions of their respective andThen
operations:
instance : Monad Option where
pure x := some x
bind opt next :=
match opt with
 none => none
 some x => next x
instance : Monad (Except ε) where
pure x := Except.ok x
bind attempt next :=
match attempt with
 Except.error e => Except.error e
 Except.ok x => next x
As an example, firstThirdFifthSeventh
was defined separately for Option α
and Except String α
return types.
Now, it can be defined polymorphically for any monad.
It does, however, require a lookup function as an argument, because different monads might fail to find a result in different ways.
The infix version of bind
is >>=
, which plays the same role as ~~>
in the examples.
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
lookup xs 0 >>= fun first =>
lookup xs 2 >>= fun third =>
lookup xs 4 >>= fun fifth =>
lookup xs 6 >>= fun seventh =>
pure (first, third, fifth, seventh)
Given example lists of slow mammals and fast birds, this implementation of firstThirdFifthSeventh
can be used with Option
:
def slowMammals : List String :=
["Threetoed sloth", "Slow loris"]
def fastBirds : List String := [
"Peregrine falcon",
"Saker falcon",
"Golden eagle",
"Grayheaded albatross",
"Spurwinged goose",
"Swift",
"Anna's hummingbird"
]
#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals
none
#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds
some ("Peregrine falcon", "Golden eagle", "Spurwinged goose", "Anna's hummingbird")
After renaming Except
's lookup function get
to something more specific, the very same implementation of firstThirdFifthSeventh
can be used with Except
as well:
def getOrExcept (xs : List α) (i : Nat) : Except String α :=
match xs[i]? with
 none => Except.error s!"Index {i} not found (maximum is {xs.length  1})"
 some x => Except.ok x
#eval firstThirdFifthSeventh getOrExcept slowMammals
Except.error "Index 2 not found (maximum is 1)"
#eval firstThirdFifthSeventh getOrExcept fastBirds
Except.ok ("Peregrine falcon", "Golden eagle", "Spurwinged goose", "Anna's hummingbird")
The fact that m
must have a Monad
instance means that the >>=
and pure
operations are available.
General Monad Operations
Because many different types are monads, functions that are polymorphic over any monad are very powerful.
For example, the function mapM
is a version of map
that uses a Monad
to sequence and combine the results of applying a function:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
 [] => pure []
 x :: xs =>
f x >>= fun hd =>
mapM f xs >>= fun tl =>
pure (hd :: tl)
The return type of the function argument f
determines which Monad
instance will be used.
In other words, mapM
can be used for functions that produce logs, for functions that can fail, or for functions that use mutable state.
Because f
's type determines the available effects, they can be tightly controlled by API designers.
As described in this chapter's introduction, State σ α
represents programs that make use of a mutable variable of type σ
and return a value of type α
.
These programs are actually functions from a starting state to a pair of a value and a final state.
The Monad
class requires that its parameter expect a single type argument—that is, it should be a Type → Type
.
This means that the instance for State
should mention the state type σ
, which becomes a parameter to the instance:
instance : Monad (State σ) where
pure x := fun s => (s, x)
bind first next :=
fun s =>
let (s', x) := first s
next x s'
This means that the type of the state cannot change between calls to get
and set
that are sequence using bind
, which is a reasonable rule for stateful computations.
The operator increment
increases a saved state by a given amount, returning the old value:
def increment (howMuch : Int) : State Int Int :=
get >>= fun i =>
set (i + howMuch) >>= fun ⟨⟩ =>
pure i
Using mapM
with increment
results in a program that computes the sum of the entries in a list.
More specifically, the mutable variable contains the sum so far, while the resulting list contains a running sum.
In other words, mapM increment
has type List Int → State Int (List Int)
, and expanding the definition of State
yields List Int → Int → (Int × List Int)
.
It takes an initial sum as an argument, which should be 0
:
#eval mapM increment [1, 2, 3, 4, 5] 0
(15, [0, 1, 3, 6, 10])
A logging effect can be represented using WithLog
.
Just like State
, its Monad
instance is polymorphic with respect to the type of the logged data:
instance : Monad (WithLog logged) where
pure x := {log := [], val := x}
bind result next :=
let {log := thisOut, val := thisRes} := result
let {log := nextOut, val := nextRes} := next thisRes
{log := thisOut ++ nextOut, val := nextRes}
saveIfEven
is a function that logs even numbers but returns its argument unchanged:
def saveIfEven (i : Int) : WithLog Int Int :=
(if isEven i then
save i
else pure ⟨⟩) >>= fun ⟨⟩ =>
pure i
Using this function with mapM
results in a log containing even numbers paired with an unchanged input list:
#eval mapM saveIfEven [1, 2, 3, 4, 5]
{ log := [2, 4], val := [1, 2, 3, 4, 5] }
The Identity Monad
Monads encode programs with effects, such as failure, exceptions, or logging, into explicit representations as data and functions. Sometimes, however, an API will be written to use a monad for flexibility, but the API's client may not require any encoded effects. The identity monad is a monad that has no effects, and allows pure code to be used with monadic APIs:
def Id (t : Type) : Type := t
instance : Monad Id where
pure x := x
bind x f := f x
The type of pure
should be α → Id α
, but Id α
reduces to just α
.
Similarly, the type of bind
should be α → (α → Id β) → Id β
.
Because this reduces to α → (α → β) → β
, the second argument can be applied to the first to find the result.
With the identity monad, mapM
becomes equivalent to map
.
To call it this way, however, Lean requires a hint that the intended monad is Id
:
#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]
[2, 3, 4, 5, 6]
Omitting the hint results in an error:
#eval mapM (· + 1) [1, 2, 3, 4, 5]
failed to synthesize instance
HAdd Nat Nat (?m.8896 ?m.8898)
In this error, the application of one metavariable to another indicates that Lean doesn't run the typelevel computation backwards.
The return type of the function is expected to be the monad applied to some other type.
Similarly, using mapM
with a function whose type doesn't provide any specific hints about which monad is to be used results in an "instance problem stuck" message:
#eval mapM (fun x => x) [1, 2, 3, 4, 5]
typeclass instance problem is stuck, it is often due to metavariables
Monad ?m.8896
The Monad Contract
Just as every pair of instances of BEq
and Hashable
should ensure that any two equal values have the same hash, there is a contract that each instance of Monad
should obey.
First, pure
should be a left identity of bind
.
That is, bind (pure v) f
should be the same as f v
.
Secondly, pure
should be a right identity of bind
, so bind v pure
is the same as v
.
Finally, bind
should be associative, so bind (bind v f) g
is the same as bind v (fun x => bind (f x) g)
.
This contract specifies the expected properties of programs with effects more generally.
Because pure
has no effects, sequencing its effects with bind
shouldn't change the result.
The associative property of bind
basically says that the sequencing bookkeeping itself doesn't matter, so long as the order in which things are happening is preserved.
Exercises
Mapping on a Tree
Define a function BinTree.mapM
.
By analogy to mapM
for lists, this function should apply a monadic function to each data entry in a tree, as a preorder traversal.
The type signature should be:
def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)
The Option Monad Contract
First, write a convincing argument that the Monad
instance for Option
satisfies the monad contract.
Then, consider the following instance:
instance : Monad Option where
pure x := some x
bind opt next := none
Both methods have the correct type. Why does this instance violate the monad contract?
Example: Arithmetic in Monads
Monads are a way of encoding programs with side effects into a language that does not have them.
It would be easy to read this as a sort of admission that pure functional programs are missing something important, requiring programmers to jump through hoops just to write a normal program.
However, while using the Monad
API does impose a syntactic cost on a program, it brings two important benefits:
 Programs must be honest about which effects they use in their types. A quick glance at a type signature describes everything that the program can do, rather than just what it accepts and what it returns.
 Not every language provides the same effects. For example, only some language have exceptions. Other languages have unique, exotic effects, such as Icon's searching over multiple values and Scheme or Ruby's continuations. Because monads can encode any effect, programmers can choose which ones are the best fit for a given application, rather than being stuck with what the language developers provided.
One example of a program that can make sense in a variety of monads is an evaluator for arithmetic expressions.
Arithmetic Expressions
An arithmetic expression is either a literal integer or a primitive binary operator applied to two expressions. The operators are addition, subtraction, multiplication, and division:
inductive Expr (op : Type) where
 const : Int → Expr op
 prim : op → Expr op → Expr op → Expr op
inductive Arith where
 plus
 minus
 times
 div
The expression 2 + 3
is represented:
open Expr in
open Arith in
def twoPlusThree : Expr Arith :=
prim plus (const 2) (const 3)
and 14 / (45  5 * 9)
is represented:
open Expr in
open Arith in
def fourteenDivided : Expr Arith :=
prim div (const 14) (prim minus (const 45) (prim times (const 5) (const 9)))
Evaluating Expressions
Because expressions include division, and division by zero is undefined, evaluation might fail.
One way to represent failure is to use Option
:
def evaluateOption : Expr Arith → Option Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateOption e1 >>= fun v1 =>
evaluateOption e2 >>= fun v2 =>
match p with
 Arith.plus => pure (v1 + v2)
 Arith.minus => pure (v1  v2)
 Arith.times => pure (v1 * v2)
 Arith.div => if v2 == 0 then none else pure (v1 / v2)
This definition uses the Monad Option
instance to propagate failures from evaluating both branches of a binary operator.
However, the function mixes two concerns: evaluating subexpressions and applying a binary operator to the results.
It can be improved by splitting it into two functions:
def applyPrim : Arith → Int → Int → Option Int
 Arith.plus, x, y => pure (x + y)
 Arith.minus, x, y => pure (x  y)
 Arith.times, x, y => pure (x * y)
 Arith.div, x, y => if y == 0 then none else pure (x / y)
def evaluateOption : Expr Arith → Option Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateOption e1 >>= fun v1 =>
evaluateOption e2 >>= fun v2 =>
applyPrim p v1 v2
Running #eval evaluateOption fourteenDivided
yields none
, as expected, but this is not a very useful error message.
Because the code was written using >>=
rather than by explicitly handling the none
constructor, only a small modification is required for it to provide an error message on failure:
def applyPrim : Arith → Int → Int → Except String Int
 Arith.plus, x, y => pure (x + y)
 Arith.minus, x, y => pure (x  y)
 Arith.times, x, y => pure (x * y)
 Arith.div, x, y =>
if y == 0 then
Except.error s!"Tried to divide {x} by zero"
else pure (x / y)
def evaluateExcept : Expr Arith → Except String Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateExcept e1 >>= fun v1 =>
evaluateExcept e2 >>= fun v2 =>
applyPrim p v1 v2
The only difference is that the type signature mentions Except String
instead of Option
, and the failing case uses Except.error
instead of none
.
By making evaluate
polymorphic over its monad and passing it applyPrim
as an argument, a single evaluator becomes capable of both forms of error reporting:
def applyPrimOption : Arith → Int → Int → Option Int
 Arith.plus, x, y => pure (x + y)
 Arith.minus, x, y => pure (x  y)
 Arith.times, x, y => pure (x * y)
 Arith.div, x, y =>
if y == 0 then
none
else pure (x / y)
def applyPrimExcept : Arith → Int → Int → Except String Int
 Arith.plus, x, y => pure (x + y)
 Arith.minus, x, y => pure (x  y)
 Arith.times, x, y => pure (x * y)
 Arith.div, x, y =>
if y == 0 then
Except.error s!"Tried to divide {x} by zero"
else pure (x / y)
def evaluateM [Monad m] (applyPrim : Arith → Int → Int → m Int): Expr Arith → m Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateM applyPrim e1 >>= fun v1 =>
evaluateM applyPrim e2 >>= fun v2 =>
applyPrim p v1 v2
Using it with applyPrimOption
works just like the first version of evaluate
:
#eval evaluateM applyPrimOption fourteenDivided
none
Similarly, using it with applyPrimExcept
works just like the version with error messages:
#eval evaluateM applyPrimExcept fourteenDivided
Except.error "Tried to divide 14 by zero"
The code can still be improved.
The functions applyPrimOption
and applyPrimExcept
differ only in their treatment of division, which can be extracted into another parameter to the evaluator:
def applyDivOption (x : Int) (y : Int) : Option Int :=
if y == 0 then
none
else pure (x / y)
def applyDivExcept (x : Int) (y : Int) : Except String Int :=
if y == 0 then
Except.error s!"Tried to divide {x} by zero"
else pure (x / y)
def applyPrim [Monad m] (applyDiv : Int → Int → m Int) : Arith → Int → Int → m Int
 Arith.plus, x, y => pure (x + y)
 Arith.minus, x, y => pure (x  y)
 Arith.times, x, y => pure (x * y)
 Arith.div, x, y => applyDiv x y
def evaluateM [Monad m] (applyDiv : Int → Int → m Int): Expr Arith → m Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateM applyDiv e1 >>= fun v1 =>
evaluateM applyDiv e2 >>= fun v2 =>
applyPrim applyDiv p v1 v2
In this refactored code, the fact that the two code paths differ only in their treatment of failure has been made fully apparent.
Further Effects
Failure and exceptions are not the only kinds of effects that can be interesting when working with an evaluator. While division's only side effect is failure, adding other primitive operators to the expressions make it possible to express other effects.
The first step is an additional refactoring, extracting division from the datatype of primitives:
inductive Prim (special : Type) where
 plus
 minus
 times
 other : special → Prim special
inductive CanFail where
 div
The name CanFail
suggests that the effect introduced by division is potential failure.
The second step is to broaden the scope of the division handler argument to evaluateM
so that it can process any special operator:
def divOption : CanFail → Int → Int → Option Int
 CanFail.div, x, y => if y == 0 then none else pure (x / y)
def divExcept : CanFail → Int → Int → Except String Int
 CanFail.div, x, y =>
if y == 0 then
Except.error s!"Tried to divide {x} by zero"
else pure (x / y)
def applyPrim [Monad m] (applySpecial : special → Int → Int → m Int) : Prim special → Int → Int → m Int
 Prim.plus, x, y => pure (x + y)
 Prim.minus, x, y => pure (x  y)
 Prim.times, x, y => pure (x * y)
 Prim.other op, x, y => applySpecial op x y
def evaluateM [Monad m] (applySpecial : special → Int → Int → m Int): Expr (Prim special) → m Int
 Expr.const i => pure i
 Expr.prim p e1 e2 =>
evaluateM applySpecial e1 >>= fun v1 =>
evaluateM applySpecial e2 >>= fun v2 =>
applyPrim applySpecial p v1 v2
No Effects
The type Empty
has no constructors, and thus no values, like the Nothing
type in Scala or Kotlin.
In Scala and Kotlin, Nothing
can represent computations that never return a result, such as functions that crash the program, throw exceptions, or always fall into infinite loops.
An argument to a function or method of type Nothing
indicates dead code, as there will never be a suitable argument value.
Lean doesn't support infinite loops and exceptions, but Empty
is still useful as an indication to the type system that a function cannot be called.
Using the syntax nomatch E
when E
is an expression whose type has no constructors indicates to Lean that the current expression need not return a result, because it could never have been called.
Using Empty
as the parameter to Prim
indicates that there are no additional cases beyond Prim.plus
, Prim.minus
, and Prim.times
, because it is impossible to come up with a value of type Empty
to place in the Prim.other
constructor.
Because a function to apply an operator of type Empty
to two integers can never be called, it doesn't need to return a result.
Thus, it can be used in any monad:
def applyEmpty [Monad m] (op : Empty) (_ : Int) (_ : Int) : m Int :=
nomatch op
This can be used together with Id
, the identity monad, to evaluate expressions that have no effects whatsoever:
open Expr Prim in
#eval evaluateM (m := Id) applyEmpty (prim plus (const 5) (const (14)))
9
Nondeterministic Search
Instead of simply failing when encountering division by zero, it would also be sensible to backtrack and try a different input.
Given the right monad, the very same evaluateM
can perform a nondeterministic search for a set of answers that do not result in failure.
This requires, in addition to division, some means of specifying a choice of results.
One way to do this is to add a function choose
to the language of expressions that instructs the evaluator to pick either of its arguments while searching for nonfailing results.
The result of the evaluator is now a multiset of values, rather than a single value. The rules for evaluation into a multiset are:
 Constants \( n \) evaluate to singleton sets \( {n} \).
 Arithmetic operators other than division are called on each pair from the Cartesian product of the operators, so \( X + Y \) evaluates to \( \{ x + y \mid x ∈ X, y ∈ Y \} \).
 Division \( X / Y \) evaluates to \( \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\} \). In other words, all \( 0 \) values in \( Y \) are thrown out.
 A choice \( \mathrm{choose}(x, y) \) evaluates to \( \{ x, y \} \).
For example, \( 1 + \mathrm{choose}(2, 5) \) evaluates to \( \{ 3, 6 \} \), \(1 + 2 / 0 \) evaluates to \( \{\} \), and \( 90 / (\mathrm{choose}(5, 5) + 5) \) evaluates to \( \{ 9 \} \). Using multisets instead of true sets simplifies the code by removing the need to check for uniqueness of elements.
A monad that represents this nondeterministic effect must be able to represent a situation in which there are no answers, and a situation in which there is at least one answer together with any remaining answers:
inductive Many (α : Type) where
 none : Many α
 more : α → (Unit → Many α) → Many α
This datatype looks very much like List
.
The difference is that where cons
stores the rest of the list, more
stores a function that should compute the next value on demand.
This means that a consumer of Many
can stop the search when some number of results have been found.
A single result is represented by a more
constructor that returns no further results:
def Many.one (x : α) : Many α := Many.more x (fun ⟨⟩ => Many.none)
The union of two multisets of results can be computed by checking whether the first multiset is empty. If so, the second multiset is the union. If not, the union consists of the first element of the first multiset followed by the union of the rest of the first multiset with the second multiset:
def Many.union : Many α → Many α → Many α
 Many.none, ys => ys
 Many.more x xs, ys => Many.more x (fun ⟨⟩ => union (xs ⟨⟩) ys)
It can be convenient to start a search process with a list of values.
Many.fromList
converts a list into a multiset of results:
def Many.fromList : List α → Many α
 [] => Many.none
 x :: xs => Many.more x (fun ⟨⟩ => fromList xs)
Similarly, once a search has been specified, it can be convenient to extract either a number of values, or all the values:
def Many.take : Nat → Many α → List α
 0, _ => []
 _ + 1, Many.none => []
 n + 1, Many.more x xs => x :: (xs ⟨⟩).take n
def Many.takeAll : Many α → List α
 Many.none => []
 Many.more x xs => x :: (xs ⟨⟩).takeAll
A Monad Many
instance requires a bind
operator.
In a nondeterministic search, sequencing two operations consists of taking all possibilities from the first step and running the rest of the program on each of them, taking the union of the results.
In other words, if the first step returns three possible answers, the second step needs to be tried for all three.
Because the second step can return any number of answers for each input, taking their union represents the entire search space.
def Many.bind : Many α → (α → Many β) → Many β
 Many.none, _ =>
Many.none
 Many.more x xs, f =>
(f x).union (bind (xs ⟨⟩) f)
Many.one
and Many.bind
obey the monad contract.
To check that Many.bind (Many.one v) f
is the same as f v
, start by evaluating the expression as far as possible:
Many.bind (Many.one v) f
===>
Many.bind (Many.more v (fun ⟨⟩ => Many.none)) f
===>
(f v).union (Many.bind Many.none f)
===>
(f v).union Many.none
The empty multiset is a right identity of union
, so the answer is equivalent to f v
.
To check that Many.bind v Many.one
is the same as v
, consider that bind
takes the union of applying Many.one
to each element of v
.
In other words, if v
has the form {v1, v2, v3, ..., vn}
, then Many.bind v Many.one
is {v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn}
, which is {v1, v2, v3, ..., vn}
.
Finally, to check that Many.bind
is associative, check that Many.bind (Many.bind bind v f) g
is the same as Many.bind v (fun x => Many.bind (f x) g)
.
If v
has the form {v1, v2, v3, ..., vn}
, then:
Many.bind v f
===>
f v1 ∪ f v2 ∪ f v3 ∪ ... ∪ f vn
which means that
Many.bind (Many.bind bind v f) g
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g
Similarly,
Many.bind v (fun x => Many.bind (f x) g)
===>
(fun x => Many.bind (f x) g) v1 ∪
(fun x => Many.bind (f x) g) v2 ∪
(fun x => Many.bind (f x) g) v3 ∪
... ∪
(fun x => Many.bind (f x) g) vn
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g
Thus, both sides are equal, so Many.bind
is associative.
The resulting monad instance is:
instance : Monad Many where
pure := Many.one
bind := Many.bind
An example search using this monad finds all the combinations of numbers in a list that add to 15:
def addsTo (goal : Nat) : List Nat → Many (List Nat)
 [] =>
if goal == 0 then
pure []
else
Many.none
 x :: xs =>
if x > goal then
addsTo goal xs
else
(addsTo goal xs).union
(addsTo (goal  x) xs >>= fun answer =>
pure (x :: answer))
The search process is recursive over the list.
The empty list is a successful search when the goal is 0
; otherwise, it fails.
When the list is nonempty, there are two possibilities: either the head of the list is greater than the goal, in which case it cannot participate in any successful searches, or it is not, in which case it can.
If the head of the list is not a candidate, then the search proceeds to the tail of the list.
If the head is a candidate, then there are two possibilities to be combined with Many.union
: either the solutions found contain the head, or they do not.
The solutions that do not contain the head are found with a recursive call on the tail, while the solutions that do contain it result from subtracting the head from the goal, and then attaching the head to the solutions that result from the recursive call.
Returning to the arithmetic evaluator that produces multisets of results, the both
and neither
operators can be written as follows:
inductive NeedsSearch
 div
 choose
def applySearch : NeedsSearch → Int → Int → Many Int
 NeedsSearch.choose, x, y =>
Many.fromList [x, y]
 NeedsSearch.div, x, y =>
if y == 0 then
Many.none
else Many.one (x / y)
Using these operators, the earlier examples can be evaluated:
open Expr Prim NeedsSearch
#eval (evaluateM applySearch (prim plus (const 1) (prim (other choose) (const 2) (const 5)))).takeAll
[3, 6]
#eval (evaluateM applySearch (prim plus (const 1) (prim (other div) (const 2) (const 0)))).takeAll
[]
#eval (evaluateM applySearch (prim (other div) (const 90) (prim plus (prim (other choose) (const (5)) (const 5)) (const 5)))).takeAll
[9]
Custom Environments
The evaluator can be made userextensible by allowing strings to be used as operators, and then providing a mapping from strings to a function that implements them. For example, users could extend the evaluator with a remainder operator or with one that returns the maximum of its two arguments. The mapping from function names to function implementations is called an environment.
The environments needs to be passed in each recursive call.
Initially, it might seem that evaluateM
needs an extra argument to hold the environment, and that this argument should be passed to each recursive invocation.
However, passing an argument like this is another form of monad, so an appropriate Monad
instance allows the evaluator to be used unchanged.
Using functions as a monad is typically called a reader monad. When evaluating expressions in the reader monad, the following rules are used:
 Constants \( n \) evaluate to constant functions \( λ e . n \),
 Arithmetic operators evaluate to functions that pass their arguments on, so \( f + g \) evaluates to \( λ e . f(e) + g(e) \), and
 Custom operators evaluate to the result of applying the custom operator to the arguments, so \( f \ \mathrm{OP}\ g \) evaluates to \[ λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} \] with \( 0 \) serving as a fallback in case an unknown operator is applied.
To define the reader monad in Lean, the first step is to define the Reader
type and the effect that allows users to get ahold of the environment:
def Reader (ρ : Type) (α : Type) : Type := ρ → α
def read : Reader ρ ρ := fun env => env
By convention, the Greek letter ρ
, which is pronounced "rho", is used for environments.
The fact that constants in arithmetic expressions evaluate to constant functions suggests that the appropriate definition of pure
for Reader
is a a constant function:
def Reader.pure (x : α) : Reader ρ α := fun _ => x
On the other hand, bind
is a bit tricker.
Its type is Reader ρ α → (α → Reader ρ β) → Reader ρ β
.
This type can be easier to understand by expanding the definitions of Reader
, which yields (ρ → α) → (α → ρ → β) → ρ → β
.
It should take an environmentaccepting function as its first argument, while the second argument should transform the result of the environmentaccepting function into yet another environmentaccepting function.
The result of combining these is itself a function, waiting for an environment.
It's possible to use Lean interactively to get help writing this function. The first step is to write down the arguments and return type, being very explicit in order to get as much help as possible, with an underscore for the definition's body:
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
_
Lean provides a message that describes which variables are available in scope, and the type that's expected for the result.
The ⊢
symbol, called a turnstile due to its resemblance to subway entrances, separates the local variables from the desired type, which is ρ → β
in this message:
don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
⊢ ρ → β
Because the return type is a function, a good first step is to wrap a fun
around the underscore:
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => _
The resulting message now shows the function's argument as a local variable:
don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ β
The only thing in the context that can produce a β
is next
, and it will require two arguments to do so.
Each argument can itself be an underscore:
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next _ _
The two underscores have the following respective messages associated with them:
don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ α
don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ
Attacking the first underscore, only one thing in the context can produce an α
, namely result
:
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result _) _
Now, both underscores have the same error:
don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ
Happily, both underscores can be replaced by env
, yielding:
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result env) env
The final version can be obtained by undoing the expansion of Reader
and cleaning up the explicit details:
def Reader.bind (result : Reader ρ α) (next : α → Reader ρ β) : Reader ρ β :=
fun env => next (result env) env
It's not always possible to write correct functions by simply "following the types", and it carries the risk of not understanding the resulting program.
However, it can also be easier to understand a program that has been written than one that has not, and the process of filling in the underscores can bring insights.
In this case, Reader.bind
works just like bind
for Id
, except it accepts an additional argument that it then passes down to its arguments, and this intuition can help in understanding how it works.
Reader.pure
, which generates constant functions, and Reader.bind
obey the monad contract.
To check that Reader.bind (Reader.pure v) f
is the same as f v
, it's enough to replace definitions until the last step:
Reader.bind (Reader.pure v) f
===>
fun env => f ((Reader.pure v) env) env
===>
fun env => f ((fun _ => v) env) env
===>
fun env => f v env
===>
f v
For every function f
, fun x => f x
is the same as f
, so the first part of the contract is satisfied.
To check that Reader.bind r Reader.pure
is the same as r
, a similar technique works:
Reader.bind r Reader.pure
===>
fun env => Reader.pure (r env) env
===>
fun env => (fun _ => (r env)) env
===>
fun env => r env
Because reader actions r
are themselves functions, this is the same as r
.
To check associativity, the same thing can be done for both Reader.bind (Reader.bind r f) g
and Reader.bind r (fun x => Reader.bind (f x) g)
:
Reader.bind (Reader.bind r f) g
===>
fun env => g ((Reader.bind r f) env) env
===>
fun env => g ((fun env' => f (r env') env') env) env
===>
fun env => g (f (r env) env) env
Reader.bind r (fun x => Reader.bind (f x) g)
===>
Reader.bind r (fun x => fun env => g (f x env) env)
===>
fun env => (fun x => fun env' => g (f x env') env') (r env) env
===>
fun env => (fun env' => g (f (r env) env') env') env
===>
fun env => g (f (r env) env) env
Thus, a Monad (Reader ρ)
instance is justified:
instance : Monad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
The custom environments that will be passed to the expression evaluator can be represented as lists of pairs:
abbrev Env : Type := List (String × (Int → Int → Int))
For instance, exampleEnv
contains maximum and modulus functions:
def exampleEnv : Env := [("max", max), ("mod", (· % ·))]
Lean already has a function List.lookup
that finds the value associated with a key in a list of pairs, so applyPrimReader
needs only check whether the custom function is present in the environment. It returns 0
if the function is unknown:
def applyPrimReader (op : String) (x : Int) (y : Int) : Reader Env Int :=
read >>= fun env =>
match env.lookup op with
 none => pure 0
 some f => pure (f x y)
Using evaluateM
with applyPrimReader
and an expression results in a function that expects an environment.
Luckily, exampleEnv
is available:
open Expr Prim in
#eval evaluateM applyPrimReader (prim (other "max") (prim plus (const 5) (const 4)) (prim times (const 3) (const 2))) exampleEnv
9
Like Many
, Reader
is an example of an effect that is difficult to encode in most languages, but type classes and monads make it just as convenient as any other effect.
The dynamic or special variables found in Common Lisp, Clojure, and Emacs Lisp can be used like Reader
.
Similarly, Scheme and Racket's parameter objects are an effect that exactly correspond to Reader
.
The Kotlin idiom of context objects can solve a similar problem, but they are fundamentally a means of passing function arguments automatically, so this idiom is more like the encoding as a reader monad than it is an effect in the language.
Exercises
Checking Contracts
Check the monad contract for State σ
and Except ε
.
Readers with Failure
Adapt the reader monad example so that it can also indicate failure when the custom operator is not defined, rather than just returning zero. In other words, given these definitions:
def ReaderOption (ρ : Type) (α : Type) : Type := ρ → Option α
def ReaderExcept (ε : Type) (ρ : Type) (α : Type) : Type := ρ → Except ε α
do the following:
 Write suitable
pure
andbind
functions  Check that these functions satisfy the
Monad
contract  Write
Monad
instances forReaderOption
andReaderExcept
 Define suitable
applyPrim
operators and test them withevaluateM
on some example expressions
A Tracing Evaluator
The WithLog
type can be used with the evaluator to add optional tracing of some operations.
In particular, the type ToTrace
can serve as a signal to trace a given operator:
inductive ToTrace (α : Type) : Type where
 trace : α → ToTrace α
For the tracing evaluator, expressions should have type Expr (Prim (ToTrace (Prim Empty)))
.
This says that the operators in the expression consist of addition, subtraction, and multiplication, augmented with traced versions of each. The innermost argument is Empty
to signal that there are no further special operators inside of trace
, only the three basic ones.
Do the following:
 Implement a
Monad (WithLog logged)
instance  Write an
applyTraced
function to apply traced operators to their arguments, logging both the operator and the arguments, with typeToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int
If the exercise has been completed correctly, then
open Expr Prim ToTrace in
#eval evaluateM applyTraced (prim (other (trace times)) (prim (other (trace plus)) (const 1) (const 2)) (prim (other (trace minus)) (const 3) (const 4)))
should result in
{ log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, 1)], val := 3 }
Hint: values of type Prim Empty
will appear in the resulting log. In order to display them as a result of #eval
, the following instances are required:
deriving instance Repr for WithLog
deriving instance Repr for Empty
deriving instance Repr for Prim
do
Notation for Monads
While APIs based on monads are very powerful, the explicit use of >>=
with anonymous functions is still somewhat noisy.
Just as infix operators are used instead of explicit calls to HAdd.hAdd
, Lean provides a syntax for monads called do
notation that can make programs that use monads easier to read and write.
This is the very same do
notation that is used to write programs in IO
, and IO
is also a monad.
In Hello, World!, the do
syntax is used to combine IO
actions, but the meaning of these programs is explained directly.
Understanding how to program with monads means that do
can now be explained in terms of how it translates into uses of the underlying monad operators.
The first translation of do
is used when the only statement in the do
is a single expression E
.
In this case, the do
is removed, so
do E
translates to
E
The second translation is used when the first statement of the do
is a let
with an arrow, binding a local variable.
This translates to a use of >>=
together with a function that binds that very same variable, so
do let x ← E1
Stmt
...
En
translates to
E1 >>= fun x =>
do Stmt
...
En
When the first statement of the do
block is an expression, then it is considered to be a monadic action that returns Unit
, so the function matches the Unit
constructor and
do E1
Stmt
...
En
translates to
E1 >>= fun ⟨⟩ =>
do Stmt
...
En
Finally, when the first statement of the do
block is a let
that uses :=
, the translated form is an ordinary let expression, so
do let x := E1
Stmt
...
En
translates to
let x := E1
do Stmt
...
En
The definition of firstThirdFifthSeventh
that uses the Monad
class looks like this:
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
lookup xs 0 >>= fun first =>
lookup xs 2 >>= fun third =>
lookup xs 4 >>= fun fifth =>
lookup xs 6 >>= fun seventh =>
pure (first, third, fifth, seventh)
Using do
notation, it becomes significantly more readable:
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) := do
let first ← lookup xs 0
let third ← lookup xs 2
let fifth ← lookup xs 4
let seventh ← lookup xs 6
pure (first, third, fifth, seventh)
Without the Monad
type class, the function number
that numbers the nodes of a tree was written:
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
 BinTree.leaf => ok BinTree.leaf
 BinTree.branch left x right =>
helper left ~~> fun numberedLeft =>
get ~~> fun n =>
set (n + 1) ~~> fun ⟨⟩ =>
helper right ~~> fun numberedRight =>
ok (BinTree.branch numberedLeft (n, x) numberedRight)
(helper t 0).snd
With Monad
and do
, its definition is much less noisy:
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
 BinTree.leaf => pure BinTree.leaf
 BinTree.branch left x right => do
let numberedLeft ← helper left
let n ← get
set (n + 1)
let numberedRight ← helper right
ok (BinTree.branch numberedLeft (n, x) numberedRight)
(helper t 0).snd
All of the conveniences from do
with IO
are also available when using it with other monads.
For example, nested actions also work in any monad.
The original definition of mapM
was:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
 [] => pure []
 x :: xs =>
f x >>= fun hd =>
mapM f xs >>= fun tl =>
pure (hd :: tl)
With do
notation, it can be written:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
 [] => pure []
 x :: xs => do
let hd ← f x
let tl ← mapM f xs
pure (hd :: tl)
Using nested actions makes it almost as short as the original nonmonadic map
:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
 [] => pure []
 x :: xs => do
pure ((← f x) :: (← mapM f xs))
Using nested actions, number
can be made much more concise:
def increment : State Nat Nat := do
let n ← get
set (n + 1)
pure n
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
 BinTree.leaf => pure BinTree.leaf
 BinTree.branch left x right => do
pure (BinTree.branch (← helper left) ((← increment), x) (← helper right))
(helper t 0).snd
Exercises
 Rewrite
evaluateM
, its helpers, and the different specific use cases usingdo
notation instead of explicit calls to>>=
.  Rewrite
firstThirdFifthSeventh
using nested actions.
The IO Monad
IO
as a monad can be understood from two perspectives, which were described in the section on running programs.
Each can help to understand the meanings of pure
and bind
for IO
.
From the first perspective, an IO
action is an instruction to Lean's runtime system.
For example, the instruction might be "read a string from this file descriptor, then reinvoke the pure Lean code with the string".
This perspective is an exterior one, viewing the program from the perspective of the operating system.
In this case, pure
is an IO
action that does not request any effects from the RTS, and bind
instructs the RTS to first carry out one potentiallyeffectful operation and then invoke the rest of the program with the resulting value.
From the second perspective, an IO
action transforms the whole world.
IO
actions are actually pure, because they receive a unique world as an argument and then return the changed world.
This perspective is an interior one that matches how IO
is represented inside of Lean.
The world is represented in Lean as a token, and the IO
monad is structured to make sure that each token is used exactly once.
To see how this works, it can be helpful to peel back one definition at a time.
The #print
command reveals the internals of Lean datatypes and definitions.
For example,
#print Nat
results in
inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat
and
#print Char.isAlpha
results in
def Char.isAlpha : Char → Bool :=
fun c => Char.isUpper c  Char.isLower c
Sometimes, the output of #print
includes Lean features that have not yet been presented in this book.
For example,
#print List.isEmpty
produces
def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
fun {α} x =>
match x with
 [] => true
 head :: tail => false
which includes a .{u}
after the definition's name, and annotates types as Type u
rather than just Type
.
This can be safely ignored for now.
Printing the definition of IO
shows that it's defined in terms of simpler structures:
#print IO
@[reducible] def IO : Type → Type :=
EIO IO.Error
IO.Error
represents all the errors that could be thrown by an IO
action:
#print IO.Error
inductive IO.Error : Type
number of parameters: 0
constructors:
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
IO.Error.otherError : UInt32 → String → IO.Error
IO.Error.resourceBusy : UInt32 → String → IO.Error
IO.Error.resourceVanished : UInt32 → String → IO.Error
IO.Error.unsupportedOperation : UInt32 → String → IO.Error
IO.Error.hardwareFault : UInt32 → String → IO.Error
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
IO.Error.illegalOperation : UInt32 → String → IO.Error
IO.Error.protocolError : UInt32 → String → IO.Error
IO.Error.timeExpired : UInt32 → String → IO.Error
IO.Error.interrupted : String → UInt32 → String → IO.Error
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
IO.Error.unexpectedEof : IO.Error
IO.Error.userError : String → IO.Error
EIO ε α
represents IO
actions that will either terminate with an error of type ε
or succeed with a value of type α
.
This means that, like the Except ε
monad, the IO
monad includes the ability to define error handling and exceptions.
Peeling back another layer, EIO
is itself defined in terms of a simpler structure:
#print EIO
def EIO : Type → Type → Type :=
fun ε => EStateM ε IO.RealWorld
The EStateM
monad includes both errors and state—it's a combination of Except
and State
.
It is defined using another type, EStateM.Result
:
#print EStateM
def EStateM.{u} : Type u → Type u → Type u → Type u :=
fun ε σ α => σ → EStateM.Result ε σ α
In other words, a program with type EStateM ε σ α
is a function that accepts an initial state of type σ
and returns an EStateM.Result ε σ α
.
EStateM.Result
is very much like the definition of Except
, with one constructor that indicates a successful termination and one constructor that indicates an error:
#print EStateM.Result
inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u
number of parameters: 3
constructors:
EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α
EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α
Just like Except ε α
, the ok
constructor includes a result of type α
, and the error
constructor includes an exception of type ε
.
Unlike Except
, both constructors have an additional state field that includes the final state of the computation.
The Monad
instance for EStateM ε σ
requires pure
and bind
.
Just as with State
, the implementation of pure
for EStateM
accepts an initial state and returns it unchanged, and just as with Except
, it returns its argument in the ok
constructor:
#print EStateM.pure
protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α :=
fun {ε σ α} a s => EStateM.Result.ok a s
protected
means that the full name EStateM.pure
is needed even if the EStateM
namespace has been opened.
Similarly, bind
for EStateM
takes an initial state as an argument.
It passes this initial state to its first action.
Like bind
for Except
, it then checks whether the result is an error.
If so, the error is returned unchanged and the second argument to bind
remains unused.
If the result was a success, then the second argument is applied to both the returned value and to the resulting state.
#print EStateM.bind
protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β :=
fun {ε σ α β} x f s =>
match x s with
 EStateM.Result.ok a s => f a s
 EStateM.Result.error e s => EStateM.Result.error e s
Putting all of this together, IO
is a monad that tracks state and errors at the same time.
The collection of available errors is that given by the datatype IO.Error
, which has constructors that describe many things that can go wrong in a program.
The state is a type that represents the real world, called IO.RealWorld
.
Each basic IO
action receives this real world and returns another one, paired either with an error or a result.
In IO
, pure
returns the world unchanged, while bind
passes the modified world from one action into the next action.
Because the entire universe doesn't fit in a computer's memory, the world being passed around is just a representation. So long as world tokens are not reused, the representation is safe. This means that world tokens do not need to contain any data at all:
#print IO.RealWorld
def IO.RealWorld : Type :=
Unit
Additional Conveniences
Shared Argument Types
When defining a function that takes multiple arguments that have the same type, both can be written before the same colon. For example,
def equal? [BEq α] (x : α) (y : α) : Option α :=
if x == y then
some x
else
none
can be written
def equal? [BEq α] (x y : α) : Option α :=
if x == y then
some x
else
none
This is especially useful when the type signature is large.
Constructor Dot Notation
The constructors of an inductive type are in a namespace. This allows multiple related inductive types to use the same constructor names, but it can lead to programs becoming verbose. In contexts where the inductive type in question is known, the namespace can be omitted by preceding the constructor's name with a dot, and Lean uses the expected type to resolve the constructor names. For example, a function that mirrors a binary tree can be written:
def BinTree.mirror : BinTree α → BinTree α
 BinTree.leaf => BinTree.leaf
 BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)
Omitting the namespaces makes it significantly shorter, at the cost of making the program harder to read in contexts like code review tools that don't include the Lean compiler:
def BinTree.mirror : BinTree α → BinTree α
 .leaf => .leaf
 .branch l x r => .branch (mirror r) x (mirror l)
Summary
Encoding Side Effects
Lean is a pure functional language. This means that it does not include side effects such as mutable variables, logging, or exceptions. However, most side effects can be encoded using a combination of functions and inductive types or structures. For example, mutable state can be encoded as a function from an initial state to a pair of a final state and a result, and exceptions can be encoded as an inductive type with constructors for successful termination and errors.
Each set of encoded effects is a type. As a result, if a program uses these encoded effects, then this is apparent in its type. Functional programming does not mean that programs can't use effects, it simply requires that they be honest about which effects they use. A Lean type signature describes not only the types of arguments that a function expects and the type of result that it returns, but also which effects it may use.
The Monad Type Class
It's possible to write purely functional programs in languages that allow effects anywhere.
For example, 2 + 3
is a valid Python program that has no effects at all.
Similarly, combining programs that have effects requires a way to state the order in which the effects must occur.
It matters whether an exception is thrown before or after modifying a variable, after all.
The type class Monad
captures these two important properties.
It has two methods: pure
represents programs that have no effects, and bind
sequences effectful programs.
The contract for Monad
instances ensures that bind
and pure
actually capture pure computation and sequencing.
do
Notation for Monads
Rather than being limited to IO
, do
notation works for any monad.
It allows programs that use monads to be written in a style that is reminiscent of statementoriented languages, with statements sequenced after one another.
Additionally, do
notation enables a number of additional convenient shorthands, such as nested actions.
A program written with do
is translated to applications of >>=
behind the scenes.
Custom Monads
Different languages provide different sets of side effects. While most languages feature mutable variables and file I/O, not all have features like exceptions. Other languages offer effects that are rare or unique, like Icon's searchbased program execution, Scheme and Ruby's continuations, and Common Lisp's resumable exceptions. An advantage to encoding effects with monads is that programs are not limited to the set of effects that are provided by the language. Because Lean is designed to make programming with any monad convenient, programmers are free to choose exactly the set of side effects that make sense for any given application.
The IO
Monad
Programs that can affect the real world are written as IO
actions in Lean.
IO
is one monad among many.
The IO
monad encodes state and exceptions, with the state being used to keep track of the state of the world and the exceptions modeling failure and recovery.