# Monads

Building on Functors and Applicatives we can now introduce monads.

A monad is another type of abstract, functional structure. Let's explore what makes it different from the first two structures.

## What is a Monad?

A monad is a computational context. It provides a structure that allows you to chain together operations that have some kind of shared state or similar effect. Whereas pure functional code can only operate on explicit input parameters and affect the program through explicit return values, operations in a monad can affect other computations in the chain implicitly through side effects, especially modification of an implicitly shared value.

## How are monads represented in Lean?

Like functors and applicatives, monads are represented with a type class in Lean:

```
class Monad (m : Type u → Type v) extends Applicative m, Bind m where
```

Just as every applicative is a functor, every monad is also an applicative and there's one more new
base type class used here that you need to understand, namely, `Bind`

.

```
class Bind (f : Type u → Type v) where
bind : {α β : Type u} → f α → (α → f β) → f β
```

The `bind`

operator also has infix notation `>>=`

where `x >>= g`

represents the result of executing
`x`

to get a value of type `f α`

then unwrapping the value `α`

from that and passing it to function
`g`

of type `α → f β`

returning the result of type `f β`

where `f`

is the target structure type
(like `Option`

or List)

This `bind`

operation looks similar to the other ones you've seen so far, if you put them all
together `Monad`

has the following operations:

```
class Monad (f : Type u → Type v) extends Applicative f, Bind f where
pure {α : Type u} : α → f α
map : {α β : Type u} → (α → β) → f α → f β
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
bind : {α β : Type u} → f α → (α → f β) → f β
...
```

Notice `Monad`

also contains `pure`

it must also have a "default" way to wrap a value in the
structure.

The `bind`

operator is similar to the applicative `seq`

operator in that it chains two operations,
with one of them being function related. Notice that `bind`

, `seq`

and `map`

all take a function of
some kind. Let's examine those function types:

- map:
`(α → β)`

- seq:
`f (α → β)`

- bind:
`(α → f β)`

So `map`

is a pure function, `seq`

is a pure function wrapped in the structure, and `bind`

takes a
pure input but produces an output wrapped in the structure.

Note: we are ignoring the `(Unit → f α)`

function used by `seq`

here since that has a special
purpose explained in Applicatives Lazy Evaluation.

## Basic Monad Example

Just as `Option`

is a functor and an applicative functor, it is also a monad! Let's start with how
`Option`

implements the Monad type class.

`instance`**: **Monad Option

instance : `Monad`**: **(Type u_1 → Type u_1) → Type (u_1 + 1)

Monad `Option`**: **Type u_1 → Type u_1

Option where
pure := `Option.some`**: **{α : Type u_1} → α → Option α

Option.some
bind := `Option.bind`**: **{α β : Type u_1} → Option α → (α → Option β) → Option β

Option.bind

where:

```
def Option.bind : Option α → (α → Option β) → Option β
| none, _ => none
| some a, f => f a
```

Side note: this function definition is using a special shorthand syntax in Lean where the`:= match a, b with`

code can be collapsed away. To make this more clear consider the following simpler example, where`Option.bind`

is using the second form like`bar`

:

deffoo (foo:Option Nat → Nat → Option Natx :x:Option NatOptionOption:Type → TypeNat) (Nat:Typey :y:NatNat) :Nat:TypeOptionOption:Type → TypeNat := matchNat:Typex,x:Option Naty with |y:Natnone, _ =>none:{α : Type ?u.141} → Option αnone |none:{α : Type} → Option αsomesome:{α : Type ?u.159} → α → Option αx,x:Naty =>y:Natsome (some:{α : Type} → α → Option αx +x:Naty) defy:Natbar :bar:Option Nat → Nat → Option NatOptionOption:Type → TypeNat →Nat:TypeNat →Nat:TypeOptionOption:Type → TypeNat |Nat:Typenone, _ =>none:{α : Type ?u.304} → Option αnone |none:{α : Type} → Option αsomesome:{α : Type ?u.322} → α → Option αx,x:Naty =>y:Natsome (some:{α : Type} → α → Option αx +x:Naty)y:Natfoo (foo:Option Nat → Nat → Option Natsomesome:{α : Type} → α → Option α1)1:Nat2 -- some 32:Natbar (bar:Option Nat → Nat → Option Natsomesome:{α : Type} → α → Option α1)1:Nat2 -- some 32:Nat

