\chapter{Monads}
\label{chap:monads}

We take a look at an important functional programming abstraction:\ monads.
Monads generalize computation with side effects. Haskell has shown that monads
can be used very successful to write imperative programs. In Lean, they are
used to write imperative programs, but also to reason about them via the
so-called monadic laws. Monads are even useful for programming Lean
itself---or metaprogramming Lean---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 strongly recommend that you read that chapter
to get a more complete picture of monads in Lean. We also refer to Chapter~14 of
\emph{Real World Haskell} \cite{osullivan-et-al-2008} for a general introduction
to monads.

\section{Motivating Example}

Consider the following programming task: Implement a function
\li{sum_2_5_7 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 if the
list has fewer than seven elements, you can return \li{none}.

A straightforward implementation follows:

\lstinputlisting[linerange=sum_2_5_7₁-q]{../lean/love06_monads_demo_master.lean}
%
(Recall that \li{nth} counts elements from 0; thus, the second element is at
position 1, etc.) The code is quite ugly, because of all the pattern matching
on \li{option}. Can we do better? It turns out we can. We can put all the
ugliness in one function, which we call \li{bind_option}:

\lstinputlisting[linerange=bind_option-q]{../lean/love06_monads_demo_master.lean}

That function operates on an option (a value of type \li{option}). If the
option is \li{none}, we leave it as is. This corresponds to an error
condition, and errors are preserved. Otherwise, if the option is \li{some a}
for some \li{a}, then we apply the specified operation \li{f} on \li{a}.

We can now use \li{bind_option} to program our sum function:

\lstinputlisting[linerange=sum_2_5_7₂-q]{../lean/love06_monads_demo_master.lean}

Intuitively, the program reads as follows:

\begin{itemize}
\item Extract the second item from the list. If it is \li{none}, we are done.
  Otherwise, we obtain this item as \li{n2} and continue with the next step.
\item Perform the same for the fifth and seventh item, mutatis mutandis.
\item Return the sum of \li{n2}, \li{n5}, and \li{n7} in a \li{some} wrapper.
\end{itemize}

Semantically, our new function \li{sum_2_5_7₂} is equal to the original
\li{sum_2_5_7}.

Instead of defining \li{bind_option} 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=sum_2_5_7₃-q]{../lean/love06_monads_demo_master.lean}

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

\lstinputlisting[linerange=sum_2_5_7₄-q]{../lean/love06_monads_demo_master.lean}
%
The syntax \li{ma >>= f} expands to \li{bind ma f}.

The penultimate version of the sum program uses heavier syntactic sugar:

\lstinputlisting[linerange=sum_2_5_7₅-q]{../lean/love06_monads_demo_master.lean}

The \li{do} notation provides an intuitive notation for monads.
\li{do a ← ma, t} is syntactic sugar for \li{ma >>= λa, t}. If we do not care
about the return result of \li{ma}'s computation, we can write \li{do ma, t},
which expands to \li{ma >>= λ_, t}.

For convenience, the notation allows multiple \li{←} assignments in a single
\li{do} block. This brings us to the final version of the program:

\lstinputlisting[linerange=sum_2_5_7₆-q]{../lean/love06_monads_demo_master.lean}

Each line with an arrow \li{←} attempts to read a value. In case of failure, the
entire program evaluates to \li{none}. Although the notation has an imperative
flavor, the function is a pure functional program.

\section{Overview}

The \li{option} type constructor is an example of a monad. In general, a monad
is a type constructor \li{m} that depends on some type parameter
\li{α}---i.e., \li{m α}---equipped with two distinguished operations:
%
\begin{center}
\begin{tabular}{@{}r@{}c@{}l@{}}
\verb|pure| & ${}:{}$ & \li|Π{α : Type}, α → m α| \\
\verb|bind| & ${}:{}$ & \li|Π{α β : Type}, m α → (α → m β) → m β| \\
\end{tabular}
\end{center}
%
Recall that curly braces denote implicit arguments. For options, the \li{pure}
operation is simply \li{some}, whereas \li{bind} is what we called
\li{bind_option}.

Intuitively, we can think of a monad as a ``box'' containing some data. The
operation \li{pure} puts the 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 is an \li{m β} monad, not an \li{m α} monad. But there is no
general way to extract the data from the monad, i.e., to obtain an \li{α} from
an \li{m α}.

