Functor 型クラスを紹介する

LeanByExample/Reference/TypeClass/Functor.lean

@@ -0,0 +1,60 @@
+/- # Functor
+
+`Functor` は圏論における関手(functor)という概念からその名がある型クラスで、非常に雑な表現をすると、この型クラスを実装した型は「値を包んでいる」ものとして扱うことができます。
+
+より詳細には、`f : Type u → Type v` に対して `Functor` はおおむね次のように定義されています。(実際の定義とは異なります)
+-/
+namespace Hidden --#
+--#--
+/--
+info: class Functor.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+number of parameters: 1
+constructor:
+Functor.mk : {f : Type u → Type v} →
+  ({α β : Type u} → (α → β) → f α → f β) → ({α β : Type u} → α → f β → f α) → Functor f
+fields:
+map : {α β : Type u} → (α → β) → f α → f β
+mapConst : {α β : Type u} → α → f β → f α
+-/
+#guard_msgs in #print Functor
+--#--
+
+universe u v
+
+/-- 関手 -/
+class Functor (f : Type u → Type v) : Type (max (u+1) v) where
+  /-- 関数 `g : α → β` を `g* : f α → f β` に変換する -/
+  map : {α β : Type u} → (α → β) → f α → f β
+
+end Hidden --#
+/- つまり、`Functor` のインスタンスは `map` メソッドが使用できます。これは型からわかるように、関数を関数に写す高階関数で、「`f` で包まれる前の関数」から「`f` で包まれた関数」を返します。 -/
+
+-- `f` は Functor であると仮定
+variable (f : Type → Type) [Functor f]
+
+-- 関数 `g : α → β` と `x : f α` が与えられたとする
+variable {α β : Type} (g : α → β)
+
+-- 高階関数を返す
+#check (Functor.map (f := f) g : f α → f β)
+
+/- `Functor.map` はよく使われる操作であるため、`<$>` という専用の記法が用意されています。-/
+
+example (x : f α) : Functor.map g x = g <$> x := rfl
+
+/- ## 典型的なインスタンス
+
+### List
+`Functor` 型クラスのインスタンスの典型的な例のひとつが `List` です。
+これにより「リストの各要素に関数を適用する」ための簡単な方法が提供されます。
+-/
+
+#guard [1, 2, 3, 4, 5].map (fun x => x * 2) = [2, 4, 6, 8, 10]
+
+/- ### Option
+`Option` も `Functor` 型クラスのインスタンスになっています。
+これにより「`x? : Option` が `some x` の場合に関数を適用し、`none` なら `none` を返す」という操作のための簡単な方法が提供されます。
+-/
+
+#guard (some 2).map (fun x => x * 2) = some 4
+#guard (none : Option Nat).map (fun x => x * 2) = none

booksrc/SUMMARY.md

@@ -84,6 +84,7 @@
   - [CoeFun: 関数型への強制](./Reference/TypeClass/CoeFun.md)
   - [CoeSort: 型宇宙への強制](./Reference/TypeClass/CoeSort.md)
   - [Decidable: 決定可能](./Reference/TypeClass/Decidable.md)
+  - [Functor: 関手](./Reference/TypeClass/Functor.md)
   - [GetElem: n番目の要素を取得](./Reference/TypeClass/GetElem.md)
   - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md)
   - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md)