# Monad Laws

In the previous sections you learned how to use Functors, Applicatives, and Monads, and you played with some useful instances including Option, IO, Reader, State and Except and you learned about composition using Monad Transformers.

So far, you've learned the concrete details you need in order to *use* monads in your Lean programs.
But there's still one more important concept you need if you want to *create* new functors,
applicatives and monads. Namely, the notion of *structural "laws"* -- rules that these type
classes should follow in order to meet other programmers' expectations about your code.

## Life without Laws

Remember Lean represents each of these abstract structures by a type class. Each of these type classes has one or two main functions. So, as long as you implement those functions and it type checks, you have a new functor, applicative, or monad, right?

Well not quite. Yes, your program will compile and you'll be able to use the instances. But this doesn't mean your instances follow the mathematical constructs. If they don't, your instances won't fulfill other programmers' expectations. Each type class has its own "laws". For instance, suppose you have the following Point Functor:

structurePoint (Point:{α : Type} → α → α → Point αα :α:TypeType) whereType:Type 1x :x:{α : Type} → Point α → ααα:Typey :y:{α : Type} → Point α → αα derivingα:TypeRepr,Repr:Type u → Type uBEq defBEq:Type u → Type uPoint.map (Point.map:{α β : Type} → (α → β) → Point α → Point βf :f:α → βα →α:Typeβ) (β:Types :s:Point αPointPoint:Type → Typeα) :α:TypePointPoint:Type → Typeβ := { x :=β:Typeff:α → βs.s:Point αy, -- an example of something weird y :=y:{α : Type} → Point α → αff:α → βs.s:Point αx }x:{α : Type} → Point α → αinstance :instance:Functor PointFunctorFunctor:(Type → Type) → Type 1Point where map :=Point:Type → TypePoint.mapPoint.map:{α β : Type} → (α → β) → Point α → Point β(·+2) <$> ((·+2):Nat → NatPoint.mkPoint.mk:{α : Type} → α → α → Point α11:Nat2) -- { x := 4, y := 3 }2:Nat

This Point does something weird, when you `map`

it because it transposes the `x`

and `y`

coordinates
which is not what other people would expect from a `map`

function. In fact, it breaks the rules
as you will see below.

## What are the Functor laws?

Functors have two laws: the *identity* law, and the *composition* law. These laws express behaviors that
your functor instances should follow. If they don't, other programmers will be very confused at the
effect your instances have on their program.

The identity law says that if you "map" the identity function (`id`

) over your functor, the
resulting functor should be the same. A succinct way of showing this on a `List`

functor is:

deflist1 := [list1:List Nat1,1:Nat2,2:Nat3]3:Natid <$>id:{α : Type} → α → αlist1 ==list1:List Natlist1 -- truelist1:List Nat

Now let's try the same test on the `Point`

functor:

defp1 :p1:Point NatPointPoint:Type → TypeNat := (Nat:TypePoint.mkPoint.mk:{α : Type} → α → α → Point α11:Nat2)2:Natid <$>id:{α : Type} → α → αp1 ==p1:Point Natp1 -- falsep1:Point Nat

Oh, and look while the `List`

is behaving well, the `Point`

functor fails this identity test.

The *composition* law says that if you "map" two functions in succession over a functor, this
should be the same as "composing" the functions and simply mapping that one super-function over the
functor. In Lean you can compose two functions using `Function.comp f g`

(or the syntax `f ∘ g`

,
which you can type in VS code using `\o `

) and you will get the same results from both of these
showing that the composition law holds for `List Nat`

:

