18.1. 法律🔗

拥有具有适当类型的 map、pure、seq 和 bind 运算符并不足以拥有函子、应用函子或 monad。这些运算符还必须满足某些公理，这些公理通常称为类型类的 laws。

对于函子，map 操作必须保留标识和函数组合。换句话说，给定一个所谓的 Functor f，对于所有 x:f α：

id <$> x = x，和
适用于 g 和 h、(h ∘ g) <$> x = h <$> g <$> x 的所有功能。

违反这些假设的实例可能会非常令人惊讶！此外，由于 Functor 包括 mapConst 以使实例能够提供更高效的实现，因此合法函子的 mapConst 应与其默认实现等效。

Lean 标准库不需要在 Functor 的每个实例中提供这些属性的证明。尽管如此，如果一个实例违反了它们，那么它应该被视为一个错误。当需要证明这些属性时，可以使用 LawfulFunctor f 类型的实例隐式参数。 LawfulFunctor 类包括必要的证明。

type class

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

A functor satisfies the functor laws.

The Functor class contains the operations of a functor, but does not require that instances prove they satisfy the laws of a functor. A LawfulFunctor instance includes proofs that the laws are satisfied. Because Functor instances may provide optimized implementations of mapConst, LawfulFunctor instances must also prove that the optimized implementation is equivalent to the standard implementation.

Instance Constructor

LawfulFunctor.mk.{u, v}

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

The mapConst implementation is equivalent to the default implementation.

id_map : ∀ {α : Type u} (x : f α), id <$> x = x

The map implementation preserves identity.

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

The map implementation preserves function composition.

除了证明潜在优化的 SeqLeft.seqLeft 和 SeqRight.seqRight 操作与其默认实现等效之外，应用函子 f 还必须满足四个定律。

type class

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

An applicative functor satisfies the laws of an applicative functor.

The Applicative class contains the operations of an applicative functor, but does not require that instances prove they satisfy the laws of an applicative functor. A LawfulApplicative instance includes proofs that the laws are satisfied.

Because Applicative instances may provide optimized implementations of seqLeft and seqRight, LawfulApplicative instances must also prove that the optimized implementation is equivalent to the standard implementation.

Instance Constructor

LawfulApplicative.mk.{u, v}

Extends

LawfulFunctor f

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

Inherited from

LawfulFunctor f

id_map : ∀ {α : Type u} (x : f α), id <$> x = x

Inherited from

LawfulFunctor f

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

Inherited from

LawfulFunctor f

seqLeft_eq : ∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y

seqLeft is equivalent to the default implementation.

seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y

seqRight is equivalent to the default implementation.

pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x

pure before seq is equivalent to Functor.map.

This means that pure really is pure when occurring immediately prior to seq.

map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

Mapping a function over the result of pure is equivalent to applying the function under pure.

This means that pure really is pure with respect to Functor.map.

seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

pure after seq is equivalent to Functor.map.

This means that pure really is pure when occurring just after seq.

seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

seq is associative.

Changing the nesting of seq calls while maintaining the order of computations results in an equivalent computation. This means that seq is not doing any more than sequencing.

monad law 指定 pure 后跟 bind 应等效于函数应用程序（即 pure 没有效果），bind 后跟 pure 围绕函数应用程序等效于 map，并且bind 是结合的。

type class

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

Lawful monads are those that satisfy a certain behavioral specification. While all instances of Monad should satisfy these laws, not all implementations are required to prove this.

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

Instance Constructor

LawfulMonad.mk.{u, v}

Extends

LawfulApplicative m

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

Inherited from

LawfulApplicative m

id_map : ∀ {α : Type u} (x : m α), id <$> x = x

Inherited from

LawfulApplicative m

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x

Inherited from

LawfulApplicative m

seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y

Inherited from

LawfulApplicative m

seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y

Inherited from

LawfulApplicative m

pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x

Inherited from

LawfulApplicative m

map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

Inherited from

LawfulApplicative m

seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

Inherited from

LawfulApplicative m

seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

Inherited from

LawfulApplicative m

bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x

A bind followed by pure composed with a function is equivalent to a functorial map.

This means that pure really is pure after a bind and has no effects.

bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

A bind followed by a functorial map is equivalent to Applicative sequencing.

This means that the effect sequencing from Monad and Applicative are the same.

pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

pure followed by bind is equivalent to function application.

This means that pure really is pure before a bind and has no effects.

bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

bind is associative.

Changing the nesting of bind calls while maintaining the order of computations results in an equivalent computation. This means that bind is not doing more than data-dependent sequencing.

theorem

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

18.1.	法律
18.2.	提升单子
18.3.	句法
18.4.	API 参考
18.5.	单子的种类