\chapter{Effectful Programming}
\label{chap:effectful-programming}

Pure functional programming can sometimes feel overly restrictive.
\emph{Effectful functional programming} provides idioms that alleviate some of
these restrictions, giving us the impression of programming with side effects,
exceptions, nondeterminism, and other effects.

The underlying abstraction is called \emph{monad}. Monads generalize programs
with effects. They are popular in Haskell to write imperative programs. In Lean,
they are used to express imperative programs and to reason about them. They are
even useful for programming Lean itself, as we will see in
Chapter~\ref{chap:metaprogramming}.

These notes are inspired by Chapter 7 of \emph{Programming in Lean}
\cite{programming-in-lean}. We also refer to Chapter~14 of \emph{Real World
Haskell} \cite{osullivan-et-al-2008} for a general introduction to effectful
functional programming.

\section{Introductory Example}
\label{sec:introductory-example}

Consider the following programming task:
%
\begin{quote}
Implement a function
\li{sum257 ns} that sums up the second, fifth, and seventh items of a list
\li{ns} of natural numbers. Use \li{Option ℕ} for the result so that you can
return \li{Option.none} if the list has too few items.
\end{quote}
%
A straightforward solution would be as follows:

\lstinputlisting[linerange=sum257-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
(Confusingly, \li{nth} counts elements from 0.)
The code is quite inelegant, because of all the pattern matching on
\li{Option}. Although the programming task is contrived, we can all recall
writing code with nested error handling and ever increasing indentation levels.

We can do better, by concentrating the ugliness in one function:

\lstinputlisting[linerange=connect-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The \li{connect} function works on an \li{Option}. If the value is
\li{Option.}\allowbreak\hbox{\li{none},} we leave it as is. This corresponds to an error
condition, and errors are ``sticky.'' Otherwise, the value is of the form
\hbox{\li{Option.}}\allowbreak\li{some a}, and we apply the operation \li{f} on \li{a}---or
\emph{bind} \li{f}'s argument to \li{a}. We can now use \li{connect} to
program our sum function:

\lstinputlisting[linerange=sum257_connect-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
Intuitively, the program performs the following steps:
%
\begin{itemize}
\item[1.] Extract the second item from the list using \li{nth}. If there is no
  such item, \li{nth} returns \li{Option.none}; simply return this value.
  Otherwise, bind \li{n2} to this item and continue with the next step.
\item[2.] Perform the same for the fifth and seventh item, mutatis mutandis.
\item[3.] Return the sum of \li{n2}, \li{n5}, and \li{n7} in an
  \li{Option.some} wrapper.
\end{itemize}
%
Mathematically, our new function \li{sum257Connect} is equal to the original
function \li{sum257}.

Instead of defining \li{connect} ourselves, we could have used Lean's
predefined general \li{bind} operation. It takes the same arguments in the same
order. Here is the new code:

\lstinputlisting[linerange=sum257_bind-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
We also use the predefined \li{pure} function instead of \li{Option.some} to
convert a pure \li{α} value to an \li{Option α}.

One of the advantages of using the predefined \li{bind} is that it provides
syntactic sugar, in the form of the \li{>>=} operator:

\lstinputlisting[linerange=sum257_op-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The syntax \li{oa >>= f} expands to \li{bind oa f}, where \li{oa} is of type
\li{Option α}.

The next-to-last version of the sum program uses heavier syntactic sugar:

\lstinputlisting[linerange=sum257_dos-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The \li{do} notation provides a convenient syntax for effectful programs. The
program \hbox{\li{do let a ← oa …}} is equivalent to \li{oa >>= (fun a ↦ …)}. If we are
not interested in the result of \li{oa}'s computation, we can omit the
\li{let a ←} binding and write \li{do oa …}, which expands to
\li{oa >>=} \li{(fun _ ↦ …)}.

The \li{do} notation conveniently allows multiple \li{let} bindings in a
single block. This brings us to the final version of the program:

\lstinputlisting[linerange=sum257_single_do-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
Each line with an arrow \li{←} attempts to read a value. In case of failure, the
entire program evaluates to \li{Option.none}.

The above function can be read as an imperative program where each of the
\li{nth} calls can throw an exception. But even though the notation has an
imperative flavor, the function is a pure functional program.

\section{Two Operations and Three Laws}
\label{sec:two-operations-and-three-laws}

The \li{Option} type constructor is an example of a monad, called the
\emph{option monad}. In general, a monad is a unary type constructor
\li{m : Type → Type} that depends on some type parameter \li{α} equipped with
two distinguished operations:
%
\begin{center}
\begin{tabular}{@{}r@{}c@{}l@{}}
\lic|pure {α : Type}| & ${}:{}$ & \lic|α → m α| \\
\lic|bind {α β : Type}| & ${}:{}$ & \lic|m α → (α → m β) → m β| \\
\end{tabular}
\end{center}
%
As usual, curly braces denote implicit arguments. For options, the \li{pure}
operation is simply \li{Option.some}, whereas \li{bind} amounts to our
\li{connect}.

A value of type \li{m α} is an effectful program. The \li{pure}
operation embeds a pure, effectless program of type \li{α} in \li{m α}. The
\li{bind} operation composes two effectful programs, of types \li{m α} and
\li{m β}. The first program's output, of type \li{α}, is passed to the second
program. The second program's output is also the output of the composite
program.

We can think of a monad as a box containing some data. The box captures some
special effect (e.g., exceptions, a mutable state). The \li{pure} operation
puts data into the box, whereas \li{bind} allows us to access the data in the
box and modify it---possibly even changing its type, since the result has type
\li{m β}, not \li{m α}. There is, however, no general way to extract the data
from the box---i.e., to obtain an \li{α} from an \li{m α}. There might not be
any \li{α} value in it, or there might be several.

To summarize, \li{pure a} is a box containing the value \li{a}, with
no effects, whereas \li{bind ma f} (also written \li{ma >>=} \li{f} or
\hbox{\li{do a ← ma,}} \hbox{\li{f a})} executes \li{ma}, then executes \li{f} with the
unboxed result \li{a} of \li{ma}. It is convenient to use names such as \li{ma}
or \li{mb} for boxed values of type \li{m α} or \li{m β}, and \li{a} or
\li{b} for data of type \li{α} or \li{β}.

Monads are an abstract concept with many applications. The option type is only
one instance among many. The following table gives an overview of some monad
instances and their effects.

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}l@{\quad}l@{}}
\toprule
Type & Effect \\
\midrule
\li|id|                 & no effects \\
\li|Option|             & simple exceptions \\
\li|fun α ↦ \σ → α × σ| & threading through a state of type \li|\σ| \\
\li|Set|                & nondeterministic computations returning \li|\α| values \\
\li|fun α ↦ t → α|      & reading elements of type \li|t| (e.g., a configuration) \\
\li|fun α ↦ \ℕ × α|     & adjoining running time (e.g., to model time complexity) \\
\li|fun α ↦ String × α| & adjoining text output (e.g., for logging) \\
\li|IO|                 & interaction with the operating system \\
\li|TacticM|            & interaction with the proof assistant \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

All of the above are unary type constructors \hbox{\li{m : Type → Type}.}
Some effects can be combined (e.g., \li{fun α ↦ Option (t → α)}). Some
effects are not executable (e.g., \hbox{\li{Set});} these are nonetheless useful for
modeling programs abstractly. Specific type constructors \li{m} may provide
further operators beyond \hbox{\li{pure}} and \li{bind}. For example, they may
provide a way to extract the boxed value.

Monads have several benefits. They provide the highly readable \li{do}
notation. They support generic operations, such as \li|List.|\hbox{\li|mmap {α β :|}
\hbox{\li|Type} : (α → m β) →|} \hbox{\li|List α → m (List β)|,} that work
uniformly for all monads~\li{m}. To quote \emph{Programming in Lean}
\cite{programming-in-lean}:
%
\begin{quote}
The power of the abstraction is not only that it provides general functions
and notation %the
that can be used in all these various instantiations, but also
that it provides a helpful way of thinking about what they all have in
common.
%
\end{quote}
%
Besides being a useful computer science concept, monads provide a nice example
of axiomatic reasoning.

\newcommand\BIGEQ{\qquad\smash{\lower.2ex\hbox{\Large\li|=|}}\qquad\hbox{}}
\newcommand\BIGEQlower{\qquad\smash{\lower1.2ex\hbox{\Large\li|=|}}\qquad\hbox{}}

The \li{bind} and \li{pure} operations are normally required to obey three
laws. The \li{bind} operation combines two programs. If either of these is a
pure program, we can inline it and eliminate the \li{bind}. This gives us the
first two laws:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}p{8.5em}@{}l@{}p{8.5em}@{}}
\lic|do| \\
\quad \lic|let a' ← pure a|\! & \BIGEQ & \lic|f a| \\
\quad \lic|f a'|
\end{tabular}}

\vskip\abovedisplayshortskip

\noindent
and

\vskip\abovedisplayshortskip

\centerline{\begin{tabular}{@{}p{8.5em}@{}l@{}p{8.5em}@{}}
\lic|do| \\
\quad \lic|let a ← ma| & \BIGEQ & \lic|ma| \\
\quad \lic|pure a|
\end{tabular}}

\vskip\belowdisplayskip

\noindent
The third law is an associativity rule for bind. It allows us to flatten a
nested computation:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}p{8.5em}@{}l@{}p{8.5em}@{}}
\lic|do|
  \\