What is important is that `Option.bind`

is using a `match`

statement to unwrap the input value
`Option α`

, if it is `none`

then it does nothing and returns `none`

, if it has a value of type `α`

then it applies the function in the second argument `(α → Option β)`

to this value, which is
the expression `f a`

that you see in the line ` | some a, f => f a`

above. The function
returns a result of type `Option β`

which then becomes the return value for `bind`

. So there
is no structure wrapping required on the return value since the input function already did that.

But let's bring in the definition of a monad. What does it mean to describe `Option`

as a
computational context?

The `Option`

monad encapsulates the context of failure. Essentially, the `Option`

monad lets us
abort a series of operations whenever one of them fails. This allows future operations to assume
that all previous operations have succeeded. Here's some code to motivate this idea:

defoptionFunc1 :optionFunc1:String → Option NatString ->String:TypeOptionOption:Type → TypeNat |Nat:Type"" =>"":Stringnone |none:{α : Type} → Option αstr =>str:Stringsomesome:{α : Type} → α → Option αstr.str:Stringlength deflength:String → NatoptionFunc2 (optionFunc2:Nat → Option Floati :i:NatNat) :Nat:TypeOptionOption:Type → TypeFloat := ifFloat:Typei %i:Nat2 ==2:Nat0 then0:Natnone elsenone:{α : Type} → Option αsome (some:{α : Type} → α → Option αi.i:NattoFloat *toFloat:Nat → Float3.14159) def3.14159:FloatoptionFunc3 (optionFunc3:Float → Option (List Nat)f :f:FloatFloat) :Float:TypeOption (Option:Type → TypeListList:Type → TypeNat) := ifNat:Typef >f:Float15.0 then15.0:Floatnone elsenone:{α : Type} → Option αsome [some:{α : Type} → α → Option αf.f:Floatfloor.floor:Float → FloattoUInt32.toUInt32:Float → UInt32toNat,toNat:UInt32 → Natf.f:Floatceil.ceil:Float → FloattoUInt32.toUInt32:Float → UInt32toNat] deftoNat:UInt32 → NatrunOptionFuncs (runOptionFuncs:String → Option (List Nat)input :input:StringString) :String:TypeOption (Option:Type → TypeListList:Type → TypeNat) := matchNat:TypeoptionFunc1optionFunc1:String → Option Natinput with |input:Stringnone =>none:{α : Type ?u.904} → Option αnone |none:{α : Type} → Option αsomesome:{α : Type ?u.915} → α → Option αi => matchi:NatoptionFunc2optionFunc2:Nat → Option Floati with |i:Natnone =>none:{α : Type ?u.931} → Option αnone |none:{α : Type} → Option αsomesome:{α : Type ?u.941} → α → Option αf =>f:FloatoptionFunc3optionFunc3:Float → Option (List Nat)ff:FloatrunOptionFuncsrunOptionFuncs:String → Option (List Nat)"big" -- some [9, 10]"big":String

Here you see three different functions that could fail. These are then combined in `runOptionFuncs`

.
But then you have to use nested `match`

expressions to check if the previous result succeeded. It
would be very tedious to continue this pattern much longer.

The `Option`

monad helps you fix this. Here's what this function looks like using the `bind`

operator.

defrunOptionFuncsBind (runOptionFuncsBind:String → Option (List Nat)input :input:StringString) :String:TypeOption (Option:Type → TypeListList:Type → TypeNat) :=Nat:TypeoptionFunc1optionFunc1:String → Option Natinput >>=input:StringoptionFunc2 >>=optionFunc2:Nat → Option FloatoptionFunc3optionFunc3:Float → Option (List Nat)runOptionFuncsBindrunOptionFuncsBind:String → Option (List Nat)"big" -- some [9, 10]"big":String

