狠狠撸

狠狠撸Share a Scribd company logo
Scala 初心者が米田の補題を Scala で考えてみた
自己紹介
- 名前: 高瀬 和之 (たかせ かずゆき)
- 所属: Chatwork 株式会社 @大阪
- たぶん得意なこと:
- フロントエンド開発
(React / Redux / TypeScript)
- ティーチング
(アルゴリズム / 機械学習 / 数学
/ 組み込みシステム)
- ひとこと:
- Scala のイベントは 2 回目です ?
2
1. 本日の茶番パート
2. 圏論の公理
3. 函手,自然変換,函手圏
4. 米田の補題
アジェンダ
3
- この発表を聞いて得られるもの ???
- 圏論の中でも登竜門的なトピックである "米田の補題" を知ることができる
- "米田の補題" のプログラミング的位置づけを知ることができる
- ※ 後ろのセッションもないので、40 分をややオーバーするやも ?
本日の内容は、こちらの資料を見てもらうとよりわかりやすいです ?
/100005930379759/scala-hom-scala
関連資料のご紹介
4
01本日の茶番パート
「初心者とは?」の定義を決めました ? 
ある日のひとまく
6
02圏论の公理
圏論ことはじめ (1):対象と射
8
- 圏論の材料
- 対象 :点
- 射 :点から点を結ぶ矢印 (点と点の関連性を表す)
- ここまでの事実 ? なんか有向グラフっぽい
圏論ことはじめ (2):圏の例
- しりとりの圏 (対象:ひらがな,射:単語)
9
- 型と関数の圏 (対象:型,射:関数)
り ご ら ぱ と
りんご ごりら らっぱ ぱーせんと
String Int
Boolean
length
isEven
isCamelCase
圏論ことはじめ (3):Hom 集合
- 圏論では、ある対象 ● から別の対象 ● へ、複数の射が存在してもよい
- すなわち、射の集合を考えることができる ? Hom 集合と呼ぶ
- 対象 ● から対象 ● に関する Hom 集合 ? Hom(●, ●) と表す
- 下図の場合:
- Hom(●, ●) = { a, b, c, d, e }
- Hom(●, ●) = ?
10
a
e
d
b
c
ところで "公理" とは? ?
? 前提として認めてしまうルールのこと
圏論の公理 (1):合成射の存在,およびその可換性
12
- 合成射の存在
- f :A から B に向かう射
- g :B から C に向かう射
- これらが存在するとき、必ず A から C に向かう射 g ° f が存在するべき
- 可換性
- f と g をそれぞれ使って、A から C に至ること
- g ° f を 1 つ使って、A から C に至ること
- これらは等しくなるべき
f g
g ° f
A B C
NG な例 ?
13
- in Scala 圏:
- length :長さを調べる関数
- isEven :偶数であるかを調べる関数
- isCamelCase :キャメルケースであるかを調べる関数
- このとき、始点?終点となる対象 (型) はそれぞれ一致しているが、
可換性が無いため、isCamelCase は合成射になっていない!
length isEven
isCamelCase
String Int Boolean
OK な例 ??♂
14
- in Scala 圏:
- length :長さを調べる関数
- isEven :偶数であるかを調べる関数
- compose :与えられた 2 つの関数を、合成する高階関数
- このとき、compose で得られる射 (関数) は合成射の条件をみたす
length isEven
isEven compose length
String Int Boolean
f ∈ Hom(A, B) ? ?a ∈ Hom(X, A), ?b ∈ Hom(X, B), b = f ° a
- 合成射の存在より、A から B に向かう射が 1 つでも存在すれば、
必ず X から B に向かう射が存在する ? Hom(X, B) の存在がいえる
- Hom(X, A) の任意の要素を、Hom(X, B) のある要素に対応づける、
自明な関数 f ° _ を考えることができる
15
X
B
A
圏 C 集合の圏 Sets
Hom(X, A)
Hom(X, B)f
f ° _
※ 合成射が必ず存在
圏論の公理 (2):恒等射の存在,およびその単位律
16
- 恒等射の存在
- 任意の対象 X に関して、必ず X から X 自身に向かう射 idX
が存在するべき
- 単位律
- ?f:X から Y に向かう任意の射
- idX
° f , f ° idY
, および f のそれぞれが等しくなるべき
?f
idX
X
Y
X
Y
?f?f
idY
NG な例 ?
17
- in Scala 圏:
- increment ? 与えられた数を、1 増やして返す関数
- このとき、increment は Int から Int 自身に向かう射ではあるが、
恒等射になっていない! (例:increment ≠ increment ° increment)
Int
Int Int
increment
increment
increment
OK な例 ??♂
18
- in Scala 圏:
- identityInt
? 与えられた数を、そのまま返す関数
- このとき、identityInt
は恒等射の条件をみたす
∵ 任意の型 X からの任意の関数 f に対して、identityInt
° f = f
X
Int Int
identityInt
?f
?f
?X ∈ Obj(C), Hom(X, X) ≠ ?
- 恒等射の存在より、任意の対象 X には恒等射 idX
が必ず備わる
- よって、Hom(X, X) には少なくとも 1 つは射が含まれる
(※ この事実は米田の補題を考える上でも重要となる)
19
X X
圏 C
Hom(X, X)
?X, ?idX
?
idX
集合の圏 Sets
- …については割愛します ?
- ざっくり言うと:
- f :A から B に向かう射
- g :B から C に向かう射
- h :C から D に向かう射
- このとき、(h ° g) ° f と h ° (g ° f) は等しくなるべき
- そうなるように合成演算子 ° を考えてね,と捉えても良い
圏論の公理 (3):合成射の結合律
20
03函手,自然変换,函手圏
函手 / Functor
- ある圏から、グラフ構造をすべて抜き出す
- 別の圏にて、グラフ構造が一致する箇所に対応づける
- 対象と対象の対応関係,および射と射の対応関係,その 2 つ組と考えてもよい
22
圏 D圏 C
函手の記号的表現
- 圏 C から圏 D への函手を考える:
- 対象と対象の対応関係は、関数 F で表してみる
- 射と射の対応関係は、関数 mapF
で表してみる
(※ 数学的にはどちらも同じ記法で表してしまう場合が多いが、今回は分かりやすさを重視)
23
圏 D
X Y
f
F(X)
F(Y)
mapF
(f)
圏 C
考察:函手と合成射 (1)
- 合成射に関するグラフ表現を、函手で移すことを考える:
- 対象 A, B, C :対象 F(A), F(B), F(C) に対応
- 射 f, g :射 mapF
(f), mapF
(g) に対応
- 合成射 g ° f :射 mapF
(g ° f) に対応
24
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f)
- 合成射の存在より、mapF
(f) と mapF
(g) だけに着目しても、
これらの合成射 mapF
(g) ° mapF
(f) を考えることができる
- これは、mapF
(g ° f) とは別ものなのだろうか? ?
考察:函手と合成射 (2)
25
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f)
mapF
(g) ° mapF
(f)
函手の性質 (1):準同型性
- mapF
(g ° f) = mapF
(g) ° mapF
(f) となるように、函手は定めるべき
? このような性質を準同型性という
- 直感的には:
- ある圏の合成射が、別の圏でも合成射に移される,ということ
26
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f) = mapF
(g) ° mapF
(f)
函手の性質 (2):恒等射の保存
- mapF
(g ° f) = mapF
(g) ° mapF
(f) という等式の f, g に、それぞれ id*
を代入する
(※ 各射における始点?終点は、適宜調整してあるものとする)
- f に id*
を代入すると:
- mapF
(g ° id*
) = mapF
(g) = mapF
(g) ° mapF
(id*
)
∴ mapF
(g) = mapF
(g) ° mapF
(id*
) ? 右から合成しても影響がない
- g に id*
を代入すると:
- mapF
(id*
° f) = mapF
(f) = mapF
(id*
) ° mapF
(f)
∴ mapF
(f) = mapF
(id*
) ° mapF
(f) ? 左から合成しても影響がない
- これより、id*
を函手で移して得られる mapF
(id*
) は、恒等射の性質を保つ
(※ 厳密には、函手で移されていない射に対しても恒等射となることを保証するために、公理として与える)
27
函手 in Scala 圏
28
// F[_] が対象の対応関係を,map が射の対応関係を表す
trait EndoFunctor[F[_]] {
def map[X, Y](f: X => Y): F[X] => F[Y]
}
// 任意の函手の実装を、カインドで指定して取り出す (※ といいつつ Scala 圏には閉じているので、Endo = 自己)
object EndoFunctor[F[_]] {
def apply[F[_]](implicit instance: EndoFunctor[F]): EndoFunctor[F] =
instance
}
- ちなみに、圏と圏をまたぐ函手を Scala 圏で表現したい場合の例など:
- カインド C[X, Y] を用いて、C[X, Y] 部分に圏の情報をエンコード
- C[X, Y] 部分に射の情報をエンコード (始点と終点の 2 つ)
プログラミングする上での注意点!
EndoFunctor のインスタンスが実際に公理を満たすかは、実装による ?
- 圏 C から圏 D への函手を 2 つ考える:
- 1 つめは、F および mapF
で表すとする
- 2 つめは、G および mapG
で表すとする
- このとき、どちらの函手も圏 C を基点に考えている ? 関連性を見出せそう!?
考察:2 つの函手の関連性
30
圏 D
X Y
f
F(X) F(Y)
mapF
(f)
圏 C
G(X) G(Y)
mapG
(f)
- 圏 C の対象 X に対して、圏 D で F(X) と G(X) をグルーピングすることを考える
- 圏論の言葉でこれを表すには、各対象間に射 θX
を用意することが考えられる
- この θX
全体を、劣自然変換と呼ぶ
- ? "対象" のみに着目した、函手と函手の関連性
函手の弱い関連性
31
圏 D圏 C
[ F / mapF
]
[ G / mapG
]
θ●
θ●
θ●
- 各対象間に射 θX
を用意することに加えて、逆射 θX
-1
が存在する状況を考える
(※ θX
° θX
-1
,および θX
-1
° θX
が、それぞれ恒等射となること)
- なおかつ、各閉領域はそれぞれ可換だとする
- この θX
/ θX
-1
全体を、自然同型と呼ぶ
- ? 自然同型では、一方の函手から他方の函手を完全再現できる
函手の強い関連性
32
圏 D圏 C
θ●
/ θ●
-1
θ●
/ θ●
-1
θ●
/ θ●
-1
[ F / mapF
]
[ G / mapG
]
- 各対象間に射 θX
を用意する
- なおかつ、各閉領域はそれぞれ可換だとする
- この θX
全体を、自然変換と呼ぶ (θ : F ? G と表す)
- ? "対象" と "射" の双方に着目した、函手と函手の関連性 (ほどほどの関連性)
自然変換 / Natural Transformation
33
圏 D圏 C
θ●
θ●
θ●
 ? θ