\quad \lic|let b ←| &
  & \lic|do| \\
\qquad \lic|do| & \BIGEQlower
  & \quad \lic|let a ← ma| \\
\qquad\quad \lic|let a ← ma| &
  & \quad \lic|let b ← f a| \\
\qquad\quad \lic|f a| &
  & \quad \lic|g b| \\
\quad \lic|g b|
\end{tabular}}

\vskip\belowdisplayskip

Earlier we compared a monad to a box. It may help to think of the box more
concretely as a Swiss bank account, with \li{α := }money. The first law means
that if you put some money in the account, you can take it out. The second law
means that nobody will notice if you take out some money and put it back
afterwards. The third law means that performing two bank operations together
followed by a third one is the same as performing the first one alone followed
by the other two. Given the Swiss banks' reputation for secrecy, all three laws
seem plausible.

\section{A Type Class}
\label{sec:a-type-class}

Monads are a mathematical structure, so we use a type class to specify them in
Lean. Recall that a type class is a structure type that is parameterized,
typically by a type, but here by a type constructor \li{m : Type → Type}.
Whenever we use a field from the type class on a concrete~\li{m}, the type
class inference mechanism retrieves the relevant structure value---the type
class instance.

A possible Lean definition of monads, together with the three laws, follows:

\lstinputlisting[linerange=LawfulMonad-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}

