Lean 语言参考手册

18.1. 定律🔗

仅有类型适当的 map、pure、seq 和 bind 运算，还不足以真正构成函子、应用函子或单子。 这些运算还必须满足某些公理，它们通常称为该类型类的定律。

对于函子，map 操作必须保持恒等函数和函数复合。换言之，给定一个声称为 Functor 的 f，对所有 x​:​f α：

  • id <$> x = x；并且

  • 对所有函数 g 和 h，有 (h ∘ g) <$> x = h <$> g <$> x。

违反这些假设的实例可能产生非常出人意料的行为！ 此外，因为 Functor 包含 mapConst，以便实例提供更高效的实现，所以合法函子的 mapConst 应当等价于其默认实现。

Lean 标准库不要求每个 Functor 实例都提供这些性质的证明。 尽管如此，如果某个实例违反了它们，就应将其视为缺陷。 需要这些性质的证明时，可以使用类型为 LawfulFunctor f 的实例隐式参数。 类型类 LawfulFunctor 包含所需的证明。

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

满足函子定律的函子。

Functor 类型类包含函子的运算，但不要求实例证明它们满足函子定律。LawfulFunctor 实例 包含这些定律成立的证明。由于 Functor 实例可以为 mapConst 提供优化实现， LawfulFunctor 实例还必须证明该优化实现等价于标准实现。

实例构造子

LawfulFunctor.mk.{u, v}

方法

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

mapConst 的实现等价于默认实现。

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

map 的实现保持恒等函数。

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

map 的实现保持函数复合。

除了要证明可能经过优化的 SeqLeft.seqLeft 和 SeqRight.seqRight 操作等价于其默认实现之外，应用函子 f 还必须满足四条定律。

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

满足应用函子定律的应用函子。

Applicative 类型类包含应用函子的运算，但不要求实例证明它们满足应用函子定律。 LawfulApplicative 实例包含这些定律成立的证明。

由于 Applicative 实例可以为 seqLeft 和 seqRight 提供优化实现， LawfulApplicative 实例还必须证明这些优化实现等价于标准实现。

实例构造子

LawfulApplicative.mk.{u, v}

扩展

方法

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

继承自父结构。

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

seqLeft 等价于默认实现。

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

seqRight 等价于默认实现。

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

pure 出现在 seq 之前等价于 Functor.map。

这意味着紧邻 seq 之前出现的 pure 确实是纯的。

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

将函数映射到 pure 的结果上，等价于在 pure 之下应用该函数。

这意味着相对于 Functor.map，pure 确实是纯的。

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

pure 出现在 seq 之后等价于 Functor.map。

这意味着紧邻 seq 之后出现的 pure 确实是纯的。

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

seq 满足结合律。

在保持计算顺序不变的前提下改变 seq 调用的嵌套，会得到等价的计算。这意味着 seq 除了安排顺序之外不做任何额外工作。

单子定律规定：pure 后接 bind 应等价于函数应用（即 pure 没有任何效应）；bind 后接用 pure 包裹的函数应用，应等价于 map；并且 bind 满足结合律。

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

合法单子是满足某种行为规范的单子。所有 Monad 实例都应满足这些定律，但并非所有实现都 必须给出证明。

LawfulMonad.mk' 是一个替代构造器，它为许多字段提供了有用的默认值。

实例构造子

LawfulMonad.mk.{u, v}

扩展

方法

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

bind 后接与函数复合的 pure，等价于函子映射。

这意味着 bind 之后的 pure 确实是纯的，不会产生副作用。

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

bind 后接函子映射，等价于 Applicative 的顺序执行。

这意味着 Monad 与 Applicative 的副作用顺序执行方式相同。

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

pure 后接 bind，等价于函数应用。

这意味着 bind 之前的 pure 确实是纯的，不会产生副作用。

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

bind 满足结合律。

在保持计算顺序不变的前提下改变 bind 调用的嵌套，会得到等价的计算。这意味着 bind 除了依赖数据地安排顺序之外不做更多工作。

🔗定理
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

常见情况下具有更多可使用默认值字段的 LawfulMonad 替代构造器。