From ce1bf6732adaf699dd35d52a60abc9941c799c54 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Wed, 13 Nov 2024 02:23:21 +0900
Subject: [PATCH] =?UTF-8?q?LawfulFunctor=20=E3=82=92=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=99=E3=82=8B=20Fixes=20#1056?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Reference/TypeClass/Functor.lean          |  4 +-
 .../Reference/TypeClass/LawfulFunctor.lean    | 43 +++++++++++++++++++
 booksrc/SUMMARY.md                            |  1 +
 3 files changed, 46 insertions(+), 2 deletions(-)
 create mode 100644 LeanByExample/Reference/TypeClass/LawfulFunctor.lean

diff --git a/LeanByExample/Reference/TypeClass/Functor.lean b/LeanByExample/Reference/TypeClass/Functor.lean
index e838585..e5e22e0 100644
--- a/LeanByExample/Reference/TypeClass/Functor.lean
+++ b/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
diff --git a/LeanByExample/Reference/TypeClass/LawfulFunctor.lean b/LeanByExample/Reference/TypeClass/LawfulFunctor.lean
new file mode 100644
index 0000000..326de58
--- /dev/null
+++ b/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 --#
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 851bb04..8339e4e 100644
--- a/booksrc/SUMMARY.md
+++ b/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)