Functional Programming in Lean

by David Thrane Christiansen

This is an in-progress 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 nightly-2022-11-26.

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 general-purpose 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 first-class 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 first-class 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 to rustup or ghcup.
  • lake builds Lean packages and their dependencies, similarly to cargo, 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 up-to-date 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 C-c C-k 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 read-eval-print-loop (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 catch-all 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 order-of-operations 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 expression-oriented 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:

  1. They allow the compiler to make decisions about the in-memory representation of a value.

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

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

  4. 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 full-blown logic for proving mathematical theorems. This cutting-edge 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 arbitrary-precision unsigned integers. In Lean, Nat is the default type for non-negative 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 arbitrarily-large 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 colon-equal 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 zero-argument 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 Nats 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 multiple-argument 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 multiple-argument 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 type String -> 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 type Nat → 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 first-class 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 right-hand side of the definition, causing Nat's overloading rules to be used for 38:

def thirtyEight : NaturalNumber := (38 : Nat)

The definition is still type-correct 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 structs in C or Rust and records 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 floating-point numbers. Defining separate structures prevents API clients from confusing one for another.

Lean's floating-point number type is called Float, and floating-point 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 three-dimensional 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 curly-brace 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 copy-paste 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 newly-allocated data structure. It is not possible to provide a custom constructor that pre-processes 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 curly-brace 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 Floats (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 curly-braced 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 a Float.
  • 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 function length : 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 and Book? 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 user-defined types are inductive datatypes. When programming, inductive datatypes are consumed through pattern matching and recursive functions.

Many of the built-in 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 re-exported 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 non-abstract class creates both a new type and new ways of allocating data. In the object-oriented 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 non-negative 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 instance-of operator to check which subclass has been received and then reading the values of the fields that are available in the given subclass. The instance-of 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.

Step-by-step, 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. Non-recursive 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

well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) 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 well-founded 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 object-oriented 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 Floats. 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 Nats. 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 pattern-matching against a datatype. When Lean is checking this function, it uses the fact that the function's body pattern-matches 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 Lists can be defined in much the same way as functions that consume Nats. 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 pattern-match 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 Built-In 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 non-null and null versions of the underlying type. The non-null 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 non-nullable 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 built-in 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 right-associative. 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 domain-specific 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, zero-argument 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 special-purpose 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 honest-to-goodness 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 with def Prod.swap {α β : Type} (pair : α × β) : β × α :=
  • Rewrite the PetName example to use a custom datatype and compare it to the version that uses Sum.
  • 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 with def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=.
  • Write a polymorphic function take that returns the first n entries in a list, where n is a Nat. If the list contains fewer than n 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.

Pattern-Matching Definitions

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

The first step is to move the arguments' types to the right of the 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 re-used.

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

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

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

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

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

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

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

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

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

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

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

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

Type Inference

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

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

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

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

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

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

#check 14
14 : Nat
#check (14 : Int)
14 : Int

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

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

leads to a message about the match expression:

invalid match-expression, pattern contains metavariables
  []

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

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

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

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

def id (x : α) := x

Omitting the argument type, however, causes an error:

def id x := x
failed to infer binder type

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

Simultaneous Matching

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

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

Natural Number Patterns

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

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

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

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

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

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

can be replaced by numeric literals and +:

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

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

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

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | 2 + n => halve n + 1
invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 2 n)

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

Anonymous Functions

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

#check fun x => x + 1
fun x => x + 1 : Nat → Nat

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

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

Similarly, implicit arguments may be written with curly braces:

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

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

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

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

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

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

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

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

if let

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

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

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

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

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

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

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

Positional Structure Arguments

The section on structures presents two ways of constructing structures:

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

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

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

invalid constructor ⟨...⟩, expected type must be an inductive type 
  ?m.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: sub-expressions 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 first-class 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:

  1. Anonymous functions are written using fun. For instance, a function that swaps the fields of a Point can be written fun (point : Point) => { x := point.y, y := point.x : Point}
  2. 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 as fun x => x - 1.
  3. Functions can be defined using def or let by adding an argument list or by using pattern-matching 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 object-oriented 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 structurally-smaller 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 non-terminating 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 batch-mode 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 command-line 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 sub-expressions 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 run-time 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 run-time system (RTS) work. Primitives in the run-time 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.

Real-World 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 re-use 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 sub-language 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 special-purpose language for interacting with databases, the do syntax can be thought of as a special-purpose sub-language 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 built-in 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 non-alphanumeric 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 first-class 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 double-check that your predictions about the side effects were correct.

Starting a Project

As a program written in Lean becomes more serious, an ahead-of-time compiler-based workflow that results in an executable becomes more attractive. Like other languages, Lean has tools for building multiple-file 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 special-purpose language for writing programs with effects (the do language), Lake contains a special-purpose language for configuring builds. These languages are referred to as embedded domain-specific languages (or sometimes domain-specific embedded languages, abbreviated EDSL or DSEL). They are domain-specific in the sense that they are used for a particular purpose, with concepts from some sub-domain, and they are typically not suitable for general-purpose 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 the main action.
  • Greeting.lean is the scaffolding of a support library for the program.
  • lakefile.lean contains the configuration that lake needs to build the application.
  • lean-toolchain 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 already-existing 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 command-line 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 non-zero exit code is returned if any of the input files do not exist.