It's much cleaner now! You take the first result and pass it into the second and third functions
using the `bind`

operation. The monad instance handles all the failure cases so you don't have to!

Let's see why the types work out. The result of `optionFunc1`

input is simply `Option Nat`

. Then the
bind operator allows you to take this `Option Nat`

value and combine it with `optionFunc2`

, whose type
is `Nat → Option Float`

The **bind operator resolves** these to an `Option Float`

. Then you pass this
similarly through the bind operator to `optionFunc3`

, resulting in the final type, `Option (List Nat)`

.

Your functions will not always combine so cleanly though. This is where `do`

notation comes into play.
This notation allows you to write monadic operations one after another, line-by-line. It almost makes
your code look like imperative programming. You can rewrite the above as:

defrunOptionFuncsDo (runOptionFuncsDo:String → Option (List Nat)input :input:StringString) :String:TypeOption (Option:Type → TypeListList:Type → TypeNat) := do letNat:Typei ←i:NatoptionFunc1optionFunc1:String → Option Natinput letinput:Stringf ←f:FloatoptionFunc2optionFunc2:Nat → Option Floatii:NatoptionFunc3optionFunc3:Float → Option (List Nat)ff:FloatrunOptionFuncsDorunOptionFuncsDo:String → Option (List Nat)"big" -- some [9, 10]"big":String

The `←`

operator used here is special. It effectively unwraps the value on the right-hand side from
the monad. This means the value `i`

has type `Nat`

, *even though* the result of `optionFunc1`

is
`Option Nat`

. This is done using a `bind`

operation under the hood.

Note you can use

`<-`

or the nice unicode symbol`←`

which you can type into VS code by typing these characters`\l`

. When you type the final space,`\l`

is replaced with`←`

.

Observe that we do not unwrap the final line of the computation. The function result is `Option (List Nat)`

which matches what `optionFunc3`

returns. At first glance, this may look more complicated
than the `bind`

example. However, it gives you a lot more flexibility, like mixing monadic and
non-monadic statements, using if then/else structures with their own local do blocks and so on. It
is particularly helpful when one monadic function depends on multiple previous functions.

## Example using List

You can easily make `List`

into a monad with the following, since List already provides an
implementation of `pure`

and `bind`

.

`instance`**: **Monad List

instance : `Monad`**: **(Type u_1 → Type u_1) → Type (u_1 + 1)

Monad `List`**: **Type u_1 → Type u_1

List where
pure := `List.pure`**: **{α : Type u_1} → α → List α

List.pure
bind := `List.bind`**: **{α β : Type u_1} → List α → (α → List β) → List β

List.bind

Like you saw with the applicative `seq`

operator, the `bind`

operator applies the given function
to every element of the list. It is useful to look at the bind implementation for List:

```
open List
def
````bind`**: **{α : Type u_1} → {β : Type u_2} → List α → (α → List β) → List β

bind (`a`**: **List α

a : `List`**: **Type u_1 → Type u_1

List `α`**: **Type u_1

α) (`b`**: **α → List β

b : `α`**: **Type u_1

α → `List`**: **Type u_2 → Type u_2

List `β`**: **Type u_2

β) : `List`**: **Type u_2 → Type u_2

List `β`**: **Type u_2

β := `join`**: **{α : Type u_2} → List (List α) → List α

