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:

structure 
Point: Type → Type
Point (
α: Type
α : 
Type: Type 1
Type) where
  
x: {α : Type} → Point α → α
x : 
α: Type
α
  
y: {α : Type} → Point α → α
y : 
α: Type
α
  deriving 
Repr: Type u → Type u
Repr, 
BEq: Type u → Type u
BEq

def 
Point.map: {α β : Type} → (α → β) → Point α → Point β
Point.map (
f: α → β
f : 
α: Type
α → 
β: Type
β) (
s: Point α
s : 
Point: Type → Type
Point 
α: Type
α) : 
Point: Type → Type
Point 
β: Type
β :=
  { x := 
f: α → β
f 
s: Point α
s.
y: {α : Type} → Point α → α
y,  -- an example of something weird
    y := 
f: α → β
f 
s: Point α
s.
x: {α : Type} → Point α → α
x }

instance: Functor Point
instance : 
Functor: (Type → Type) → Type 1
Functor 
Point: Type → Type
Point where
  map := 
Point.map: {α β : Type} → (α → β) → Point α → Point β
Point.map

#eval
{ x := 4, y := 3 }
 
(·+2): Nat → Nat
(·+2) <$> (
Point.mk: {α : Type} → α → α → Point α
Point.mk 
1: Nat
1 
2: Nat
2) -- { x := 4, y := 3 }

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:

def 
list1: List Nat
list1 := [
1: Nat
1,
2: Nat
2,
3: Nat
3]

#eval
true
 
id: {α : Type} → α → α
id <$> 
list1: List Nat
list1 == 
list1: List Nat
list1 -- true

Now let's try the same test on the Point functor:

def 
p1: Point Nat
p1 : 
Point: Type → Type
Point 
Nat: Type
Nat := (
Point.mk: {α : Type} → α → α → Point α
Point.mk 
1: Nat
1 
2: Nat
2)

#eval
false
 
id: {α : Type} → α → α
id <$> 
p1: Point Nat
p1 == 
p1: Point Nat
p1 -- false

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:

def 
double: Nat → Nat
double (
x: Nat
x : 
Nat: Type
Nat) := 
x: Nat
x + 
x: Nat
x
def 
square: Nat → Nat
square (
x: Nat
x : 
Nat: Type
Nat) := 
x: Nat
x * 
x: Nat
x

#eval
[2, 8, 18]
 
double: Nat → Nat
double <$> (
square: Nat → Nat
square <$> 
list1: List Nat
list1) -- [2, 8, 18]

#eval
true
 (
double: Nat → Nat
double <$> (
square: Nat → Nat
square <$> 
list1: List Nat
list1)) == ((
double: Nat → Nat
double ∘ 
square: Nat → Nat
square) <$> 
list1: List Nat
list1) -- true

-- ok, what about the Point class?
#eval
{ x := 2, y := 8 }
 
double: Nat → Nat
double <$> (
square: Nat → Nat
square <$> 
p1: Point Nat
p1) -- { x := 2, y := 8 }
#eval
{ x := 8, y := 2 }
 (
double: Nat → Nat
double ∘ 
square: Nat → Nat
square) <$> 
p1: Point Nat
p1   -- { x := 8, y := 2 }

#eval
false
 
double: Nat → Nat
double <$> (
square: Nat → Nat
square <$> 
p1: Point Nat
p1) == (
double: Nat → Nat
double ∘ 
square: Nat → Nat
square) <$> 
p1: Point Nat
p1  -- false

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:

def 
bad_option_map: {α β : Type u} → (α → β) → Option α → Option β
bad_option_map {
α: Type u
α 
β: Type u
β : 
Type u: Type (u + 1)
Type u} : (
α: Type u
α → 
β: Type u
β) → 
Option: Type u → Type u
Option 
α: Type u
α → 
Option: Type u → Type u
Option 
β: Type u
β
  | _, _ => 
none: {α : Type u} → Option α
none

instance: Functor Option
instance : 
Functor: (Type u_1 → Type u_1) → Type (u_1 + 1)
Functor 
Option: Type u_1 → Type u_1
Option where
    map := 
bad_option_map: {α β : Type u_1} → (α → β) → Option α → Option β
bad_option_map

def 
t1: Option Nat
t1 : 
Option: Type → Type
Option 
Nat: Type
Nat := 
some: {α : Type} → α → Option α
some 
10: Nat
10