Let us study this definition step by step:

\begin{itemize}
\item We are creating a structure parameterized by a unary type
  constructor~\li{m}---i.e., a value of type \li{Type → Type}.

\item The structure inherits the fields, and any syntactic sugar, from
  structures called \li{Pure} and \li{Bind}. These provide the
  \li{pure} and \li{bind} operations on \li{m}, with the expected types and
  the syntactic sugar.

\item Finally, three fields (\li{pure_bind}, \hbox{\li{bind_pure},}
  and \hbox{\li{bind_assoc})} are added to those already provided by
  \li{Pure} and \li{Bind}. Each field is a proof of one of the three laws.
\end{itemize}

We call our type class \li{LawfulMonad} because the three laws are required to
hold. To instantiate this definition, we must supply the type constructor
\li{m}, suitable \li{bind} and \li{pure} operators, and proofs of the laws.

Lean includes its own concept of monads, also called \li{Lawful}\-\hbox{\li{Monad}.} It
is roughly equivalent to our definition but is distributed over multiple type
classes.

\section{No Effects}
\label{sec:no-effects}

Lean's constant \li|id {α : Type} : α → α| is defined as the identity
function \li{fun x ↦} \li{x}. The identity type constructor is obtained by
taking \li{α := Type}. We can register it as a monad:

