8.1. 規則（Laws）🔗

演算子 map ・ pure ・ seq ・ bind が適切な型を持っているだけでは、関手・アプリカティブ関手・モナドを持つには十分ではありません。これらの演算子はさらに特定の公理を満たす必要があり、これはしばしば型クラスの規則（law）と呼ばれます。

関手の場合、 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

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

最適化される可能性のある SeqLeft.seqLeft と SeqRight.seqRight の操作がデフォルト実装と同等であることを証明することに加え、アプリカティブ関手 f は4つの規則を満たさなければなりません。

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

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

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

モナド則（monad laws）では、 pure の後に bind が続いたものは関数適用と同等であること（つまり pure は何の作用も持たない）、関数適用に対して bind の後に pure が続いたものは map と同等であること、 bind が結合的であることを指定します。

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

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

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.