7.1. Laws🔗

Having map, pure, seq, and bind operators with the appropriate types is not really sufficient to have a functor, applicative functor, or monad. These operators must additionally satisfy certain axioms, which are often called the laws of the type class.

For a functor, the map operation must preserve identity and function composition. In other words, given a purported Functor f, for all x​:​f α:

• id <$> x = x, and

• for all function g and h, (h ∘ g) <$> x = h <$> g <$> x.

Instances that violate these assumptions can be very surprising! Additionally, because Functor includes mapConst to enable instances to provide a more efficient implementation, a lawful functor's mapConst should be equivalent to its default implementation.

The Lean standard library does not require profs of these properties in every instance of Functor. Nonetheless, if an instance violates them, then it should be considered a bug. When proofs of these properties are necessary, an instance implicit parameter of type LawfulFunctor f can be used. The LawfulFunctor class includes the necessary proofs.

LawfulFunctor.{u, v} (f : Type u → Type v)
    [Functor f] : Prop

id <$> x = x
(h ∘ g) <$> x = h <$> g <$> x

In addition to proving that the potentially-optimized SeqLeft.seqLeft and SeqRight.seqRight operations are equivalent to their default implementations, Applicative functors f must satisfy four laws.

LawfulApplicative.{u, v} (f : Type u → Type v)
    [Applicative f] : Prop

pure id <*> v = v
pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure (· y) <*> u

The monad laws specify that pure followed by bind should be equivalent to function application (that is, pure has no effects), that bind followed by pure around a function application is equivalent to map, and that bind is associative.

LawfulMonad.{u, v} (m : Type u → Type v)
    [Monad m] : Prop

pure x >>= f = f x
x >>= pure = x
x >>= f >>= g = x >>= (fun x => f x >>= g)

LawfulMonad.mk'.{u, v} (m : Type u → Type v)
  [Monad m]
  (id_map :
    ∀ {α : Type u} (x : m α), id <$> x = x)
  (pure_bind :
    ∀ {α β : Type u} (x : α) (f : α → m β),
      pure x >>= f = f x)
  (bind_assoc :
    ∀ {α β γ : Type u} (x : m α) (f : α → m β)
      (g : β → m γ),
      x >>= f >>= g = x >>= fun x => f x >>= g)
  (map_const :
    ∀ {α β : Type u} (x : α) (y : m β),
      Functor.mapConst x y =
        Function.const β x <$> y := by
    intros; rfl)
  (seqLeft_eq :
    ∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = doA
        let a ← x
        let _ ← y
        pure a := by
    intros; rfl)
  (seqRight_eq :
    ∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = doA
        let _ ← x
        y := by
    intros; rfl)
  (bind_pure_comp :
    ∀ {α β : Type u} (f : α → β) (x : m α),
      (doA
          let y ← x
          pure (f y)) =
        f <$> x := by
    intros; rfl)
  (bind_map :
    ∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (doA
          let x_1 ← f
          x_1 <$> x) =
        f <*> x := by
    intros; rfl) :
  LawfulMonad m