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.

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

The Functor typeclass only contains the operations of a functor. LawfulFunctor further asserts that these operations satisfy the laws of a functor, including the preservation of the identity and composition laws:

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

Instance Constructor

LawfulFunctor.mk.{u, v}

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
id_map : ∀ {α : Type u} (x : f α), id <$> x = x
comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (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.

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

The Applicative typeclass only contains the operations of an applicative functor. LawfulApplicative further asserts that these operations satisfy the laws of an applicative functor:

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

Instance Constructor

LawfulApplicative.mk.{u, v}

Extends

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
Inherited from
  1. LawfulFunctor f
id_map : ∀ {α : Type u} (x : f α), id <$> x = x
Inherited from
  1. LawfulFunctor f
comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x
Inherited from
  1. LawfulFunctor f
seqLeft_eq : ∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y
seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y
pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

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.

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

The Monad typeclass only contains the operations of a monad. LawfulMonad further asserts that these operations satisfy the laws of a monad, including associativity and identity laws for bind:

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

LawfulMonad.mk' is an alternative constructor containing useful defaults for many fields.

Instance Constructor

LawfulMonad.mk.{u, v}

Extends

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
Inherited from
  1. LawfulApplicative m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
Inherited from
  1. LawfulApplicative m
comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x
Inherited from
  1. LawfulApplicative m
seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y
Inherited from
  1. LawfulApplicative m
seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y
Inherited from
  1. LawfulApplicative m
pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x
Inherited from
  1. LawfulApplicative m
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
Inherited from
  1. LawfulApplicative m
seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g
Inherited from
  1. LawfulApplicative m
seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
Inherited from
  1. LawfulApplicative m
bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x
bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> 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
🔗
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 = do
        let a ← x
        let _ ← y
        pure a := by
    intros; rfl)
  (seqRight_eq :
    ∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y := by
    intros; rfl)
  (bind_pure_comp :
    ∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x := by
    intros; rfl)
  (bind_map :
    ∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x := by
    intros; rfl) :
  LawfulMonad m

An alternative constructor for LawfulMonad which has more defaultable fields in the common case.