#eval
false
 
id: {α : Type} → α → α
id <$> 
t1: Option Nat
t1 == 
t1: Option Nat
t1 -- false
#eval
true
 
double: Nat → Nat
double <$> (
square: Nat → Nat
square <$> 
t1: Option Nat
t1) == (
double: Nat → Nat
double ∘ 
square: Nat → Nat
square) <$> 
t1: Option Nat
t1  -- true

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: Applicative List
instance : 
Applicative: (Type u_1 → Type u_1) → Type (u_1 + 1)
Applicative 
List: Type u_1 → Type u_1
List where
  pure := 
List.pure: {α : Type u_1} → α → List α
List.pure
  seq 
f: List (α✝ → β✝)
f 
x: Unit → List α✝
x := 
List.bind: {α β : Type u_1} → List α → (α → List β) → List β
List.bind 
f: List (α✝ → β✝)
f fun 
y: α✝ → β✝
y => 
Functor.map: {f : Type u_1 → Type u_1} → [self : Functor f] → {α β : Type u_1} → (α → β) → f α → f β
Functor.map 
y: α✝ → β✝
y (
x: Unit → List α✝
x 
(): Unit
())

#eval
[1, 2, 3]
 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
id: {α : Type} → α → α
id <*> [
1: Nat
1, 
2: Nat
2, 
3: Nat
3]  -- [1, 2, 3]

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: ∀ {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) = v
example [
Applicative: (Type u_1 → Type u_2) → Type (max (u_1 + 1) u_2)
Applicative 
m: Type u_1 → Type u_2
m] [
LawfulApplicative: (f : Type u_1 → Type u_2) → [inst : Applicative f] → Prop
LawfulApplicative 
m: Type u_1 → Type u_2
m] (
v: m α
v : 
m: Type u_1 → Type u_2
m 
α: Type u_1
α) :
  
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
id: {α : Type u_1} → α → α
id <*> 
v: m α
v = 
v: m α
v :=
  by
Goals accomplished! 🐙 simp
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:

def x := 1
def f := (· + 2)

#eval
true
 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
f: Nat → Nat
f <*> 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
x: Nat
x = (
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (
f: Nat → Nat
f 
x: Nat
x) : 
List: Type → Type
List 
Nat: Type
Nat) -- true

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:

def 
y: Nat
y := 
4: Nat
4
def 
g: List (Nat → Nat)
g : 
List: Type → Type
List (
Nat: Type
Nat → 
Nat: Type
Nat) := [
(· + 2): Nat → Nat
(· + 2)]

#eval
true
 
g: List (Nat → Nat)
g <*> 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
y: Nat
y = 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (· 
y: Nat
y) <*> 
g: List (Nat → Nat)
g      -- true

You can prove this with the following theorem:

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 => u
example [
Applicative: (Type ?u.4169 → Type ?u.4168) → Type (max (?u.4169 + 1) ?u.4168)
Applicative 
m: Type u_1 → Type u_2
m] [
LawfulApplicative: (f : Type u_1 → Type u_2) → [inst : Applicative f] → Prop
LawfulApplicative 
m: Type u_1 → Type u_2
m] (
u: m (α → β)
u : 
m: Type u_1 → Type u_2
m (
α: Type u_1
α → 
β: Type u_1
β)) (
y: α
y : 
α: Type u_1
α) :
  
u: m (α → β)
u <*> 
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
y: α
y = 
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure (· 
y: α
y) <*> 
u: m (α → β)
u :=
  by