This section describes a simplified version of cat, called feline. Unlike commonly-used versions of cat, feline has no command-line options for features such as numbering lines, indicating non-printing 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 copy-paste 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 command-line 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 tail-recursive function, called process. In order to return a non-zero 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 single-field 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 non-termination 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 command-line arguments and always indicate success with an exit code of 0,
  • main : IO UInt32 corresponds to int main(void) in C, for programs without arguments that return exit codes, and
  • main : List String → IO UInt32 corresponds to int 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 command-line argument --help that causes documentation about the available command-line 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 whitespace-sensitive. 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 whitespace-sensitive 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 re-executed 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 run-time 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 command-line arguments and always return exit code 0,
  • main : IO UInt32 is used for programs without arguments that may signal success or failure, and
  • main : List String → IO UInt32 is used for programs that take command-line 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 built-in domain-specific 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 multiple-file 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 domain-specific 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 potentially-infinite 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 first-class 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 compile-time error, rather than a run-time 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. Out-of-bounds 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. Computer-aided 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:

  1. Many proofs are complicated and tedious when written out down to the smallest detail, and tactics can automate these uninteresting parts.
  2. Proofs written with tactics are easier to maintain over time, because flexible automation can paper over small changes to definitions.
  3. 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
ConnectiveLean SyntaxEvidence
TrueTrueTrue.intro : True
FalseFalseNo evidence
A and BA ∧ BAnd.intro : A → B → A ∧ B
A or BA ∨ BEither Or.inl : A → A ∨ B or Or.inr : B → A ∨ B
A implies BA → BA function that transforms evidence of A into evidence of B
not A¬AA 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 hand-holding.

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 compile-time 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 built-in datatypes get special treatment. For example, in C and Java, + can be used to add floats and ints, but not arbitrary-precision numbers from a third-party library. Similarly, numeric literals can be used directly for the built-in types, but not for user-defined 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 built-in 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 object-oriented languages, because they are not closely related to classes and instances in object-oriented 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 object-oriented 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 object-oriented 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 object-oriented programming.

Positive Numbers

In some applications, only positive numbers make sense. For example, compilers and interpreters typically use one-indexed line and column numbers for source positions, and a datatype that represents only non-empty 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 object-oriented languages. In object-oriented 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 Nats 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 floating-point 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 built-in 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 built-in 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 trade-off 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 first-class 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 non-type arguments in positions where a less-flexible 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, out-of-bounds 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 at-sign (@) 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 Nats:

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 built-in 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 dynamically-sized 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 compile-time 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

Non-Empty Lists

A datatype that represents non-empty 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 non-empty 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:

  1. The index is 0, in which case the head of the list should be returned.
  2. The index is n + 1 and the tail is empty, in which case the index is out of bounds.
  3. The index is n + 1 and the tail is non-empty, in which case the function can be called recursively on the tail and n.

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 non-empty 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 compile-time 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 non-numeric 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:

ExpressionDesugaringClass Name
x + yHAdd.hAdd x yHAdd
x - yHSub.hSub x yHSub
x * yHMul.hMul x yHMul
x / yHDiv.hDiv x yHDiv
x % yHMod.hMod x yHMod
x ^ yHPow.hPow x yHPow
(- x)Neg.neg xNeg

Bitwise Operators

Lean contains a number of standard bitwise operators that are overloaded using type classes. There are instances for fixed-width 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:

ExpressionDesugaringClass Name
x &&& yHAnd.hAnd x yHAnd
x ||| y HOr.hOr x yHOr
x ^^^ yHXor.hXor x yHXor
~~~ xComplement.complement xComplement
x >>> yHShiftRight.hShiftRight x yHShiftRight
x <<< yHShiftLeft.hShiftLeft x yHShiftLeft

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 two-line 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:

ExpressionDesugaringClass Name
x < yLT.lt x yLT
x ≤ yLE.le x yLE
x > yLT.lt y xLT
x ≥ yLE.le y xLE

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 built-in 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 well-behaved 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 := ["Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider",
         "Banded Garden Spider",
         "Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider"] }

Similarly, a definition of HAppend allows non-empty 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 := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced 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 to some "[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 to some "[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 non-empty 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:

  1. Mapping the identity function should result in the original argument.
  2. 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 non-nullable 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.

Non-Empty 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 non-empty lists to ordinary lists makes sense because the List type can represent every non-empty list:

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

This allows non-empty 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 non-empty 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 non-function 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 first-class 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 Adders 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 comma-separated 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 non-empty 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 curly-brace 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, multi-step 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 non-empty 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 compile-time 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 object-oriented 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 potentially-null value. If the reciever is null, the whole expression is null. Otherwise, the underlying non-null 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) non-associative, left-associative, and right-associative 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 non-associative, 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. Higher-precedence operators are applied before lower-precedence 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 built-in exception mechanism for error handling, because throwing or catching an exception is outside of the step-by-step 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 in-bounds 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 out-of-bounds 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 log-accumulating 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, or State σ
  • 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, and get, 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 :=
  ["Three-toed sloth", "Slow loris"]

def fastBirds : List String := [
  "Peregrine falcon",
  "Saker falcon",
  "Golden eagle",
  "Gray-headed albatross",
  "Spur-winged 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", "Spur-winged 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", "Spur-winged 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 type-level 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:

  1. 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.
  2. 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

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 non-failing 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 non-deterministic 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 non-empty, 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 user-extensible 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 environment-accepting function as its first argument, while the second argument should transform the result of the environment-accepting function into yet another environment-accepting 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:

  1. Write suitable pure and bind functions
  2. Check that these functions satisfy the Monad contract
  3. Write Monad instances for ReaderOption and ReaderExcept
  4. Define suitable applyPrim operators and test them with evaluateM 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:

  1. Implement a Monad (WithLog logged) instance
  2. Write an applyTraced function to apply traced operators to their arguments, logging both the operator and the arguments, with type ToTrace (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 non-monadic 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 using do-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 run-time system. For example, the instruction might be "read a string from this file descriptor, then re-invoke 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 potentially-effectful 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 re-used, 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 statement-oriented 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 search-based 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.