defdouble (double:Nat → Natx :x:NatNat) :=Nat:Typex +x:Natx defx:Natsquare (square:Nat → Natx :x:NatNat) :=Nat:Typex *x:Natxx:Natdouble <$> (double:Nat → Natsquare <$>square:Nat → Natlist1) -- [2, 8, 18]list1:List Nat(double <$> (double:Nat → Natsquare <$>square:Nat → Natlist1)) == ((list1:List Natdouble ∘double:Nat → Natsquare) <$>square:Nat → Natlist1) -- true -- ok, what about the Point class?list1:List Natdouble <$> (double:Nat → Natsquare <$>square:Nat → Natp1) -- { x := 2, y := 8 }p1:Point Nat(double ∘double:Nat → Natsquare) <$>square:Nat → Natp1 -- { x := 8, y := 2 }p1:Point Natdouble <$> (double:Nat → Natsquare <$>square:Nat → Natp1) == (p1:Point Natdouble ∘double:Nat → Natsquare) <$>square:Nat → Natp1 -- falsep1:Point Nat

Note that composition also fails on the bad `Point`

because the x/y transpose.

As you can see this bad `Point`

implementation violates both of the functor laws. In this case it
would not be a true functor. Its behavior would confuse any other programmers trying to use it. You
should take care to make sure that your instances make sense. Once you get a feel for these type
classes, the likelihood is that the instances you'll create will follow the laws.

You can also write a bad functor that passes one law but not the other like this:

defbad_option_map {bad_option_map:{α β : Type u} → (α → β) → Option α → Option βαα:Type uβ :β:Type uType u} : (Type u:Type (u + 1)α →α:Type uβ) →β:Type uOptionOption:Type u → Type uα →α:Type uOptionOption:Type u → Type uβ | _, _ =>β:Type unonenone:{α : Type u} → Option αinstance :instance:Functor OptionFunctorFunctor:(Type u_1 → Type u_1) → Type (u_1 + 1)Option where map :=Option:Type u_1 → Type u_1bad_option_map defbad_option_map:{α β : Type u_1} → (α → β) → Option α → Option βt1 :t1:Option NatOptionOption:Type → TypeNat :=Nat:Typesomesome:{α : Type} → α → Option α1010:Natid <$>id:{α : Type} → α → αt1 ==t1:Option Natt1 -- falset1:Option Natdouble <$> (double:Nat → Natsquare <$>square:Nat → Natt1) == (t1:Option Natdouble ∘double:Nat → Natsquare) <$>square:Nat → Natt1 -- truet1:Option Nat

This fails the id law but obeys the composition law. Hopefully this explains the value of these laws, and you don't need to see any more bad examples!

## What are the Applicative Laws?

While functors have two laws, applicatives have four laws:

- Identity
- Homomorphism
- Interchange
- Composition

### Identity

`pure id <*> v = v`

Applying the identity function through an applicative structure should not change the underlying values or structure. For example:

instance :instance:Applicative ListApplicativeApplicative:(Type u_1 → Type u_1) → Type (u_1 + 1)List where pure :=List:Type u_1 → Type u_1List.pure seqList.pure:{α : Type u_1} → α → List αff:List (α✝ → β✝)x :=x:Unit → List α✝List.bindList.bind:{α β : Type u_1} → List α → (α → List β) → List βf funf:List (α✝ → β✝)y =>y:α✝ → β✝Functor.mapFunctor.map:{f : Type u_1 → Type u_1} → [self : Functor f] → {α β : Type u_1} → (α → β) → f α → f βy (y:α✝ → β✝xx:Unit → List α✝())():Unitpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αid <*> [id:{α : Type} → α → α1,1:Nat2,2:Nat3] -- [1, 2, 3]3:Nat

The `pure id`

statement here is wrapping the identity function in an applicative structure
so that you can apply that over the container `[1, 2, 3]`

using the Applicative `seq`

operation
which has the notation `<*>`

.

To prove this for all values `v`

and any applicative `m`

you can write this theorem:

