Mercurial > hg > Papers > 2015 > atton-thesis

annotate category.tex @ 22:fc44782929a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add monad in Haskell
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 09 Feb 2015 11:17:00 +0900
parents 7d94faaeb448
children 113b49263d40
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{Categorical Definitions of Monad}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
2 \label{chapter:category}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
3
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
4 \ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
5 ここで Monad の定義と要請されるMonad則について述べる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
6 また、定義は Monad の解説に必要な部分についてのみ解説する。
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
8 % {{{ Category
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
9
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \section{Category}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
11 \label{section:category}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
12 まずは Monad の定義に必要な Category (圏)について述べる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
13
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
14 category は2つの要素を持つ。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
15
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
16 \begin{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
17 \item object (要素)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
18
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
19 \item morphism (射, arrow)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
20
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
21 object から object へのマッピング。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
22
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
23 morphism によってマップされる対象を domain と呼び、マップした先の対象を codomain と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
24 つまり domain から codomain への object をマップするものが morphism である。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
25 domain A と codomain B を持つ morphism f は式\ref{exp:morphism}のように書くこととする。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
26
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
27 \begin{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
28 f : A \rightarrow B
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
29 \label{exp:morphism}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
30 \end{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
31
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
32 \end{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
33
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
34 そして category は object と moprhism に対して2つの法則を満たす。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
35
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
36 \begin{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
37 \item 全ての object について identity mapping が存在する
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
38
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
39 identity mapping とは domain と codomain が同じ morphism のことである。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
40 identity mappping は id と略する。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
41 id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
42
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
43 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
44
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
45 morphism の合成には記号 $ \circ $ を用いる。
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
46 object B から C への morpshim f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morphism_compose}となる。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
47
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
48 \begin{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
49 f \circ g : A \rightarrow C
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
50 \label{exp:morphism_compose}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
51 \end{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
52
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
53 改めて、morphism の合成の順序が結果に影響しないことを式にすると式\ref{exp:morphism_composition_law}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
54
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
55 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
56 \label{exp:morphism_composition_law}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
57 f : C \rightarrow D \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
58 g : B \rightarrow C \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
59 h : A \rightarrow B \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
60 (f \circ g) \circ h = f \circ (g \circ h) : A \rightarrow D
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
61 \end{eqnarray}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
62 \end{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
63
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
64 例えば、object A,B と A から B への moprhism を持つ category は図\ref{fig:simple_category}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
65
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
66 \begin{figure}[htbp]
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
67 \begin{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
68 \includegraphics[scale=1.0]{fig/simple_category.pdf}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
69 \caption{object A,B と morpshim f を持つ category}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
70 \label{fig:simple_category}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
71 \end{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
72 \end{figure}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
73
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
74 なお、id は全ての object に存在するために省略して書くことが多いため、これからは省略する。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
75
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
76 object を点、morphism を線とした図を commutative diagram (可換図式) と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
77 ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
78 例えば、式\ref{exp:morphism_composition_law}の category の commutative diagram は図\ref{fig:morphism_composition_law}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
79
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
80 \begin{figure}[htbp]
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
81 \begin{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
82 \includegraphics[scale=0.8]{fig/morphism_composition_law.pdf}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
83 \caption{式\ref{exp:morphism_composition_law} の morphism の合成法則の category がなす commutative diagram}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
84 \label{fig:morphism_composition_law}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
85 \end{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
86 \end{figure}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
87
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
88
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
89 commutative diagram が commutative である時、moprhism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
90 ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
91
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
92 % }}}
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
93
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
94 % {{{ Functor
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
95
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 \section{Functor}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
97 \label{section:functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
98 \ref{section:category} 節では category を定義した。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
99 \ref{section:functor} 節では category から category への mapping である Functor (関手)について解説する。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
100
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
101 functor F とはある category C から D への mapping である。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
102 functor F を用いて category C の object もしくは morphism である x を category D の object もしくは morphism に対応させることを式\ref{exp:apply_functor}のように記述する。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
103
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
104 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
105 F(x)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
106 \label{exp:apply_functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
107 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
108
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
109 functor は以下の functor 則を満たす。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
110
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
111 \begin{itemize}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
112 \item id を保存する
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
113
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
114 category C における object A への id $ 1_A $ は F A においても id として振る舞う。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
115
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
116 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
117 F(1_A) = 1_{F(A)}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
118 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
119
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
120 \item morphism の合成を保存する
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
121
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
122 category C における morphism f g の合成を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
123 合成された $ f \circ g $ を F により mapping することと、f と g を個別に F により mapping した後に合成した結果は同じである。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
124
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
125 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
126 F(f \circ g) = F(f) \circ F(g)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
127 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
128 \end{itemize}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
129
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
130 functor の例を挙げる。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
131 まず、 3つの object A,B,C と morphism f,g,h を持つ category C を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
132 category C の morphism は式\ref{exp:functor_categoryC}であるとする。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
133
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
134 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
135 \label{exp:functor_categoryC}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
136 f : A \rightarrow C \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
137 g : B \rightarrow B \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
138 h : B \rightarrow C \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
139 f = g \circ h
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
140 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
141
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
142 次に、 2 つの object A', B' と morphism f', g' を持つ category D を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
143 category D の morphism は式\ref{exp:functor_categoryD}であるとする。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
144
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
145 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
146 \label{exp:functor_categoryD}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
147 f : B' \rightarrow A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
148 g : A' \rightarrow B' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
149 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
150
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
151 C から D への functor F は式\ref{exp:functorF}のようなものがある。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
152
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
153 要素数が異なるため一見正しく mapping できないように思えるが、正しく Functor 則を満たしている。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
154
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
155 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
156 \label{exp:functorF}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
157 F(A) = A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
158 F(B) = B' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
159 F(C) = A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
160 F(id_A) = F(id_{A'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
161 F(id_B) = F(id_{B'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
162 F(id_C) = F(id_{A'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
163 F(f) = id_{A'} \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
164 F(g) = g' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
165 F(h) = f' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
166 F(h \circ g) = F(h) \circ F(g) = f' \circ g' = id_{A'} = F(f)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
167 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
168
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
169 functor F を用いて category C を category D へと mapping した図が図\ref{fig:functor}である。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
170
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
171 \begin{figure}[htbp]
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
172 \begin{center}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
173 \includegraphics[scale=0.8]{fig/functor.pdf}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
174 \caption{Functor の例}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
175 \label{fig:functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
176 \end{center}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
177 \end{figure}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
178
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
179 functor により category から category への mapping を考えることが可能となった。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
180
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
181 % }}}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
182
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
183 % {{{ Natural Transformation
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
184
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 \section{Natural Transformation}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
186 \label{section:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
187 \ref{section:functor}節では category から category への mapping である functor について述べた。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
188 \ref{section:natural_transformation}節では functor と functor の関係である Natural Transformation(自然変換)について述べる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
189
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
190 category C から D への functor F, G が存在する時、F から G への変換 t を考える。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
191
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
192 t は category C の A に対し、F(A) から G(A) への変換を提供する(式\ref{exp:trans})。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
193
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
194 \begin{equation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
195 t(A) : F(A) \rightarrow G(A)
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
196 \label{exp:trans}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
197 \end{equation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
198
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
199 t が 式\ref{exp:natural_transformation}を満たす時、t を natural transformation を呼ぶ。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
200
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
201 \begin{eqnarray}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
202 \label{exp:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
203 f : A \rightarrow B \\ \nonumber
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
204 G(f)t(A) = t(B)F(f)
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
205 \end{eqnarray}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
206
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
207 t が natural transformation である時、 category A における A を functor F で移したのちに morphism を適用しても、 functor G で移した後に morphism を適用しても良いという可換性が得られる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
208 式\ref{exp:natural_transformation}の可換図は図\ref{fig:natural_transformation}となる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
209
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
210 \begin{figure}[htbp]
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
211 \begin{center}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
212 \includegraphics[scale=1.0]{fig/natural_transformation.pdf}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
213 \caption{自然変換の可換図(式\ref{exp:natural_transformation})}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
214 \label{fig:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
215 \end{center}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
216 \end{figure}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
217
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
218 % }}}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
219
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
220 % {{{ Monad
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
221
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222 \section{Monad}
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
223 \label{section:monad}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
224 \ref{section:natural_transformation}節では functor 間の可換性 natural transformation について述べた。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
225
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
226 category, functor, natural transformation を用いて Monad を定義する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
227
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
228 category C における monad とは以下の性質を持つ $ triple (T, \eta, \mu) $ である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
229
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
230 \begin{itemize}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
231 \item $ T : C \rightarrow C $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
232
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
233 category C から C への functor T
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
234
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
235 \item $ \eta : id_C \rightarrow T $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
236
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
237 C から T への natural transformation $ \eta $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
238
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
239 \item $ \mu : T^2 \rightarrow T $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
240
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
241 $ T^2 $ から $ T $ への natural transformation $ \mu $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
242
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
243 なお、 $ T^2 $ とは $ TT $ と同義であるとする。つまり functor T による mapping を2回行なうものである。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
244 回数を n 回とすることで $ T^n $ と記述する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
245 \end{itemize}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
246
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
247 この $ triple (T, \eta, \mu) $ が図\ref{fig:monad_laws}の可換図を満たす。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
248 なお、Aに対する $ \mu $ を $ \mu_A $ と記述する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
249 同じように A に対する $ \eta $ を $ \eta_A $ と記述する
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
250
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
251 \begin{figure}[htbp]
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
252 \begin{center}
20
beebe0ffbcad Fix figures
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
253 \includegraphics[scale=0.9]{fig/monad_laws.pdf}
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
254 \caption{$ triple (T, \eta, \mu) $ が Monad であるために満たすべき可換図}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
255 \label{fig:monad_laws}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
256 \end{center}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
257 \end{figure}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
258
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
259 図\ref{fig:monad_laws} で示した可換図は monad が満たすべき Monad則であり、T に対する演算の可換性を強制する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
260 $ \eta $ は T を1つ増やすオペレーションであり、$ \mu $ は T を 2 つから1つに減らすオペレーションである。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
261
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
262 左側の可換図は T が 3つある場合の可換性である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
263 TTT に対して、 (TT)T のよう外側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても、 T(TT) のように内側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても可換であることを示す。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
264 つまり、TTTを減らす演算は左から行なっても右から行なっても良いことを示す。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
265
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
266 そして右側の可換図は T が1つである場合の可換性である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
267 T A に対して $ \eta $ を行ない TT A としてから $ \mu $ を行なっても、T A の内部の A に対して $ \eta $ を行ない TT A としてか $ \mu $ を行なっても、 T A の id と同じであることを示している。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
268 つまり、Tに対する演算における左右の単位元となるような性質を $ triple (T, \eta, \mu) $ に強制することとなる。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
269
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
270 % }}}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
271
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
272 % {{{ Category in Functional Programming
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
273
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
274 \section{Category in Functional Programming}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
275 \label{section:category_in_program}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
276 \ref{section:monad}節では Monad の定義について述べた。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
277 これからプログラムにおける Monad について述べていく。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
278 そのために\ref{section:category_in_program}節はプログラムと category の対応について述べる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
279
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
280 プログラムには値と関数のみが存在するとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
281
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
282 任意の値は型付けられるとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
283 変数x が型 A を持つ時、式\ref{exp:value_in_program}のように記述する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
284
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
285 \begin{equation}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
286 \label{exp:value_in_program}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
287 x : A
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
288 \end{equation}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
289
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
290 関数は値を受けとり値を返すものとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
291 A を取り B を返す関数f の型は式\ref{exp:function_in_program}のように記述する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
292
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
293 \begin{equation}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
294 \label{exp:function_in_program}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
295 f : A \rightarrow B
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
296 \end{equation}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
297
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
298 そして、引数と返り値の型が等しい関数は関数結合できるとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
299 関数結合の記号には $ \circ $ を用いる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
300 例えば、 A を取り B を返す関数 f と B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
301
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
302 \begin{eqnarray}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
303 \label{exp:function_compose_in_program}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
304 f : A \rightarrow B \\ \nonumber
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
305 g : B \rightarrow C \\ \nonumber
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
306 g \circ f : A \rightarrow C
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
307 \end{eqnarray}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
308
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
309 この時、型を object とし、関数を morphism とする category が構成できる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
310
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
311 この category が category が満たすべき法則を満たしているか確認する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
312
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
313 \begin{itemize}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
314 \item 全ての object について identity mapping が存在する
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
315
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
316 任意の型 A に対し $ A \rightarrow A $ である関数 id が定義できれば identitiy mapping が存在することになる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
317 任意の型の値x を受けとり、その値を返す関数が id となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
318
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
319 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
320
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
321 morpshim は関数である。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
322 つまり domain は引数の型であり、 codomain は返り値の型となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
323 morphism の合成は関数合成に相当し、合成の順序によらず引数と返り値の型は同じとなる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
324 \end{itemize}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
325
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
326 プログラムに対応する category が構成できた。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
327 特に例として用いているプログラミング言語 Haskell では値と関数は型を持つため、 category との対応が分かりやすい。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
328 よって例題には Haskell のプログラムを用いることとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
329
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
330 % }}}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
331
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
332 % {{{ Functor in Functional Programming
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
333
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
334 \section{Functor in Functional Programming}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
335 \label{section:functor_in_program}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
336 \ref{section:category_in_program}節ではプログラムとcategoryが対応していることを述べた。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
337 \ref{section:functor_in_program}節ではプログラムにおけるfunctor について述べる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
338
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
339 プログラムにおけるfunctor は型引数を持つことのできるデータ型に対応する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
340 型引数を持つデータ型とは、任意のデータ型に対して構成可能なデータ構造であり、List などが相当する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
341
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
342 たとえば、List は数値の List であっても Bool の List であっても構成可能である。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
343 この List を、型を受けとり型を返す型であると考えると、渡す型が引数のように振る舞う。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
344 この引数が型引数である。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
345
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
346 \begin{eqnarray}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
347 \label{exp:functor_type}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
348 A : Type \\ \nonumber
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
349 List A : Type \\ \nonumber
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
350 List : Type \rightarrow Type
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
351 \end{eqnarray}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
352
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
353 つまり、型と関数から構成される category から List 型と List に対応する関数からなる category へと置きかえるような functor が存在すれば良い。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
354
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
355 Haskell では functor はリスト \ref{src:functor_in_haskell} のように型クラスとして提供される。
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
356
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
357 \begin{table}[html]
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
358 \lstinputlisting[label=src:functor_in_haskell, caption=Haskell における Functor の定義] {src/functor_class.hs}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
359 \end{table}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
360
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
361 functor であることを保証したい型は f として表される。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
362 そしてデータ型が functor であることを示すためには、 fmap という関数を定義すれば良いことが分かる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
363 fmap は型a から型bへの関数を取り、f a を取り f b を返す。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
364 つまり、f でない型への演算をfの型においても適用するために変換する関数である。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
365 morpshim は関数であるため、 $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っていることが分かる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
366 よって morphism を morphism へと mapping することができるため functor となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
367
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
368 また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
369 ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
370 よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
371 なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
372
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
373 functor の例として、型がInt である変数 x と Int から Bool を返す even 関数を考える。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
374 このプログラムがなす category C は object が Int であり、 morphism が show となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
375 category C を functor によって別の category に写すことができる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
376
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
377 例えば List がなす category がある。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
378
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
379 まずHaskell において List を定義する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
380 List は任意の型 a を取り、 List a とする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
381 空の List は Nil とし、List a に対して a の値を Cons で追加することによって List を構築するとする。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
382
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
383 ここで List が Functor であると定義する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
384 fmap は a を取りbを返す関数を取り、List a を取って List b を返す関数である。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
385 つまり、関数を取ってList の全ての要素に適用することで実現できる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
386
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
387 定義した結果がリスト\ref{src:list_in_haskell} である。
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
388
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
389 \begin{table}[html]
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
390 \lstinputlisting[label=src:list_in_haskell, caption=Haskell におけるListの例] {src/list.hs}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
391 \end{table}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
392
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
393 Int型を持つ値x と、Intから Bool返す関数 even を考える。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
394 even を x に適用すると Bool となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
395
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
396 この際、x を持つ List の型は List Int であり、 fmap によって even を List Int に適用すると List Bool となる。
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
397 Haskell における実行結果はリスト\ref{src:exec_list_in_haskell} のようになる。
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
398
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
399 \begin{table}[html]
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
400 \lstinputlisting[label=src:exec_list_in_haskell, caption=Haskell における List の実行例] {src/exec_list_in_haskell.txt}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
401 \end{table}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
402
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
403 なお、 Haskell において型Aを持つ値xは $ x :: A $ のように記述される。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
404 x と even からなるプログラムから、型List と fmap を用いることにより List におけるプログラムでも同じように Bool が得られる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
405 これを通常のプログラムから List のプログラムへの functor とみなす。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
406
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
407 このように、型引数を持つ型とfmapによる関数の変換を定義することによってプログラムにおける functor を実現する。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
408 可換図で表現すると図\ref{fig:functor_in_haskell}となる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
409
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
410 \begin{figure}[htbp]
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
411 \begin{center}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
412 \includegraphics[scale=0.8]{fig/functor_in_haskell.pdf}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
413 \caption{Haskell における Functor の例がなす可換図}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
414 \label{fig:functor_in_haskell}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
415 \end{center}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
416 \end{figure}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
417
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
418 functor の定義にあたり、\ref{section:functor}節で示したように Functor則を満たすようにデータ型と fmap を定義しなくてはならない。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
419
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
420 Haskell における Functor則はリスト\ref{src:functor_laws_in_haskell}のように表される。
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
421
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
422 \begin{table}[html]
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
423 \lstinputlisting[label=src:functor_laws_in_haskell, caption=Haskellにおける Functor則] {src/functor_laws_in_haskell.txt}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
424 \end{table}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
425
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
426 1行目がid の保存に、2行目が関数の合成の保存に対応している。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
427 なお、 Haskell における関数合成は \verb/./ によって行なわれる。
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
428
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
429 % }}}
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
430
21
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
431 % {{{ Natural Transformation in Functional Programming
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
432
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
433 \section{Natural Transformation in Functional Programming}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
434 \label{section:natural_transformation_in_program}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
435 \ref{section:functor_in_program}節ではプログラムにおける functor を定義した。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
436 \ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べる。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
437
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
438 natural transformation は functor と functor 間の変換である。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
439 プログラムにおいて functor は型引数を持つデータ構造であったため、データ構造からデータ構造への変換となる。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
440
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
441 natural transformationは図\ref{fig:natural_transformation}で示したような可換図が可換になるような t であった。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
442 つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
443
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
444 プログラムにおける natural transformation は t は図\ref{fig:natural_transformation}を満たすような関数として表現される。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
445 Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
446
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
447 List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
448
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
449 \begin{table}[html]
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
450 \lstinputlisting[label=src:natural_transformation_in_haskell, caption=List の先頭を除いた List を返す tail 関数] {src/natural_transformation_list.hs}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
451 \end{table}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
452
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
453 100, 200, 300 の数値を持つ List Int を考える。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
454 この List が functor f に相当する。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
455 Int を取り Bool を返す関数 even を fmap により適用すると List Bool が得られる。
18
086fc8bb6ea9 Add description for category/functor in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
456
21
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
457 ここで natural transformation tail を考える。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
458 tail は List a から List a への関数であるため、 functor f,g は両方とも List である。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
459 natural transformation の定義から、 tail を行なってから fmap even しても、 fmap even を行なってら tail を行なっても結果が同じであれば良い。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
460 実行した結果がリスト\ref{src:exec_tail}である。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
461
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
462 \begin{table}[html]
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
463 \lstinputlisting[label=src:exec_tail, caption=tail の実行例] {src/exec_tail_in_haskell.txt}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
464 \end{table}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
465
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
466 tail (fmap even list) と fmap even (tail list) の型が同じように List Bool であり、値も等しいことが分かる。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
467 なお、 tail は同一名の関数が既に定義されているため、 Main.tail として名前を指定している。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
468 List の値を変換してから先頭を除いても、List の先頭を除いてから値を変換しても結果が同じであることは直感的にも正しいように思える。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
469
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
470 これがプログラムにおける natural transformation である。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
471
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
472 図で表すと、図\ref{fig:natural_transformation_in_program}のような可換図となり、これは可換である。
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
473
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
474 \begin{figure}[htbp]
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
475 \begin{center}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
476 \includegraphics[scale=1.0]{fig/natural_transformation_in_haskell.pdf}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
477 \caption{natural transformation tail の可換図}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
478 \label{fig:natural_transformation_in_program}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
479 \end{center}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
480 \end{figure}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
481
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
482 % }}}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
483
22
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
484 % {{{ Monads in Functional Programming
21
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
485
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
486 \section{Monads in Functional Programming}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
487 \label{section:monads_in_program}
7d94faaeb448 Add natural transformation in program
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
488
22
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
489 \ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べた。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
490 \ref{section:monads_in_program}節ではプログラムにおける Monad について述べる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
491
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
492 Monad とは 図\ref{fig:monad_laws}の可換図を満たす $ triple (T, \eta, \mu) $ であった。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
493 T は functorであり、$ \eta $ は $ A \rightarrow T A $ 、 $ \mu $ は $ T^2 A \rightarrow T $ の natural transformation であった。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
494
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
495 Haskell において functor は型引数を持つ型とfmapで表現され、 natural transformation は図\ref{fig:natural_transformation}の可換図を満たす関数であった。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
496 つまり、型と fmap、2つの関数を適切に定義することによって表現される。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
497
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
498 Haskell において、 $ \eta $ と $ \mu $ の型は以下のようになる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
499
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
500 \begin{itemize}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
501 \item eta : \verb/A -> T A/
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
502
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
503 ここで、 T は functor である型引数を持つ型
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
504
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
505 \item mu : \verb/T (T A) -> T A/
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
506
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
507 本来の $ \mu $ は $ T^2 \rightarrow T $ であるため、 T によって2度 mapping された値から T によって mapping された値への関数になる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
508 \end{itemize}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
509
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
510 Monad 則により、Tに対する演算は単位元のように振る舞わせることと、演算の可換性を持つ。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
511 ここでメタ計算を T に対する演算として定義する。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
512 そうすることで、型Aを持つ値に対する計算から functor Tにより T の計算へと変換し、メタ計算部分は T に対する演算として行なうことで任意のAに対応するメタ計算を行なうことができるようになる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
513 これがプログラムにおける monad を通したデータ型とメタ計算の対応である。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
514 そして、 Monad 則はメタ計算をTに対して $ \eta $ と $ \mu $ で定義する際に満たすべき制約として機能する。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
515
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
516 Haskell において List は monad としても振る舞う。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
517 List は nondeterminism (非決定性)を表現するデータ構造である。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
518 List に対する演算を行なう際、結果としてありうる値を全て列挙することにより非決定性を表現しようとするものである。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
519
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
520 List において非決定性を表現する時、$ \eta $ は通常の値から List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
521 $ \mu $ で何故非決定性を表現できるかと述べる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
522 まず、List a と、 a から List a を返す関数を考える。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
523 List a がありうる値の集合で、関数が値から取りうる値を計算して返すものだとする。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
524 List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
525 この際、 List a に対して a から List a を返す関数を適用するために List a を持つ List が構築される。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
526 ネストされた List を、全ての取りうる値として通常の List に戻すために concat を用いる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
527
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
528 ここで、Haskell における monad の型クラスを振り返る(リスト\ref{src:monad_class})。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
529 Haskell においては monad は Monad 型クラスとして提供されているが、$ \eta $ と $ \mu $ による記述はされていない。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
530 これは、Haskell がメタ計算との対応として Kleisli Category の triple を採用しているからである。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
531 monad と Kleisli category は互いに同型であるために相互に変換することができる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
532 また、 category や program の文脈が変わることで $ \eta $ を unit と呼んだり、 $ \mu $ を join と呼んだり、 \verb/>>=/ を bind と呼んだりする。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
533 しかし今までの解説には $ \eta $ と $ \mu $ を用いているために、このまま $ \eta $ と $ \mu $ で解説していくこととする。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
534
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
535 なお、monad と Kleisli triple との変換は Haskell においてはリスト \ref{src:monad_and_bind} のようになる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
536
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
537 \begin{table}[html]
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
538 \lstinputlisting[label=src:monad_and_bind, caption=Haskell における monad と Kleisli triple との変換] {src/monad_and_bind.hs}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
539 \end{table}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
540
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
541 では List を用いて非決定性を表現した例を示す。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
542
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
543 まずは List を monad とする(リスト\ref{src:list_monad})。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
544
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
545 \begin{table}[html]
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
546 \lstinputlisting[label=src:list_monad, caption= Haskell における List に対する monad の定義] {src/list_monad.hs}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
547 \end{table}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
548
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
549 先程述べたように、 $ \eta $ は値を List とする関数、 $ \mu $ はList を内包する List を全て結合する関数である。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
550
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
551 この List Monad を実行する。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
552 まずはありうる値のリストとして100, 200, 400 を持つ List の x を考える。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
553 次に、値から取りうる計算結果を返す関数として f を定義する。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
554 取りうる計算結果として、1加算した結果、10加算した結果、2乗した結果が存在するとし、結果は List として返す。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
555
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
556 この x と f から全ての取りうる値を計算した結果がリスト\ref{src:exec_list_monad}である。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
557
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
558 \begin{table}[html]
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
559 \lstinputlisting[label=src:exec_list_monad, caption= Haskell において List を monad として実行した例] {src/exec_list_monad.txt}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
560 \end{table}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
561
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
562 3つのありうる値に対して、取りうる3つの計算結果から生成された9つの値が全て計算されている。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
563 このように、ある性質を持つデータ型と、そのデータ型を返す関数の演算によって通常の計算に加えてメタ計算を実現することができた。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
564
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
565 これがプログラムにおける Monad であり、結果としてメタ計算とデータ型の対応が得られる。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
566
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
567 なお、 Haskell においても Monad 則は存在し、リスト\ref{src:monad_laws_in_haskell}の性質を満たすよう $ \eta $ や $ \mu $ を定義しなくてはならない。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
568
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
569 \begin{table}[html]
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
570 \lstinputlisting[label=src:monad_laws_in_haskell, caption=Haskell における Monad 則] {src/monad_laws_in_haskell.hs}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
571 \end{table}
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
572
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
573 1つめの則が図\ref{fig:monad_laws}における左側の可換図に対応し、Tに対する演算の可換性を示す。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
574 2つめの則が図\ref{fig:monad_laws}における右側の可換図に対応し、Tに対する演算における単位元のような振舞いを強制する。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
575 3つめの則が eta に対する natural transformation の要請であり、4つめの則が mu に対する natural transformation の要請である。
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
576
fc44782929a7 Add monad in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
577 % }}}