[ F / mapF
]
[ G / mapG
]
自然変換の何がうれしいか? ?
? 自然同型よりも弱い仮定のもと、数学的 / 工学的に良い性質があること
- 自然変換そのものは、各対象間に射 θX
として与えられる
? すなわち、函手で移した任意の型ごとに、関数が備わっている ≒ 多相的な関数
- F[X] => G[X] を、型 X ごとにアドホックに実装すると辛い… (ほぼ不可能 ?)
? X は多相型として考えてしまう場合が多い
自然変換 in Scala 圏 (1)
35
Scala 圏Scala 圏
θA
θB
θC
A B C
G[A] G[B] G[C]
F[A] F[B] F[C]
自然変換 in Scala 圏 (2)
36
// F, G にそれぞれ函手を指定する
trait ~>[F[_], G[_]] {
def apply[X](x: F[X]): G[X] // ?X. F[X] => G[X] に相当
}
// Seq 函手の実装
implicit val seqFunctor = new EndoFunctor[Seq] {
def map[X, Y](f: X => Y): Seq[X] => Seq[Y] = _.map(f)
}
// Const 函手の実装 (常に特定の対象と射に移す函手)
type Const[X] = Int // Int で固定しているが、* -> * -> * というカインドだとより汎用的
implicit val constFunctor = new EndoFunctor[Const] {
def map[X, Y](f: X => Y): Const[X] => Const[Y] = x => x // 常に恒等射に移す
}
自然変換 in Scala 圏 (3)
37
// Seq 函手と Const 函手にまたがる自然変換の例
val length = new (Seq ~> Const) {
def apply[X](x: Seq[X]): Const[X] = x.length
}
// 函手で移す射
val f: Int => String = x => s"$x"
// 可換性の簡易テスト: lengthString
° mapSeq
(f) = mapConst
(f) ° lengthInt
println( length(EndoFunctor[Seq].map(f)(Seq(0, 1, 2))) )
println( EndoFunctor[Const].map(f)(length(Seq(0, 1, 2))) )
- ちなみに、多相関数として F[A] => G[A] を考えると、
自然と可換性も満たされる場合があります ? e.g. Parametricity
プログラミングする上での注意点!
~> のインスタンスが実際に可換性を満たすかは、実装による ? (再び
- 函手で移した構造全体を、まるごと 1 つで対象と捉える
- θX
全体を、まるごと 1 つで射と捉える
- このようにして得られる圏を、函手圏と呼ぶ
- 基点とした圏を C,函手で移す先の圏を D とする場合、函手圏は DC
で表す
函手圏 / Functor Category
39
F / mapF
函手圏 DC
G / mapG
θ = ?X. θX
圏 D圏 C
θ●
θ●
θ●
α●
γ●
α●
γ●
- 函手で移した構造全体に対して、複数の自然変換が存在する場合を考える
(※ 異なる自然変換同士で、可換性が満たされる必要はない)
- このとき、函手圏では 2 対象間に複数の射が存在することになる
- 下図の函手圏 DC
で Hom 集合を考えた場合:
- Hom( [ F / mapF
] , [ G / mapG
] ) = { α, β, γ }
函手圏における Hom 集合
40
F / mapF
函手圏 DC
G / mapG
α = ?X. αX
β = ?X. βX
γ = ?X. γX
圏 D
β●
β●
β●
α●
γ●
考察:そもそも自然変換はいくつも存在しうるのか? ?
41
// これとか…
val length1 = new (Seq ~> Const) {
def apply[X](x: Seq[X]): Const[X] = x.length
}
// あれとか…
val length2 = new (Seq ~> Const) {
def apply[X](x: Seq[X]): Const[X] = 0
}
// それとか,ね? ?
val length3 = new (Seq ~> Const) {
import scala.math.sqrt
def apply[X](x: Seq[X]): Const[X] = sqrt(x.length).toInt
}
04米田の补题
共変 Hom 函手
- 任意の圏から集合の圏 Sets への函手であって,
- 対象 * を対象 Hom(X, *) へ移し,
- 射 f を射 f ° _ へ移す,そんな函手
43
?a
?b
?f, b = f ° a
Hom(X, A)
Hom(X, B)
f ° _
X
B
A
圏 C 集合の圏 Sets
Hom 函手と集合値函手の自然変換
- 圏 C から集合の圏 Sets への函手を 2 つ考える:
- 1 つめは、対象 X を固定した Hom 函手 :[ Hom(X, *) / f → f ° _ ]
- 2 つめは、適当な集合値函手 :[ F / mapF
]
- このとき、自然変換 θ = ?A. θA
: Hom(X, A) → F(A)
44
集合の圏 Sets圏 C
θA
θB
θC
A B C
F(A) F(B) F(C)X
Hom(X, A) Hom(X, B) Hom(X, C)
Hom 函手と集合値函手の、函手圏における Hom 集合
- ここで、函手圏 SetsC
で Hom 集合を考えたいが、表記が紛らわしい ?
- ? 函手圏での Hom 集合は、Nat(   ,   ) のように表すとする
- 下図の函手圏 SetsC
で Hom 集合を考えた場合:
- Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF
] ) = { α, β, γ }
45
α●
γ●
α●
γ●
Hom(X, *) / f → f ° _
函手圏 SetsC
F / mapF
α = ?X. αX
β = ?X. βX
γ = ?X. γX
集合の圏 Sets
β●
β●
β●
α●
γ●
F(A) F(B) F(C)
Hom(X, A) Hom(X, B) Hom(X, C)
"米田の補題" の主張
- 函手圏 SetsC
での Hom 集合もまた、集合の圏 Sets の対象
- 圏 C で固定した対象 X を、函手で移した F(X) もまた、集合の圏 Sets の対象
- ここで:
- Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF
] ) ? F(X)
(※ これら 2 つの集合の要素が、それぞれ 1 対 1 に対応すること)
46
α●
γ●
α●
γ●
β●
β●
β●
α●
γ●
F(A) F(B) F(C)
Nat( [ Hom(X, *) / f → f ° _ ], [ F / mapF
] )
F(X)
※ 全単射が存在する
Hom(X, A) Hom(X, B) Hom(X, C)
集合の圏 Sets
? < ちょっと何言ってるか分からないっす
- …おっしゃる通り?,少し Scala 圏の表現に翻訳してみましょう:
- 集合 :"型" として捉えてみる
- 全単射 :"関数" と "逆関数" がある状態と捉えてみる
- その上で:
- F(X) :型 F[X] (※ 集合値の意味づけによる埋め込み)
- Hom(X, Y) :型 X => Y (※ 指数対象による埋め込み)
- Nat(   ,   ) :多相型 [A](X => A) => F[A]
(※ 多相型ラムダ計算の圏論的な意味づけによる埋め込み)
47
"米田の補題" の主張 in Scala 圏
- よって、米田の補題は次の 2 つが存在することを表す:
- 高階多相関数 lowerY = (f: [A](X => A) => F[A] ): F[X] { ... }
- 高階多相関数 liftY = (x: F[X] ): [A](X => A) => F[A] { ... }
- なおかつ:
- lowerY compose liftY == identityF[X]
- liftY compose lowerY == identity[A](X => A) => F[A]
48
米田の補題 in Scala 圏
49
// Hom 集合の型表現をカインドとして用意 (※ 本当は EndoFunctor のインスタンスも用意するべきだが、割愛)
type Hom[X, Y] = X => Y
// 函手 F で移された型の値を受け取って、自然変換を返す
def liftY[F[_], X](x: F[X])(implicit F: EndoFunctor[F]): Hom[X, *] ~> F =
new (Hom[X, *] ~> F) {
def apply[A](f: Hom[X, A]): F[A] = EndoFunctor[F].map(f)(x)
}
// 自然変換を受け取って、函手 F で移された型の値を返す
def lowerY[F[_], X](f: Hom[X, *] ~> F): F[X] =
f(x => x)
- Rank2Types は、呼び出し可能インスタンスで代用できるという知見を得た ?
- implicit parameter の探索範囲は、勝手に拡張されないという知見を得た ? (1 敗
実装の数学的な証明
※ まだ時間が大丈夫そうだったら説明するパート ???
固定した対象 X を中心とした、圏 C のセッティング
- 固定した対象 X と、射で接続された対象たちをピックアップ
- e.g. A, B, C, ...
- このとき X 自身にも、恒等射 idX
による接続がある
- 各対象間には複数の射が存在しうるので、対象ごとに f*
, g*
, h*
, ... と表してみる
- e.g. X から A に伸びる射であれば、fA
, gA
, hA
, ...
51
圏 C
A B
X
X C
idX
X と A に着目した自然変換 (1)
- X と A を接続する射は、fA
, gA
, hA
, ... と複数ある
- ? ここでは fA
をピックアップし、それぞれの函手で移す
- ここで、自然変換の満たす可換図式から、以下の 2 つが等価:
- mapF
(fA
) ° θX
- θA
° (fA
° _)
52
圏 C
A B
X
X C
集合の圏 Sets
θX
θA
F(X) F(A)
Hom(X, X) Hom(X, A)
idX
fA
° _
mapF
(fA
)
fA
, gA
, hA
, ...
X と A に着目した自然変換 (2)
- Hom(X, X) には idX
が含まれるので、試しに代入してみる:
- (mapF
(fA
) ° θX
)(idX
) = mapF
(fA
)(θX
(idX
))
- (θA
° (fA
° _))(idX
) = θA
(fA
° idX
)
= θA
(fA
)
- ∴ mapF
(fA
)(θX
(idX
)) = θA
(fA
)
- X から A への全ての射 fA
, gA
, hA
, ... に関して、同様な計算を行うと:
- mapF
(fA
)(θX
(idX
)) = θA
(fA
)
- mapF
(gA
)(θX
(idX
)) = θA
(gA
)
- mapF
(hA
)(θX
(idX
)) = θA
(hA
)
- ...
53
X と A に着目した自然変換 (3)
- ここで、  でハイライトした箇所は、圏 C や函手の構成から既知である:
- mapF
(fA
) (θX
( idX
)) = θA
( fA
)
- mapF
(gA
) (θX
( idX
)) = θA
( gA
)
- mapF
(hA
) (θX
( idX
)) = θA
( hA
)
- ...
- 仮に、θX
(idX
) の写像を、F(X) の要素から 1 つ選び、αX
とおくと:
- mapF
(fA
)(αX
) = θA
( fA
)
- mapF
(gA
)(αX
) = θA
( gA
)
- mapF
(hA
)(αX
) = θA
( hA
)
- ...
54
X と A に着目した自然変換 (4)
- したがって、下記の対応は、 Hom(X, A) から F(A) への関数 θA
を完全に定める
- mapF
(fA
)(αX
) = θA
( fA
)
- mapF
(gA
)(αX
) = θA
( gA
)
- mapF
(hA
)(αX
) = θA
( hA
)
- ...
55
圏 C
A B
X
X C
集合の圏 Sets
θX
θA
{ αX
} F(A)
Hom(X, A)
idX
fA
, gA
, hA
, ...
※ Hom(X, A) の要素 fA
, gA
, hA
, ... の行き先を全てカバー
{ idX
}
X と B に着目した自然変換
- 同様に、 Hom(X, B) から F(B) への関数 θB
も完全に定まる
- mapF
(fB
)(αX
) = θB
( fB
)
- mapF
(gB
)(αX
) = θB
( gB
)
- mapF
(hB
)(αX
) = θB
( hB
)
- ...
56
圏 C
A B
X
X C
集合の圏 Sets
θX
θB
{ αX
} F(B)
Hom(X, B)
idX
fB
, gB
, hB
, ...
※ Hom(X, B) の要素 fB
, gB
, hB
, ... の行き先を全てカバー
{ idX
}
X と C に着目した自然変換
- 同様に、 Hom(X, C) から F(C) への関数 θC
も完全に定まる
- mapF
(fC
)(αX
) = θC
( fC
)
- mapF
(gC
)(αX
) = θC
( gC
)
- mapF
(hC
)(αX
) = θC
( hC
)
- ...
57
圏 C
A B
X
X C
集合の圏 Sets
θX
θC
{ αX
} F(C)
Hom(X, C)
idX
fC
, gC
, hC
, ...
※ Hom(X, C) の要素 fC
, gC
, hC
, ... の行き先を全てカバー
{ idX
}
αX
= θX
(idX
) が定まれば、自然変換 θ が定まる
- 結局:
- * :圏 C の任意の対象
- f*
:X から * への任意の射
- これら全てに対して、mapF
(f*
)(αX
) = θ*
(f*
) が成り立つ
- この等式で任意性がある部分は、αX
の選び方だけ
58
圏 C
A B
X
X C
集合の圏 Sets
θX
θ*
{ αX
} F(*)
{ idX
} Hom(X, *)
idX
?f*
° _
mapF
(?f*
)
Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF ] ) ? F(X)
- F(X) の要素を αX
, βX
, γX
, ... とおく:
- αX
によってできる自然変換 :α とする
- βX
によってできる自然変換 :β とする
- γX
によってできる自然変換 :γ とする
- ...
- これより、F(X) の要素数と、自然変換の数は一致する ■
59
liftY:F(X) の要素を 1 つ受け取り、自然変換を構成する
60
// 函手 F で移された型の値を受け取って、自然変換を返す
def liftY[F[_], X](x: F[X])(implicit F: EndoFunctor[F]): Hom[X, *] ~> F =
new (Hom[X, *] ~> F) {
def apply[A](f: Hom[X, A]): F[A] = EndoFunctor[F].map(f)(x)
}
- liftY の実装は、x => ?A. ?fA
. mapF
(fA
)(x) という関数になっている:
- ?A :型パラメータ [A]
- ?fA
:Hom[X, A] 型の引数 f
- mapF
(fA
)(x) :EndoFunctor[F].map(f)(x)
lowerY:自然変換を受け取り、θX
(idX
) を取り出す
61
// 自然変換を受け取って、函手 F で移された型の値を返す
def lowerY[F[_], X](f: Hom[X, *] ~> F): F[X] =
f(x => x)
- lowerY の実装は、?A. θA
=> θX
(idX
) という関数になっている:
- ?A. θA
:Hom[X, *] ~> F のインスタンス f
- idX
:X 型の恒等関数 x => x
- θX
(idX
) :f(x => x)
Any Questions ?
Chatwork 株式会社では、
フロントエンド,バックエンドのどちらでも、
関数型や圏論の考え方で設計をキレイにしたい
エンジニアを募集しています (勉強会もあるよ ?)
We are Hiring !!!
63
働くを
もっと楽しく、
創造的に
Appendix:さらに学ぶために
- もう諦めない圏論入門 (@norkron)
https://qiita.com/norkron/items/237735106ee6e5333678
- 圏論勉強会 第 4 回 ~ 射で考える (@9_ties)
http://nineties.github.io/category-seminar/4.html#/
- 圏論とプログラミング (@inamiy)
https://speakerdeck.com/inamiy/category-theory-and-programming
- Category Theory for Programmers ~ Scala Edition (@BartoszMilewski)
https://github.com/hmemcpy/milewski-ctfp-pdf
64