\lstinputlisting[linerange=id_monad-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The registration process requires us to provide five components:\
the \li{pure} and \li{bind} operations and the proofs of the three laws.

The \emph{identity monad} is the simplest monad possible. It provides a simple
box, with a single value in it, without any effect. It plays a similar role as
0 in additive arithmetic. We can think of the other monads as variations of it;
for example, the option monad is an identity monad enriched with a special
\li{Option.none} value representing an error state.

\section{Basic Exceptions}
\label{sec:basic-exceptions}

As we saw above, the option type provides a basic exception mechanism. The
following code shows how to register \hbox{\li{Option :}} \li{Type → Type} as a
lawful monad:
%
\lstinputlisting[linerange=option_monad-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The three proofs are straightforward.

Beyond the standard operations, it can be useful to throw and catch exceptions.
This can be implemented as follows:
%
\lstinputlisting[linerange=option_throw_catch-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The \li{Option.throw} operation raises an exception, leaving the program in an
error state (\li{Option.none}). The \li{Option.catch} operation can be used
to recover from an earlier exception. If the program is currently in an error
state, \li{Option.catch} invokes some exception-handling code (its second
argument). This code might in turn raise a new exception. If \li{Option.catch}
is applied to a normal state (of the form \li{Option.some a}), nothing happens.

As a convenient alternative to \li{Option.}\allowbreak\li{catch ma ma'}, Lean
supports the syntax \li{ma.catch ma'}. Here is a schematic example that
demonstrates throwing and catching with this syntax:
%
\begin{lstlisting}
do
  …
  if … then
    Option.throw
  else
    …
.catch do
  …
\end{lstlisting}
%
The corresponding Java code would look as follows:
%
{\tabletsmall
\begin{lstlisting}[language=minijavaandc]
try {
    …
    if (…) {
        throw new UnknownException();
    } else {
        …
    }
} catch (UnknownException e) {
    …
}
\end{lstlisting}}

Options cater for only one kind of error state. A more general abstraction,
called \emph{error monad}, supports different errors, as with the exceptions of
Java and other programming languages.

\section{Mutable State}
\label{sec:mutable-state}

The \emph{state monad} provides an abstraction corresponding to a mutable
state. For some programming languages, the compiler can detect the use of the
state monad and translate programs using them to more efficient imperative
programs.

Admittedly, ``abstraction corresponding to a mutable state'' may sound somewhat
abstract, so let us consider a semiconcrete example. If you have some
experience with functional programming, you probably at some point or other
have written code that looks very much like this fragment:

\begin{lstlisting}
def welcomeNewUser (userName : String) (ctxt : Context) :
  (ℕ × String) × Context :=
  let
    (user, ctxt') := createUser userName ctxt
    (password, ctxt'') := generateTemporaryPassword user ctxt'
    (ok, ctxt''') := sendUnencryptedEmail user password ctxt''
  in
    ((user, password), ctxt''')
\end{lstlisting}
%
(It is very important to send the password in an unencrypted email, and to
ignore the \li{ok} status of the function.) The function takes some global
state or context as input and invokes three functions in turn, each of which
takes a context value and returns both some data and a new context. The context
is effectively \emph{threaded through} the program. This allows us to have a
mutable state in a programming language without side effects.

The above approach is error-prone---it is all too easy to forget one prime
(\li{'}) and pass the wrong context to a function. The code is also cluttered by
all the context variables. What if we could simply write the following instead?

\begin{lstlisting}
def welcomeNewUserDo (userName : String) :
  Context → (ℕ × String) × Context :=
  do
    let user ← createUser userName
    let password ← generateTemporaryPassword user
    let ok ← sendUnencryptedEmail user password
    pure (user, password)
\end{lstlisting}
%
This is exactly what the state monad provides.

The state monad builds on top of a binary type constructor \li{Action}, which
captures the concept of computations or actions over states of type \li{σ} with
return values of type \li{α}. In Lean, \hbox{\li{Action}} \li{σ} \li{α} is
defined as equal to \li{σ → α × σ}:%
\footnote{This type constructor is traditionally called \texttt{State}, but this
name is very confusing.}
%
\lstinputlisting[linerange=action-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
(Since types are terms, we can use \li{def} also to define type abbreviations.)
For a given type \li{σ}, we have that \li{Action σ : Type} \li{→} \li{Type} is a
monad. The type \li{σ} abstracts over the exact memory layout. We could use
tuples or lists to represent memory, for example, and instantiate the abstract
state \li{σ} accordingly.

A stateful action is a function that takes some state and returns both a value
and some new state. The \li{σ →} part of \hbox{\li{Action}'s} definition
gives the old state; the left component of the cartesian product, \li{α},
gives the result of the computation; and the right component of the product,
\li{σ}, gives the new state. Thus, the state is implicitly threaded through
the program. As with other effectful programs, the \li{do} notation only
exposes the data---the value of type~\li{α}---and conceals the effect---the old
and new \li{σ} states.

The case where \li{σ := Unit}, a type of cardinality one (similar to \li{void}
in C or Java) whose unique value is written \li{()}, corresponds to the
identity monad: The type \li{Unit → α × Unit} is isomorphic to \li{α}. This
intuition can guide us when defining \li{pure} and \li{bind}.

We start by defining basic operations:\ two operations, \li{read} and
\li{write}, to access the memory, and the standard operations \li{bind} and
\li{pure}:

\lstinputlisting[linerange=action_monad_defs-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The \li{read} operation simply returns the current state \li{s} (in the first
pair component) and leaves the state unchanged (in the second pair component).
The \li{write} operation replaces the current state with \li{s} and returns
\li{()}. The \li{pure} operation returns the current state \li{s} unchanged
tupled together with the given value \li{a}. The \hbox{\li{bind}} operation
passes the initial state to the \li{ma} argument, yielding a result \li{a} and a
new state \li{s'}. These are passed to \li{f}, which returns a new result and a
new state.

To register the \li{Action} type constructor as a lawful monad,
we need as before to prove the three laws:

\lstinputlisting[linerange=action_monad_register-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
Notice that, in all three proofs, we unfold the definitions of the generic
\li{pure} and \li{bind} constants to expand them to \li{Action.pure} and
\li{Action.bind}, whose definitions we also expand.

As a concrete example, the following program removes all elements that are
smaller than a previous element in the list, leaving us with a list of
increasing elements. The maximal element is stored as the state~\li{σ}.
Notice how the state is accessed by \li{read} and \li{write}.

\lstinputlisting[linerange=increasingly-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}

To execute the program, we must supply an initial state. The last state is
returned along with the resulting list. It corresponds to the largest element
encountered in the list or the start state. Thus, the commands

\lstinputlisting[linerange=increasingly_eval-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
produce the output

\begin{lstlisting}[language=]
([1, 2, 3], 3)
([1, 2, 3, 4, 5], 5)
\end{lstlisting}

\section{Nondeterminism}
\label{sec:nondeterminism}

Whereas the option monad stores zero or one \li{α} values and the identity and
state monads store exactly one value, the \emph{set monad} stores a possibly
infinite number of values. This is useful to model nondeterminism, as a set of
possible behaviors.

Lean's type \li{Set α} is defined as \li{α → Prop}. In other words, a set is
identified with its characteristic predicate. Familiar operators such as
the empty set (\li{∅}), the universal set (\li{Set.univ}), union \hbox{(\li{∪}),}
intersection (\li{∩}), and membership (\li{∈}) are supported, as well as
traditional curly brace notations such as \li${a}$, \li${a, b}$, and
\li${x |$ \li$P x}$. Many set constructs can be simplified by \li{simp}.

The \li{Set} type constructor can be registered as a lawful monad as follows:

\lstinputlisting[linerange=set_monad-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The \li{pure} operation simply puts the given value \li{a} in a singleton set
\li${a}$. The \li{bind} operation calls \li{f} on all values in the set \li{A}
and returns the union of all the results. For example, if \hbox{\li$A := {3, 8}$} and
\li$f := (fun a ↦ {a + 1, a + 2})$, then \li|set.bind A f| equals
\hbox{\li|{4, 5, 9, 10}|.}

The last proof relies on \emph{set extensionality},
which states that two sets that contain the same elements must be equal:
%
\[\hbox{\lic$Set.ext {α : Type} {A B : set α}$ \lic{:} \lic|(∀x, x ∈ A ↔ x ∈ B) → A = B|}\]
%
Another noteworthy point is the use of the \li{aesop} tactic. The
goal's target is
\begin{align*}
\hbox{\li$\∀x,$~}
  & \hbox{\li$x ∈ {b | ∃ a, (∃ a_1, a_1 ∈ ma ∧ a ∈ f a_1) ∧ b ∈ g a}$} \\[-\jot]
  & \hbox{\li$\↔ x ∈ {b | ∃ a, a ∈ ma ∧ ∃ a_1, a_1 ∈ f a ∧ b ∈ g a_1}$}
\end{align*}
%
where the two sides of \li{↔} are the same except for the placement of the
existential quantifiers (and, confusingly, the names of the bound variables).
This ugly proposition could be proved by a tedious sequence of introduction and
elimination, but we deserve more automation.

\section{Aesop Tactic}
\label{sec:aesop-tactic}

\subsection*{aesop}

The \li{aesop} tactic \cite{limperg-from-2023}, whose name stands for Automated
Extensible Search for Obvious Proofs, is a general-purpose proof search tactic.
Among others, it performs elimination of the logical symbols \li{∧}, \li{∨},
\li{↔}, and \li{∃} in hypotheses and introduction of \li{∧}, \li{↔}, and \li{∃}
in the target, and it regularly invokes \li{simp}. It can succeed at proving a
goal, fail, or succeed partially, leaving some unfinished subgoals to the user.

\section{A Generic Algorithm: Iteration over a List}
\label{sec:a-generic-algorithm-iteration-over-a-list}

Suppose we apply an effectful function \li{f} on all elements of a list using
\li{map}. We then obtain a regular list of effectful values. For example:

\lstinputlisting[linerange=nths_fine-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
The function \li{nthsFine xss n} tries to extract the \li{(n + 1)}st element of
each list in \li{xss}. Running

\lstinputlisting[linerange=nths_fine_eval-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
returns \li{[Option.some 13, Option.some 23]}.

These \li{Option.some} constructors can be inconvenient. Often, we only care
about whether any error arose. This leads us to our final example:\ a generic
effectful program \li{mmap} that iterates over a list and applies an effectful
function \li{f} to each element. The definition is recursive:

\lstinputlisting[linerange=mmap_def-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
Notice that the function returns a single \li{m} value containing a list and
not a list of \li{m} values. Try to work out why it is well typed and has the
desired behavior.

We can now trying using \li{mmap} instead of \li{map}:

\lstinputlisting[linerange=nths_coarse-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
Running

\lstinputlisting[linerange=nths_coarse_eval-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}
%
returns \li{Option.some [13, 23]}, with a single \li{Option.some} around a pure list.

The \li{mmap} function distributes over the append operator \li{++}. The \li{do}
notation is useful not only for defining functions but also for stating their
properties:

\lstinputlisting[linerange=mmap_append-q]{../lean/LoVe/LoVe07_EffectfulProgramming_DemoMaster.lean}

%Incidentally, Lean already includes a function called \li{List.mmap} corresponding to our
%\li{mmap}.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Notations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|do| & indicates the start of an effectful program \\
\lic|let … ← …| & assigns a variable in an effectful program \\
\li|>>=| & composes effectful computations \\
\end{xltabular}

\subsection*{Theorem}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|Set.ext| & set extensionality \\
\end{xltabular}

\subsection*{Tactic}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|aesop| & proves propositions using a generic search procedure \\
\end{xltabular}

\endgroup