join (`map`**: **{α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β

map `b`**: **α → List β

b `a`**: **List α

a)

So `Functor.map`

is used to apply the function `b`

to every element of `a`

but this would
return a whole bunch of little lists, so `join`

is used to turn those back into a single list.

Here's an example where you use `bind`

to convert a list of strings into a combined list of chars:

"apple"."apple":StringtoList -- ['a', 'p', 'p', 'l', 'e']toList:String → List Char["apple","apple":String"orange"] >>="orange":StringString.toList -- ['a', 'p', 'p', 'l', 'e', 'o', 'r', 'a', 'n', 'g', 'e']String.toList:String → List Char

## The IO Monad

The `IO Monad`

is perhaps the most important monad in Lean. It is also one of the hardest monads to
understand starting out. Its actual implementation is too intricate to discuss when first learning
monads. So it is best to learn by example.

What is the **computational context** that describes the IO monad? IO operations can read
information from or write information to the terminal, file system, operating system, and/or
network. They interact with systems outside of your program. If you want to get user input, print a
message to the user, read information from a file, or make a network call, you'll need to do so
within the IO Monad.

The state of the world outside your program can change at virtually any moment, and so this IO context is particularly special. So these IO operations are "side effects" which means you cannot perform them from "pure" Lean functions.

Now, the most important job of pretty much any computer program is precisely to perform this
interaction with the outside world. For this reason, the root of all executable Lean code is a
function called main, with the type `IO Unit`

. So every program starts in the IO monad!

When your function is `IO`

monadic, you can get any input you need, call into "pure" code with the
inputs, and then output the result in some way. The reverse does not work. You cannot call into IO
code from pure code like you can call into a function that takes `Option`

as input. Another way to
say this is you cannot invent an `IO`

context out of thin air, it has to be given to you in your
`main`

function.

Let's look at a simple program showing a few of the basic IO functions. It also uses `do`

notation
to make the code read nicely:

`def ``main`**: **IO Unit

main : `IO`**: **Type → Type

IO `Unit`**: **Type

Unit := do
`IO.println`**: **{α : Type} → [inst : ToString α] → α → IO Unit

IO.println `"enter a line of text:"`**: **String

"enter a line of text:"
let `stdin`**: **IO.FS.Stream

stdin ← `IO.getStdin`**: **BaseIO IO.FS.Stream

IO.getStdin -- IO IO.FS.Stream (monadic)
let `input`**: **String

input ← `stdin`**: **IO.FS.Stream

stdin.`getLine`**: **IO.FS.Stream → IO String

getLine -- IO.FS.Stream → IO String (monadic)
let `uppercased`**: **String

uppercased := `input`**: **String

input.`toUpper`**: **String → String

toUpper -- String → String (pure)
`IO.println`**: **{α : Type} → [inst : ToString α] → α → IO Unit

IO.println `uppercased`**: **String

uppercased -- IO Unit (monadic)

So, once again you can see that the `do`

notation lets you chain a series of monadic actions.
`IO.getStdin`

is of type `IO IO.FS.Stream`

and `stdin.getLine`

is of type `IO String`

and `IO.println`

is of type `IO Unit`

.

In between you see a non-monadic expression `let uppercased := input.toUpper`

which is fine too.
A let statement can occur in any monad. Just as you could unwrap `i`

from `Option Nat`

to get the
inner Nat, you can use `←`

to unwrap the result of `getLine`

to get a String. You can then manipulate
this value using normal pure string functions like `toUpper`

, and then you can pass the result to the
`IO.println`

function.

This is a simple echo program. It reads a line from the terminal, and then prints the line back out capitalized to the terminal. Hopefully it gives you a basic understanding of how IO works.

You can test this program using `lean --run`

as follows:

```
> lean --run Main.lean
enter a line of text:
the quick brown fox
THE QUICK BROWN FOX
```

Here the user entered the string `the quick brown fox`

and got back the uppercase result.

## What separates Monads from Applicatives?

The key that separates these is **context**. You cannot really determine the structure of
"future" operations without knowing the results of "past" operations, because the past can alter the
context in which the future operations work. With applicatives, you can't get the final function
result without evaluating everything, but you can determine the structure of how the operation will
take place. This allows some degree of parallelism with applicatives that is not generally possible
with monads.

## Conclusion

Hopefully you now have a basic level understanding of what a monad is. But perhaps some more examples of what a "computational context" means would be useful to you. The Reader, State and Except monads each provide a concrete and easily understood context that can be compared easily to function parameters. You can learn more about those in Reader monads, State monads, and the Except monad.