example [example:∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m] [inst_1 : LawfulApplicative m] (v : m α), (Seq.seq (pure id) fun x => v) = vApplicativeApplicative:(Type u_1 → Type u_2) → Type (max (u_1 + 1) u_2)m] [m:Type u_1 → Type u_2LawfulApplicativeLawfulApplicative:(f : Type ?u.34052 → Type ?u.34051) → [inst : Applicative f] → Propm] (m:Type u_1 → Type u_2v :v:m αmm:Type u_1 → Type u_2α) :α:Type u_1purepure:{f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f αid <*>id:{α : Type u_1} → α → αv =v:m αv :=v:m αGoals accomplished! 🐙-- Goals accomplished 🎉Goals accomplished! 🐙

### Homomorphism

`pure f <*> pure x = pure (f x)`

Suppose you wrap a function and an object in `pure`

. You can then apply the wrapped function over the
wrapped object. Of course, you could also apply the normal function over the normal object, and then
wrap it in `pure`

. The homomorphism law states these results should be the same.

For example:

defx :=x:Nat1 def1:Natf :=f:Nat → Nat(· + 2)(· + 2):Nat → Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αf <*>f:Nat → Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αx = (x:Natpure (pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αff:Nat → Natx) :x:NatListList:Type → TypeNat) -- trueNat:Type

You should see a distinct pattern here. The overriding theme of almost all these laws is that these
`Applicative`

types should behave like normal containers. The `Applicative`

functions should not
have any side effects. All they should do is facilitate the wrapping, unwrapping, and transformation
of data contained in the container resulting in a new container that has the same structure.

### Interchange

`u <*> pure y = pure (. y) <*> u`

.

This law is is a little more complicated, so don't sweat it too much. It states that the order that
you wrap things shouldn't matter. One the left, you apply any applicative `u`

over a pure wrapped
object. On the right, you first wrap a function applying the object as an argument. Note that `(· y)`

is short hand for: `fun f => f y`

. Then you apply this to the first applicative `u`

. These
should be the same.

For example:

defy :=y:Nat4 def4:Natg :g:List (Nat → Nat)List (List:Type → TypeNat →Nat:TypeNat) := [Nat:Type(· + 2)](· + 2):Nat → Natg <*>g:List (Nat → Nat)purepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αy =y:Natpure (·pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αy) <*>y:Natg -- trueg:List (Nat → Nat)

You can prove this with the following theorem:

example [example:∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Applicative m] [inst_1 : LawfulApplicative m] (u : m (α → β)) (y : α), (Seq.seq u fun x => pure y) = Seq.seq (pure fun x => x y) fun x => uApplicativeApplicative:(Type u_1 → Type u_2) → Type (max (u_1 + 1) u_2)m] [m:Type u_1 → Type u_2LawfulApplicativeLawfulApplicative:(f : Type u_1 → Type u_2) → [inst : Applicative f] → Propm] (m:Type u_1 → Type u_2u :u:m (α → β)m (m:Type u_1 → Type u_2α →α:Type u_1β)) (β:Type u_1y :y:αα) :α:Type u_1u <*>u:m (α → β)purepure:{f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f αy =y:αpure (·pure:{f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f αy) <*>y:αu :=u:m (α → β)Goals accomplished! 🐙-- Goals accomplished 🎉Goals accomplished! 🐙

### Composition:

`u <*> v <*> w = u <*> (v <*> w)`

This final applicative law mimics the second functor law. It is a composition law. It states that function composition holds across applications within the applicative:

For example:

defu := [u:List Nat1,1:Nat2] def2:Natv := [v:List Nat3,3:Nat4] def4:Natw := [w:List Nat5,5:Nat6]6:Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f α(·+·+·) <*>(·+·+·):Nat → Nat → Nat → Natu <*>u:List Natv <*>v:List Natw -- [9, 10, 10, 11, 10, 11, 11, 12]w:List Natletgrouping :=grouping:List Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f α(·+·) <*>(·+·):Nat → Nat → Natv <*>v:List Natww:List Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f α(·+·) <*>(·+·):Nat → Nat → Natu <*>u:List Natgrouping -- [9, 10, 10, 11, 10, 11, 11, 12]grouping:List Nat

To test composition you see the separate grouping `(v <*> w)`

then that can be used in the outer
sequence `u <*> grouping`

to get the same final result `[9, 10, 10, 11, 10, 11, 11, 12]`

.

## What are the Monad Laws?

Monads have three laws:

- Left Identity
- Right Identity
- Associativity

### Left Identity

Identity laws for monads specify that `pure`

by itself shouldn't really change anything about the
structure or its values.

Left identity is `x >>= pure = x`

and is demonstrated by the following examples on a monadic `List`

:

instance :instance:Monad ListMonadMonad:(Type u_1 → Type u_1) → Type (u_1 + 1)List where pure :=List:Type u_1 → Type u_1List.pure bind :=List.pure:{α : Type u_1} → α → List αList.bind defList.bind:{α β : Type u_1} → List α → (α → List β) → List βa := [a:List String"apple","apple":String"orange"]"orange":Stringa >>=a:List Stringpure -- ["apple", "orange"]pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αa >>=a:List Stringpure =pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αa -- truea:List String

### Right Identity

Right identity is `pure x >>= f = f x`

and is demonstrated by the following example:

defh (h:Nat → Option Natx :x:NatNat) :Nat:TypeOptionOption:Type → TypeNat :=Nat:Typesome (some:{α : Type} → α → Option αx +x:Nat1) def1:Natz :=z:Nat55:Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αz >>=z:Nath -- some 6h:Nat → Option Nathh:Nat → Option Natz -- some 6z:Natpurepure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αz >>=z:Nath =h:Nat → Option Nathh:Nat → Option Natz -- truez:Nat

So in this example, with this specific `z`

and `h`

, you see that the rule holds true.

### Associativity

The associativity law is written as:

```
x >>= f >>= g = x >>= (λ x => f x >>= g)
```

where `(x : m α)`

and `(f : α → m β)`

and `(g : β → m γ)`

.

The associativity law is difficult to parse like some of the applicative laws, but what it is saying
is that if you change the grouping of `bind`

operations, you should still get the same result.
This law has a parallel structure to the other composition laws.

You can see this in action in the following rewrite of `runOptionFuncsBind`

from monads:

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 → NatrunOptionFuncsBind (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 FloatoptionFunc3 defoptionFunc3:Float → Option (List Nat)runOptionFuncsBindGrouped (runOptionFuncsBindGrouped:String → Option (List Nat)input :input:StringString) :String:TypeOption (Option:Type → TypeListList:Type → TypeNat) :=Nat:TypeoptionFunc1optionFunc1:String → Option Natinput >>= (λinput:Stringx =>x:NatoptionFunc2optionFunc2:Nat → Option Floatx >>=x:NatoptionFunc3)optionFunc3:Float → Option (List Nat)runOptionFuncsBindrunOptionFuncsBind:String → Option (List Nat)"big" -- some [9, 10]"big":StringrunOptionFuncsBindGroupedrunOptionFuncsBindGrouped:String → Option (List Nat)"big" -- some [9, 10]"big":String

Notice here we had to insert a `λ`

function just like the definition says: `(λ x => f x >>= g)`

.
This is because unlike applicatives, you can't resolve the structure of later operations without the
results of earlier operations quite as well because of the extra context monads provide. But you can
still group their later operations into composite functions taking their inputs from earlier on, and
the result should be the same.

## Summary

While these laws may be a bit difficult to understand just by looking at them, the good news is that most of the instances you'll make will naturally follow the laws so long as you keep it simple, so you shouldn't have to worry about them too much.

There are two main ideas from all the laws:

- Applying the identity or pure function should not change the underlying values or structure.
- It should not matter what order you group operations in. Another way to state this is function composition should hold across your structures.

Following these laws will ensure other programmers are not confused by the behavior of your new functors, applicatives and monads.