To summarize, \li{pure a} (also called \li{return a}) simply provides a box
containing the the value \li{a}, with no side effects, whereas \li{bind ma f}
(also written \li{ma >>=} \li{f}) executes \li{ma}, then executes \li{f} with
the boxed result \li{a} of \li{ma}.

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

\kern\belowdisplayskip

\begin{center}
\begin{tabular}{@{}l@{\quad}l@{}}
\toprule
Type & Effect \\
\midrule
\li|option α| & failure when \li|none|; otherwise, \li|some (a : α)| is the result \\
\li|set α| & nondeterministic behavior (set of behaviors) \\
\li|t → α| & reading elements of type \li|t| (e.g., a configuration) \\
\li|ℕ × α| & adjoining running time (e.g., to model algorithmic complexity) \\
\li|string × α| & adjoining text output (e.g., for logging) \\
\li|prob α| & probability (e.g., using random number generators) \\
\li|io α| & interaction with the operating system \\
\li|tactic α| & interaction with the prover \\
\bottomrule
\end{tabular}
\end{center}

All of the above are type constructors \li{m} are parameterized by a type
\li{α}. Some effects can be combined (e.g.,
\li{option (t → α)}). Some effects are not executable (e.g., \li{set α},
\li{prob α}); they are nonetheless useful for modeling programs abstractly in
the logic.

Specific monads \li{m} may provide further operators. For example, they may
provide a way to extract the boxed value stored in the monad without
\li{bind}'s requirement of putting it back in a monad.

Monads have several benefits. We get the convenient and highly readable
\li{do} notation. They also offer generic operations, such as
\li{mmap : (α → M β) → list α → M (list β)}, which work uniformly across
all monad instances. To quote \emph{Programming in Lean}
\cite{programming-in-lean},
``The power of the abstraction is not only that it provides general functions
and notation the 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.''

\section{Monadic Laws}

The \li{bind} and \li{pure} operations are normally required to obey three
laws, called the monadic laws.

\newcommand\BIGEQ{\qquad\smash{\lower.6ex\hbox{\huge\li|=|}}\qquad\hbox{}}

The \li{bind} operation combines two programs. If either of these is simply
pure data, we can eliminate the \li{bind}. This gives us the first two monadic
laws. The first law:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}l@{}l@{}l@{}}
\li|(do| \\
\quad \li|a' ← pure a,| & \BIGEQ & \li|f a| \\
\quad \li|f a')|
\end{tabular}}

\vskip\belowdisplayskip

\noindent
The second law:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}l@{}l@{}l@{}}
\li|(do| \\
\quad \li|a ← x,| & \BIGEQ & \li|x| \\
\quad \li|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}{@{}l@{}l@{}l@{}}
\li|(do| &
  & \li|(do| \\
\quad \li|b ← (do| &
  & \quad \li|a ← x,| \\
\qquad \li|a ← x,| & \BIGEQ
  & \quad \li|b ← f a,| \\
\qquad \li|f a),| &
  & \quad \li|g b)| \\
\quad \li|g b)|
\end{tabular}}

\vskip\belowdisplayskip

\section{A Type Class of Monads}

Monads are a mathematical structure, so we use \li{class} to add them as a
type class. Type classes will be covered in more detail in
Chapter~\ref{chap:basic-mathematical-structures}. We can think of a type
class as a structure or record that is parameterized by a type---or here,
by a type constructor \li{m : Type → Type}.

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

\lstinputlisting[linerange=lawful_monad-q]{../lean/love06_monads_demo_master.lean}

Let us analyze this definition step by step:

\begin{itemize}
\item We are creating a structure parameterized by a unary type constructor
  \li{m : Type → Type}.

\item The type class inherits the fields, and any syntactic sugar, from
  type classes called \li{has_bind} and \li{has_pure}. These provide the
  \li{bind} and \li{pure} operations on \li{m}, with the expected types and
  the syntactic sugar.

\item The type \li{Type 1} is a technical necessity. Because monads quantify
  over types, they cannot be standard types themselves. They need to live in a
  larger type universe, called \li{Type 1}. (The familiar \li{Type} type of
  types is also called \li{Type 0}.) We will come back to this fine point in
  Chapter~\ref{chap:logical-foundations-of-mathematics}.

\item Finally, the definition adds three fields to those already provided by
  \li{has_}\allowbreak\li{bind} and \li{has_pure}. Each field is a proof of one
  of the three monadic laws.