More Related Content

Scala 初心者が米田の補題を Scala で考えてみた

  • 2. 自己紹介 - 名前: 高瀬 和之 (たかせ かずゆき) - 所属: Chatwork 株式会社 @大阪 - たぶん得意なこと: - フロントエンド開発 (React / Redux / TypeScript) - ティーチング (アルゴリズム / 機械学習 / 数学 / 組み込みシステム) - ひとこと: - Scala のイベントは 2 回目です ? 2
  • 3. 1. 本日の茶番パート 2. 圏論の公理 3. 函手,自然変換,函手圏 4. 米田の補題 アジェンダ 3 - この発表を聞いて得られるもの ??? - 圏論の中でも登竜門的なトピックである "米田の補題" を知ることができる - "米田の補題" のプログラミング的位置づけを知ることができる - ※ 後ろのセッションもないので、40 分をややオーバーするやも ?
  • 8. 圏論ことはじめ (1):対象と射 8 - 圏論の材料 - 対象 :点 - 射 :点から点を結ぶ矢印 (点と点の関連性を表す) - ここまでの事実 ? なんか有向グラフっぽい
  • 9. 圏論ことはじめ (2):圏の例 - しりとりの圏 (対象:ひらがな,射:単語) 9 - 型と関数の圏 (対象:型,射:関数) り ご ら ぱ と りんご ごりら らっぱ ぱーせんと String Int Boolean length isEven isCamelCase
  • 10. 圏論ことはじめ (3):Hom 集合 - 圏論では、ある対象 ● から別の対象 ● へ、複数の射が存在してもよい - すなわち、射の集合を考えることができる ? Hom 集合と呼ぶ - 対象 ● から対象 ● に関する Hom 集合 ? Hom(●, ●) と表す - 下図の場合: - Hom(●, ●) = { a, b, c, d, e } - Hom(●, ●) = ? 10 a e d b c
  • 11. ところで "公理" とは? ? ? 前提として認めてしまうルールのこと
  • 12. 圏論の公理 (1):合成射の存在,およびその可換性 12 - 合成射の存在 - f :A から B に向かう射 - g :B から C に向かう射 - これらが存在するとき、必ず A から C に向かう射 g ° f が存在するべき - 可換性 - f と g をそれぞれ使って、A から C に至ること - g ° f を 1 つ使って、A から C に至ること - これらは等しくなるべき f g g ° f A B C
  • 13. NG な例 ? 13 - in Scala 圏: - length :長さを調べる関数 - isEven :偶数であるかを調べる関数 - isCamelCase :キャメルケースであるかを調べる関数 - このとき、始点?終点となる対象 (型) はそれぞれ一致しているが、 可換性が無いため、isCamelCase は合成射になっていない! length isEven isCamelCase String Int Boolean
  • 14. OK な例 ??♂ 14 - in Scala 圏: - length :長さを調べる関数 - isEven :偶数であるかを調べる関数 - compose :与えられた 2 つの関数を、合成する高階関数 - このとき、compose で得られる射 (関数) は合成射の条件をみたす length isEven isEven compose length String Int Boolean
  • 15. f ∈ Hom(A, B) ? ?a ∈ Hom(X, A), ?b ∈ Hom(X, B), b = f ° a - 合成射の存在より、A から B に向かう射が 1 つでも存在すれば、 必ず X から B に向かう射が存在する ? Hom(X, B) の存在がいえる - Hom(X, A) の任意の要素を、Hom(X, B) のある要素に対応づける、 自明な関数 f ° _ を考えることができる 15 X B A 圏 C 集合の圏 Sets Hom(X, A) Hom(X, B)f f ° _ ※ 合成射が必ず存在
  • 16. 圏論の公理 (2):恒等射の存在,およびその単位律 16 - 恒等射の存在 - 任意の対象 X に関して、必ず X から X 自身に向かう射 idX が存在するべき - 単位律 - ?f:X から Y に向かう任意の射 - idX ° f , f ° idY , および f のそれぞれが等しくなるべき ?f idX X Y X Y ?f?f idY
  • 17. NG な例 ? 17 - in Scala 圏: - increment ? 与えられた数を、1 増やして返す関数 - このとき、increment は Int から Int 自身に向かう射ではあるが、 恒等射になっていない! (例:increment ≠ increment ° increment) Int Int Int increment increment increment
  • 18. OK な例 ??♂ 18 - in Scala 圏: - identityInt ? 与えられた数を、そのまま返す関数 - このとき、identityInt は恒等射の条件をみたす ∵ 任意の型 X からの任意の関数 f に対して、identityInt ° f = f X Int Int identityInt ?f ?f
  • 19. ?X ∈ Obj(C), Hom(X, X) ≠ ? - 恒等射の存在より、任意の対象 X には恒等射 idX が必ず備わる - よって、Hom(X, X) には少なくとも 1 つは射が含まれる (※ この事実は米田の補題を考える上でも重要となる) 19 X X 圏 C Hom(X, X) ?X, ?idX ? idX 集合の圏 Sets
  • 20. - …については割愛します ? - ざっくり言うと: - f :A から B に向かう射 - g :B から C に向かう射 - h :C から D に向かう射 - このとき、(h ° g) ° f と h ° (g ° f) は等しくなるべき - そうなるように合成演算子 ° を考えてね,と捉えても良い 圏論の公理 (3):合成射の結合律 20
  • 22. 函手 / Functor - ある圏から、グラフ構造をすべて抜き出す - 別の圏にて、グラフ構造が一致する箇所に対応づける - 対象と対象の対応関係,および射と射の対応関係,その 2 つ組と考えてもよい 22 圏 D圏 C
  • 23. 函手の記号的表現 - 圏 C から圏 D への函手を考える: - 対象と対象の対応関係は、関数 F で表してみる - 射と射の対応関係は、関数 mapF で表してみる (※ 数学的にはどちらも同じ記法で表してしまう場合が多いが、今回は分かりやすさを重視) 23 圏 D X Y f F(X) F(Y) mapF (f) 圏 C
  • 24. 考察:函手と合成射 (1) - 合成射に関するグラフ表現を、函手で移すことを考える: - 対象 A, B, C :対象 F(A), F(B), F(C) に対応 - 射 f, g :射 mapF (f), mapF (g) に対応 - 合成射 g ° f :射 mapF (g ° f) に対応 24 A 圏 D圏 C B C F(B) F(A) F(C) f g mapF (f) mapF (g) g ° f mapF (g ° f)
  • 25. - 合成射の存在より、mapF (f) と mapF (g) だけに着目しても、 これらの合成射 mapF (g) ° mapF (f) を考えることができる - これは、mapF (g ° f) とは別ものなのだろうか? ? 考察:函手と合成射 (2) 25 A 圏 D圏 C B C F(B) F(A) F(C) f g mapF (f) mapF (g) g ° f mapF (g ° f) mapF (g) ° mapF (f)
  • 26. 函手の性質 (1):準同型性 - mapF (g ° f) = mapF (g) ° mapF (f) となるように、函手は定めるべき ? このような性質を準同型性という - 直感的には: - ある圏の合成射が、別の圏でも合成射に移される,ということ 26 A 圏 D圏 C B C F(B) F(A) F(C) f g mapF (f) mapF (g) g ° f mapF (g ° f) = mapF (g) ° mapF (f)
  • 27. 函手の性質 (2):恒等射の保存 - mapF (g ° f) = mapF (g) ° mapF (f) という等式の f, g に、それぞれ id* を代入する (※ 各射における始点?終点は、適宜調整してあるものとする) - f に id* を代入すると: - mapF (g ° id* ) = mapF (g) = mapF (g) ° mapF (id* ) ∴ mapF (g) = mapF (g) ° mapF (id* ) ? 右から合成しても影響がない - g に id* を代入すると: - mapF (id* ° f) = mapF (f) = mapF (id* ) ° mapF (f) ∴ mapF (f) = mapF (id* ) ° mapF (f) ? 左から合成しても影響がない - これより、id* を函手で移して得られる mapF (id* ) は、恒等射の性質を保つ (※ 厳密には、函手で移されていない射に対しても恒等射となることを保証するために、公理として与える) 27
  • 28. 函手 in Scala 圏 28 // F[_] が対象の対応関係を,map が射の対応関係を表す trait EndoFunctor[F[_]] { def map[X, Y](f: X => Y): F[X] => F[Y] } // 任意の函手の実装を、カインドで指定して取り出す (※ といいつつ Scala 圏には閉じているので、Endo = 自己) object EndoFunctor[F[_]] { def apply[F[_]](implicit instance: EndoFunctor[F]): EndoFunctor[F] = instance } - ちなみに、圏と圏をまたぐ函手を Scala 圏で表現したい場合の例など: - カインド C[X, Y] を用いて、C[X, Y] 部分に圏の情報をエンコード - C[X, Y] 部分に射の情報をエンコード (始点と終点の 2 つ)
  • 30. - 圏 C から圏 D への函手を 2 つ考える: - 1 つめは、F および mapF で表すとする - 2 つめは、G および mapG で表すとする - このとき、どちらの函手も圏 C を基点に考えている ? 関連性を見出せそう!? 考察:2 つの函手の関連性 30 圏 D X Y f F(X) F(Y) mapF (f) 圏 C G(X) G(Y) mapG (f)
  • 31. - 圏 C の対象 X に対して、圏 D で F(X) と G(X) をグルーピングすることを考える - 圏論の言葉でこれを表すには、各対象間に射 θX を用意することが考えられる - この θX 全体を、劣自然変換と呼ぶ - ? "対象" のみに着目した、函手と函手の関連性 函手の弱い関連性 31 圏 D圏 C [ F / mapF ] [ G / mapG ] θ● θ● θ●
  • 32. - 各対象間に射 θX を用意することに加えて、逆射 θX -1 が存在する状況を考える (※ θX ° θX -1 ,および θX -1 ° θX が、それぞれ恒等射となること) - なおかつ、各閉領域はそれぞれ可換だとする - この θX / θX -1 全体を、自然同型と呼ぶ - ? 自然同型では、一方の函手から他方の函手を完全再現できる 函手の強い関連性 32 圏 D圏 C θ● / θ● -1 θ● / θ● -1 θ● / θ● -1 [ F / mapF ] [ G / mapG ]
  • 33. - 各対象間に射 θX を用意する - なおかつ、各閉領域はそれぞれ可換だとする - この θX 全体を、自然変換と呼ぶ (θ : F ? G と表す) - ? "対象" と "射" の双方に着目した、函手と函手の関連性 (ほどほどの関連性) 自然変換 / Natural Transformation 33 圏 D圏 C θ● θ● θ●  ? θ [ F / mapF ] [ G / mapG ]
  • 35. - 自然変換そのものは、各対象間に射 θX として与えられる ? すなわち、函手で移した任意の型ごとに、関数が備わっている ≒ 多相的な関数 - F[X] => G[X] を、型 X ごとにアドホックに実装すると辛い… (ほぼ不可能 ?) ? X は多相型として考えてしまう場合が多い 自然変換 in Scala 圏 (1) 35 Scala 圏Scala 圏 θA θB θC A B C G[A] G[B] G[C] F[A] F[B] F[C]
  • 36. 自然変換 in Scala 圏 (2) 36 // F, G にそれぞれ函手を指定する trait ~>[F[_], G[_]] { def apply[X](x: F[X]): G[X] // ?X. F[X] => G[X] に相当 } // Seq 函手の実装 implicit val seqFunctor = new EndoFunctor[Seq] { def map[X, Y](f: X => Y): Seq[X] => Seq[Y] = _.map(f) } // Const 函手の実装 (常に特定の対象と射に移す函手) type Const[X] = Int // Int で固定しているが、* -> * -> * というカインドだとより汎用的 implicit val constFunctor = new EndoFunctor[Const] { def map[X, Y](f: X => Y): Const[X] => Const[Y] = x => x // 常に恒等射に移す }
  • 37. 自然変換 in Scala 圏 (3) 37 // Seq 函手と Const 函手にまたがる自然変換の例 val length = new (Seq ~> Const) { def apply[X](x: Seq[X]): Const[X] = x.length } // 函手で移す射 val f: Int => String = x => s"$x" // 可換性の簡易テスト: lengthString ° mapSeq (f) = mapConst (f) ° lengthInt println( length(EndoFunctor[Seq].map(f)(Seq(0, 1, 2))) ) println( EndoFunctor[Const].map(f)(length(Seq(0, 1, 2))) ) - ちなみに、多相関数として F[A] => G[A] を考えると、 自然と可換性も満たされる場合があります ? e.g. Parametricity
  • 39. - 函手で移した構造全体を、まるごと 1 つで対象と捉える - θX 全体を、まるごと 1 つで射と捉える - このようにして得られる圏を、函手圏と呼ぶ - 基点とした圏を C,函手で移す先の圏を D とする場合、函手圏は DC で表す 函手圏 / Functor Category 39 F / mapF 函手圏 DC G / mapG θ = ?X. θX 圏 D圏 C θ● θ● θ●
  • 40. α● γ● α● γ● - 函手で移した構造全体に対して、複数の自然変換が存在する場合を考える (※ 異なる自然変換同士で、可換性が満たされる必要はない) - このとき、函手圏では 2 対象間に複数の射が存在することになる - 下図の函手圏 DC で Hom 集合を考えた場合: - Hom( [ F / mapF ] , [ G / mapG ] ) = { α, β, γ } 函手圏における Hom 集合 40 F / mapF 函手圏 DC G / mapG α = ?X. αX β = ?X. βX γ = ?X. γX 圏 D β● β● β● α● γ●
  • 41. 考察:そもそも自然変換はいくつも存在しうるのか? ? 41 // これとか… val length1 = new (Seq ~> Const) { def apply[X](x: Seq[X]): Const[X] = x.length } // あれとか… val length2 = new (Seq ~> Const) { def apply[X](x: Seq[X]): Const[X] = 0 } // それとか,ね? ? val length3 = new (Seq ~> Const) { import scala.math.sqrt def apply[X](x: Seq[X]): Const[X] = sqrt(x.length).toInt }
  • 43. 共変 Hom 函手 - 任意の圏から集合の圏 Sets への函手であって, - 対象 * を対象 Hom(X, *) へ移し, - 射 f を射 f ° _ へ移す,そんな函手 43 ?a ?b ?f, b = f ° a Hom(X, A) Hom(X, B) f ° _ X B A 圏 C 集合の圏 Sets
  • 44. Hom 函手と集合値函手の自然変換 - 圏 C から集合の圏 Sets への函手を 2 つ考える: - 1 つめは、対象 X を固定した Hom 函手 :[ Hom(X, *) / f → f ° _ ] - 2 つめは、適当な集合値函手 :[ F / mapF ] - このとき、自然変換 θ = ?A. θA : Hom(X, A) → F(A) 44 集合の圏 Sets圏 C θA θB θC A B C F(A) F(B) F(C)X Hom(X, A) Hom(X, B) Hom(X, C)
  • 45. Hom 函手と集合値函手の、函手圏における Hom 集合 - ここで、函手圏 SetsC で Hom 集合を考えたいが、表記が紛らわしい ? - ? 函手圏での Hom 集合は、Nat(   ,   ) のように表すとする - 下図の函手圏 SetsC で Hom 集合を考えた場合: - Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF ] ) = { α, β, γ } 45 α● γ● α● γ● Hom(X, *) / f → f ° _ 函手圏 SetsC F / mapF α = ?X. αX β = ?X. βX γ = ?X. γX 集合の圏 Sets β● β● β● α● γ● F(A) F(B) F(C) Hom(X, A) Hom(X, B) Hom(X, C)
  • 46. "米田の補題" の主張 - 函手圏 SetsC での Hom 集合もまた、集合の圏 Sets の対象 - 圏 C で固定した対象 X を、函手で移した F(X) もまた、集合の圏 Sets の対象 - ここで: - Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF ] ) ? F(X) (※ これら 2 つの集合の要素が、それぞれ 1 対 1 に対応すること) 46 α● γ● α● γ● β● β● β● α● γ● F(A) F(B) F(C) Nat( [ Hom(X, *) / f → f ° _ ], [ F / mapF ] ) F(X) ※ 全単射が存在する Hom(X, A) Hom(X, B) Hom(X, C) 集合の圏 Sets
  • 47. ? < ちょっと何言ってるか分からないっす - …おっしゃる通り?,少し Scala 圏の表現に翻訳してみましょう: - 集合 :"型" として捉えてみる - 全単射 :"関数" と "逆関数" がある状態と捉えてみる - その上で: - F(X) :型 F[X] (※ 集合値の意味づけによる埋め込み) - Hom(X, Y) :型 X => Y (※ 指数対象による埋め込み) - Nat(   ,   ) :多相型 [A](X => A) => F[A] (※ 多相型ラムダ計算の圏論的な意味づけによる埋め込み) 47
  • 48. "米田の補題" の主張 in Scala 圏 - よって、米田の補題は次の 2 つが存在することを表す: - 高階多相関数 lowerY = (f: [A](X => A) => F[A] ): F[X] { ... } - 高階多相関数 liftY = (x: F[X] ): [A](X => A) => F[A] { ... } - なおかつ: - lowerY compose liftY == identityF[X] - liftY compose lowerY == identity[A](X => A) => F[A] 48
  • 49. 米田の補題 in Scala 圏 49 // Hom 集合の型表現をカインドとして用意 (※ 本当は EndoFunctor のインスタンスも用意するべきだが、割愛) type Hom[X, Y] = X => Y // 函手 F で移された型の値を受け取って、自然変換を返す def liftY[F[_], X](x: F[X])(implicit F: EndoFunctor[F]): Hom[X, *] ~> F = new (Hom[X, *] ~> F) { def apply[A](f: Hom[X, A]): F[A] = EndoFunctor[F].map(f)(x) } // 自然変換を受け取って、函手 F で移された型の値を返す def lowerY[F[_], X](f: Hom[X, *] ~> F): F[X] = f(x => x) - Rank2Types は、呼び出し可能インスタンスで代用できるという知見を得た ? - implicit parameter の探索範囲は、勝手に拡張されないという知見を得た ? (1 敗
  • 51. 固定した対象 X を中心とした、圏 C のセッティング - 固定した対象 X と、射で接続された対象たちをピックアップ - e.g. A, B, C, ... - このとき X 自身にも、恒等射 idX による接続がある - 各対象間には複数の射が存在しうるので、対象ごとに f* , g* , h* , ... と表してみる - e.g. X から A に伸びる射であれば、fA , gA , hA , ... 51 圏 C A B X X C idX
  • 52. X と A に着目した自然変換 (1) - X と A を接続する射は、fA , gA , hA , ... と複数ある - ? ここでは fA をピックアップし、それぞれの函手で移す - ここで、自然変換の満たす可換図式から、以下の 2 つが等価: - mapF (fA ) ° θX - θA ° (fA ° _) 52 圏 C A B X X C 集合の圏 Sets θX θA F(X) F(A) Hom(X, X) Hom(X, A) idX fA ° _ mapF (fA ) fA , gA , hA , ...
  • 53. X と A に着目した自然変換 (2) - Hom(X, X) には idX が含まれるので、試しに代入してみる: - (mapF (fA ) ° θX )(idX ) = mapF (fA )(θX (idX )) - (θA ° (fA ° _))(idX ) = θA (fA ° idX ) = θA (fA ) - ∴ mapF (fA )(θX (idX )) = θA (fA ) - X から A への全ての射 fA , gA , hA , ... に関して、同様な計算を行うと: - mapF (fA )(θX (idX )) = θA (fA ) - mapF (gA )(θX (idX )) = θA (gA ) - mapF (hA )(θX (idX )) = θA (hA ) - ... 53
  • 54. X と A に着目した自然変換 (3) - ここで、  でハイライトした箇所は、圏 C や函手の構成から既知である: - mapF (fA ) (θX ( idX )) = θA ( fA ) - mapF (gA ) (θX ( idX )) = θA ( gA ) - mapF (hA ) (θX ( idX )) = θA ( hA ) - ... - 仮に、θX (idX ) の写像を、F(X) の要素から 1 つ選び、αX とおくと: - mapF (fA )(αX ) = θA ( fA ) - mapF (gA )(αX ) = θA ( gA ) - mapF (hA )(αX ) = θA ( hA ) - ... 54
  • 55. X と A に着目した自然変換 (4) - したがって、下記の対応は、 Hom(X, A) から F(A) への関数 θA を完全に定める - mapF (fA )(αX ) = θA ( fA ) - mapF (gA )(αX ) = θA ( gA ) - mapF (hA )(αX ) = θA ( hA ) - ... 55 圏 C A B X X C 集合の圏 Sets θX θA { αX } F(A) Hom(X, A) idX fA , gA , hA , ... ※ Hom(X, A) の要素 fA , gA , hA , ... の行き先を全てカバー { idX }
  • 56. X と B に着目した自然変換 - 同様に、 Hom(X, B) から F(B) への関数 θB も完全に定まる - mapF (fB )(αX ) = θB ( fB ) - mapF (gB )(αX ) = θB ( gB ) - mapF (hB )(αX ) = θB ( hB ) - ... 56 圏 C A B X X C 集合の圏 Sets θX θB { αX } F(B) Hom(X, B) idX fB , gB , hB , ... ※ Hom(X, B) の要素 fB , gB , hB , ... の行き先を全てカバー { idX }
  • 57. X と C に着目した自然変換 - 同様に、 Hom(X, C) から F(C) への関数 θC も完全に定まる - mapF (fC )(αX ) = θC ( fC ) - mapF (gC )(αX ) = θC ( gC ) - mapF (hC )(αX ) = θC ( hC ) - ... 57 圏 C A B X X C 集合の圏 Sets θX θC { αX } F(C) Hom(X, C) idX fC , gC , hC , ... ※ Hom(X, C) の要素 fC , gC , hC , ... の行き先を全てカバー { idX }
  • 58. αX = θX (idX ) が定まれば、自然変換 θ が定まる - 結局: - * :圏 C の任意の対象 - f* :X から * への任意の射 - これら全てに対して、mapF (f* )(αX ) = θ* (f* ) が成り立つ - この等式で任意性がある部分は、αX の選び方だけ 58 圏 C A B X X C 集合の圏 Sets θX θ* { αX } F(*) { idX } Hom(X, *) idX ?f* ° _ mapF (?f* )
  • 59. Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF ] ) ? F(X) - F(X) の要素を αX , βX , γX , ... とおく: - αX によってできる自然変換 :α とする - βX によってできる自然変換 :β とする - γX によってできる自然変換 :γ とする - ... - これより、F(X) の要素数と、自然変換の数は一致する ■ 59
  • 60. liftY:F(X) の要素を 1 つ受け取り、自然変換を構成する 60 // 函手 F で移された型の値を受け取って、自然変換を返す def liftY[F[_], X](x: F[X])(implicit F: EndoFunctor[F]): Hom[X, *] ~> F = new (Hom[X, *] ~> F) { def apply[A](f: Hom[X, A]): F[A] = EndoFunctor[F].map(f)(x) } - liftY の実装は、x => ?A. ?fA . mapF (fA )(x) という関数になっている: - ?A :型パラメータ [A] - ?fA :Hom[X, A] 型の引数 f - mapF (fA )(x) :EndoFunctor[F].map(f)(x)
  • 61. lowerY:自然変換を受け取り、θX (idX ) を取り出す 61 // 自然変換を受け取って、函手 F で移された型の値を返す def lowerY[F[_], X](f: Hom[X, *] ~> F): F[X] = f(x => x) - lowerY の実装は、?A. θA => θX (idX ) という関数になっている: - ?A. θA :Hom[X, *] ~> F のインスタンス f - idX :X 型の恒等関数 x => x - θX (idX ) :f(x => x)
  • 64. Appendix:さらに学ぶために - もう諦めない圏論入門 (@norkron) https://qiita.com/norkron/items/237735106ee6e5333678 - 圏論勉強会 第 4 回 ~ 射で考える (@9_ties) http://nineties.github.io/category-seminar/4.html#/ - 圏論とプログラミング (@inamiy) https://speakerdeck.com/inamiy/category-theory-and-programming - Category Theory for Programmers ~ Scala Edition (@BartoszMilewski) https://github.com/hmemcpy/milewski-ctfp-pdf 64