Merge pull request #1088 from lean-ja/Seasawher/issue1056

LawfulFunctor を紹介する

LeanByExample/Reference/TypeClass/Functor.lean

@@ -2,7 +2,7 @@
 
 `Functor` は圏論における関手(functor)という概念からその名がある型クラスで、非常に雑な表現をすると、この型クラスを実装した型は「値を包んでいる」ものとして扱うことができます。
 
-より詳細には、`f : Type u → Type v` に対して `Functor` はおおむね次のように定義されています。(実際の定義とは異なります)
+より詳細には、`f : Type u → Type v` に対して `Functor` はおおむね次のように定義されています。(実際の定義には `mapConst` というフィールドがありますが、ここでは省略しました)
 -/
 namespace Hidden --#
 --#--
@@ -63,7 +63,7 @@ example (x : f α) : Functor.map g x = g <$> x := rfl
 
 `Functor` 型クラスのインスタンスには満たすべきルールがあります。
 このルールを破っていても `Functor` 型クラスのインスタンスにすることは可能ですが、API の使用者が予期せぬ挙動をするので避けるべきです。
-ルール込みで `Functor` 型クラスのインスタンスを定義するためには、`LawfulFunctor` 型クラスを使います。
+ルール込みで `Functor` 型クラスのインスタンスを定義するためには、[`LawfulFunctor`](./LawfulFunctor.md) 型クラスを使います。
 -/
 
 #check LawfulFunctor

LeanByExample/Reference/TypeClass/LawfulFunctor.lean

@@ -0,0 +1,43 @@
+/- # LawfulFunctor
+
+`LawfulFunctor` は、[`Functor`](./Functor.md) 型クラスにファンクタ則を満たすという条件を加えたものです。
+
+ファンクタ則とは、ファンクタ `F : Type u → Type u` が満たしているべきルールで、以下のようなものです。
+
+1. `Functor.map` は恒等関数を保存する。つまり `id <$> x = x` が成り立つ。
+2. `Functor.map` は関数合成を保存する。つまり `(f ∘ g) <$> x = f <$> (g <$> x)` が成り立つ。
+
+`LawfulFunctor` クラスは、これをほぼそのままコードに落とし込んだものとして、おおむね次のように定義されています。（実際の定義には `map_const` というフィールドがありますが、ここでは省略しました）
+-/
+--#--
+-- # LawfulFunctor の仕様変更を監視するためのコード
+/--
+info: class LawfulFunctor.{u, v} : (f : Type u → Type v) → [inst : Functor f] → Prop
+number of parameters: 2
+constructor:
+LawfulFunctor.mk : ∀ {f : Type u → Type v} [inst : Functor f],
+  (∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) →
+    (∀ {α : Type u} (x : f α), id <$> x = x) →
+      (∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) → LawfulFunctor f
+fields:
+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
+-/
+#guard_msgs in #print LawfulFunctor
+--#--
+
+namespace Hidden --#
+
+universe u v
+
+variable {α β γ : Type u}
+
+class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
+  /-- 恒等関数を保つ -/
+  id_map (x : f α) : id <$> x = x
+
+  /-- 合成を保つ -/
+  comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
+
+end Hidden --#

booksrc/SUMMARY.md

@@ -89,6 +89,7 @@
   - [HAdd: + のための記法クラス](./Reference/TypeClass/HAdd.md)
   - [HMul: * のための記法クラス](./Reference/TypeClass/HMul.md)
   - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md)
+  - [LawfulFunctor: ルール付きファンクタ](./Reference/TypeClass/LawfulFunctor.md)
   - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md)
   - [Repr: 表示方法を指定](./Reference/TypeClass/Repr.md)
   - [ToString: 文字列に変換](./Reference/TypeClass/ToString.md)