\end{itemize}

We call our type class ``lawful monad'' because the monadic laws are required
to hold. To instantiate this definition with a concrete monad (e.g., the
option monad), we must supply the monad \li{m}, suitable \li{bind} and
\li{pure} operators, and proofs corresponding to the three monadic laws.

Our definition captures the essence of Lean's predefined concept of monads.
Lean's actual definition is more complicated. One of the differences is that
it distributes the definition over two type classes, called \li{monad} and
\li{is_lawful_monad}.

\section{The Option Monad}

The following code extract shows how to register the type constructor
\li{option : Type → Type} as a lawful monad:
%
\lstinputlisting[linerange=option_monad-q]{../lean/love06_monads_demo_master.lean}
%
The registration process requires us to provide five components:\
the \li{pure} and \li{bind} operations and the proofs of the three monadic laws.
To avoid polluting the name space, we tidily put our code in an \li{option}
namespace. For the first and second components of the record, we use the \li{@}
syntax to make the type arguments explicit, in agreement with the format
expected by \li{has_pure} and \li{has_bind}. The three proofs are
straightforward.

\section{The State Monad}

The next monad is called the state monad. It provides an abstraction
corresponding to a mutable state. For some programming languages, the compiler
can detect the use of the state monad and translate state-monadic programs to
more efficient imperative programs.

The type constructor is

\lstinputlisting[linerange=state-q]{../lean/love06_monads_demo_master.lean}
%
For a given \li{σ}, we have that \li{state σ : Type → Type} is a monad. We
abstract over the exact memory layout. We could use tuples or lists to
represent memory, for example, and instantiate the abstract \li{σ}
accordingly.

Intuitively, the \li{σ →} part of \li{state}'s definition provides the current
state; the left component of the cartesian product, \li{α}, is where the
result of a computation goes; and the right component of the product, \li{σ},
can be used to provide a new state, overwriting the received one. Thus, the
state is threaded through the monadic program.

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

\lstinputlisting[linerange=state_monad_defs-q]{../lean/love06_monads_demo_master.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 state \li{s} with \li{t} and returns an
empty tuple.

The \li{pure} operation returns the current state \li{s} unchanged tupled
together with the given value \li{a}.

The \li{bind} operation passes the initial state to the \li{f} argument,
yielding a result \li{a} and a new state \li{t}. These are passed to \li{g},
which returns a new result and a new state.

Registering the state monad as a lawful monad is similar as for \li{option},
but we need to reason about functional extensionality (\li{funext}). Namely,
to prove \li{f = g}, it suffices to prove \li{∀x, f x = g x}.

\lstinputlisting[linerange=state_monad_register-q]{../lean/love06_monads_demo_master.lean}

As an example, the following state-monadic 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 in the monad.

\lstinputlisting[linerange=diff_list-q]{../lean/love06_monads_demo_master.lean}

Notice how the state is accessed by \li{read} and \li{write}.

To execute the program, we must provide a start state. We also get back the
last state, which is the largest element seen in the list or the start state:

\lstinputlisting[linerange=diff_list_eval-q]{../lean/love06_monads_demo_master.lean}
%
Output:

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

\section{Example: Generic Iteration over a List}

As a final example, we consider a generic monadic program \li{mmap} that
iterates over a list and applies a function \li{f} to each element. The
definition is recursive and monadic:

\lstinputlisting[linerange=mmap_def-q]{../lean/love06_monads_demo_master.lean}

Notice that the function returns a single monad containing the resulting list,
not a list of monads. Try to work out why the function is well typed and has
the expected behavior.

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

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

Here is an example of how we could use \li{mmap}:

\lstinputlisting[linerange=nths-q]{../lean/love06_monads_demo_master.lean}

The function \li{nths xss n} selects the (\textit{n} + 1)st elements of
each list in \li{xss}. It fails with \li{none} if one of the list is not
long enough. For example, the call

\lstinputlisting[linerange=nths_eval-q]{../lean/love06_monads_demo_master.lean}
%
produces the result \li{some [13, 23, 33]}.

\section{Summary of New Syntax}

\small

\subsection{Declaration}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|class| & declares a structure as a type class \\
\end{tabularx}

\subsection{Monadic Notations}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|do| & indicates the start of a monadic program \\
\li{>>=} & combines effectful computations \\
\end{tabularx}