Goals accomplished! 🐙 simp [
pure_seq: ∀ {f : Type ?u.4398 → Type ?u.4397} [inst : Applicative f] [self : LawfulApplicative f] {α β : Type ?u.4398} (g : α → β)
  (x : f α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
pure_seq]
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:

def u := [1, 2]
def v := [3, 4]
def w := [5, 6]

#eval
[9, 10, 10, 11, 10, 11, 11, 12]
 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
(·+·+·): Nat → Nat → Nat → Nat
(·+·+·) <*> 
u: List Nat
u <*> 
v: List Nat
v <*> 
w: List Nat
w
-- [9, 10, 10, 11, 10, 11, 11, 12]

#eval
[9, 10, 10, 11, 10, 11, 11, 12]
 let 
grouping: List Nat
grouping := 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
(·+·): Nat → Nat → Nat
(·+·) <*> 
v: List Nat
v <*> 
w: List Nat
w
      
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
(·+·): Nat → Nat → Nat
(·+·) <*> 
u: List Nat
u <*> 
grouping: List Nat
grouping
-- [9, 10, 10, 11, 10, 11, 11, 12]

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

def 
a: List String
a := [
"apple": String
"apple", 
"orange": String
"orange"]

#eval
["apple", "orange"]
 
a: List String
a >>= 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure      -- ["apple", "orange"]

#eval
true
 
a: List String
a >>= 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure = 
a: List String
a  -- true

Right Identity

Right identity is pure x >>= f = f x and is demonstrated by the following example:

def 
h: Nat → Option Nat
h (
x: Nat
x : 
Nat: Type
Nat) : 
Option: Type → Type
Option 
Nat: Type
Nat :=  
some: {α : Type} → α → Option α
some (
x: Nat
x + 
1: Nat
1)
def 
z: Nat
z := 
5: Nat
5

#eval
some 6
 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
z: Nat
z >>= 
h: Nat → Option Nat
h                  -- some 6
#eval
some 6
 
h: Nat → Option Nat
h 
z: Nat
z                           -- some 6

#eval
true
 
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
z: Nat
z >>= 
h: Nat → Option Nat
h = 
h: Nat → Option Nat
h 
z: Nat
z            -- true

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:

def 
optionFunc1: String → Option Nat
optionFunc1 : 
String: Type
String -> 
Option: Type → Type
Option 
Nat: Type
Nat
  | 
"": String
"" => 
none: {α : Type} → Option α
none
  | 
str: String
str => 
some: {α : Type} → α → Option α
some 
str: String
str.
length: String → Nat
length

def 
optionFunc2: Nat → Option Float
optionFunc2 (
i: Nat
i : 
Nat: Type
Nat) : 
Option: Type → Type
Option 
Float: Type
Float :=
  if 
i: Nat
i % 
2: Nat
2 == 
0: Nat
0 then 
none: {α : Type} → Option α
none else 
some: {α : Type} → α → Option α
some (
i: Nat
i.
toFloat: Nat → Float
toFloat * 
3.14159: Float
3.14159)

def 
optionFunc3: Float → Option (List Nat)
optionFunc3 (
f: Float
f : 
Float: Type
Float) : 
Option: Type → Type
Option (
List: Type → Type
List 
Nat: Type
Nat) :=
  if 
f: Float
f > 
15.0: Float
15.0 then 
none: {α : Type} → Option α
none else 
some: {α : Type} → α → Option α
some [
f: Float
f.
floor: Float → Float
floor.
toUInt32: Float → UInt32
toUInt32.
toNat: UInt32 → Nat
toNat, 
f: Float
f.
ceil: Float → Float
ceil.
toUInt32: Float → UInt32
toUInt32.
toNat: UInt32 → Nat
toNat]


def 
runOptionFuncsBind: String → Option (List Nat)
runOptionFuncsBind (
input: String
input : 
String: Type
String) : 
Option: Type → Type
Option (
List: Type → Type
List 
Nat: Type
Nat) :=
   
optionFunc1: String → Option Nat
optionFunc1 
input: String
input >>= 
optionFunc2: Nat → Option Float
optionFunc2 >>= 
optionFunc3: Float → Option (List Nat)
optionFunc3

def 
runOptionFuncsBindGrouped: String → Option (List Nat)
runOptionFuncsBindGrouped (
input: String
input : 
String: Type
String) : 
Option: Type → Type
Option (
List: Type → Type
List 
Nat: Type
Nat) :=
   
optionFunc1: String → Option Nat
optionFunc1 
input: String
input >>= (λ 
x: Nat
x => 
optionFunc2: Nat → Option Float
optionFunc2 
x: Nat
x >>= 
optionFunc3: Float → Option (List Nat)
optionFunc3)

#eval
some [9, 10]
 
runOptionFuncsBind: String → Option (List Nat)
runOptionFuncsBind 
"big": String
"big"        -- some [9, 10]
#eval
some [9, 10]
 
runOptionFuncsBindGrouped: String → Option (List Nat)
runOptionFuncsBindGrouped 
"big": String
"big" -- some [9, 10]

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:

1. Applying the identity or pure function should not change the underlying values or structure.
2. 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.