Mercurial > hg > Papers > 2015 > atton-thesis

annotate functional_programming.tex @ 50:37a832dff044

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add DeltaM example
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 17:56:51 +0900
parents 113b49263d40
children bf136bd59e7a
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
33
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{Monads in Functional Programming}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 \label{chapter:functional_programming}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 第\ref{chapter:category} 章では category による Monad の定義を述べた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 第\ref{chapter:functional_programming}章ではプログラミングにおける Monad について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 プログラムがなす category と functor, natural transformation を定義し、Monad を用いたデータとメタ計算との対応について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 % {{{ Category
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 \section{Category}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \label{section:category_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 \ref{section:monad}節では Monad の定義について述べた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 これからプログラムにおける Monad について述べていく。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 そのために\ref{section:category_in_program}節はプログラムと category の対応について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 プログラムには値と関数のみが存在するとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 任意の値は型付けられるとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 変数x が型 A を持つ時、式\ref{exp:value_in_program}のように記述する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 \begin{equation}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 \label{exp:value_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 x : A
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 \end{equation}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 関数は値を受けとり値を返すものとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 A を取り B を返す関数f の型は式\ref{exp:function_in_program}のように記述する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 \begin{equation}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 \label{exp:function_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 f : A \rightarrow B
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 \end{equation}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 そして、引数と返り値の型が等しい関数は関数結合できるとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 関数結合の記号には $ \circ $ を用いる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 例えば、 A を取り B を返す関数 f と B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 \begin{eqnarray}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 \label{exp:function_compose_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 f : A \rightarrow B \\ \nonumber
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 g : B \rightarrow C \\ \nonumber
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 g \circ f : A \rightarrow C
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 \end{eqnarray}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 この時、型を object とし、関数を morphism とする category が構成できる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 この category が category が満たすべき法則を満たしているか確認する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 \begin{itemize}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 \item 全ての object について identity mapping が存在する
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 任意の型 A に対し $ A \rightarrow A $ である関数 id が定義できれば identitiy mapping が存在することになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 任意の型の値x を受けとり、その値を返す関数が id となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 morpshim は関数である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 つまり domain は引数の型であり、 codomain は返り値の型となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 morphism の合成は関数合成に相当し、合成の順序によらず引数と返り値の型は同じとなる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 \end{itemize}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 プログラムに対応する category が構成できた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 特に例として用いているプログラミング言語 Haskell では値と関数は型を持つため、 category との対応が分かりやすい。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 よって例題には Haskell のプログラムを用いることとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 % }}}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 % {{{ Functor
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 \section{Functor}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 \label{section:functor_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 \ref{section:category_in_program}節ではプログラムとcategoryが対応していることを述べた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 \ref{section:functor_in_program}節ではプログラムにおけるfunctor について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 プログラムにおけるfunctor は型引数を持つことのできるデータ型に対応する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 型引数を持つデータ型とは、任意のデータ型に対して構成可能なデータ構造であり、List などが相当する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 たとえば、List は数値の List であっても Bool の List であっても構成可能である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 この List を、型を受けとり型を返す型であると考えると、渡す型が引数のように振る舞う。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 この引数が型引数である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 \begin{eqnarray}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 \label{exp:functor_type}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 A : Type \\ \nonumber
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 List A : Type \\ \nonumber
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 List : Type \rightarrow Type
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 \end{eqnarray}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 つまり、型と関数から構成される category から List 型と List に対応する関数からなる category へと置きかえるような functor が存在すれば良い。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 Haskell では functor はリスト \ref{src:functor_in_haskell} のように型クラスとして提供される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 \lstinputlisting[label=src:functor_in_haskell, caption=Haskell における Functor の定義] {src/functor_class.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 functor であることを保証したい型は f として表される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 そしてデータ型が functor であることを示すためには、 fmap という関数を定義すれば良いことが分かる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 fmap は型a から型bへの関数を取り、f a を取り f b を返す。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 つまり、f でない型への演算をfの型においても適用するために変換する関数である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 morpshim は関数であるため、 $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っていることが分かる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 よって morphism を morphism へと mapping することができるため functor となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 functor の例として、型がInt である変数 x と Int から Bool を返す even 関数を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 このプログラムがなす category C は object が Int であり、 morphism が show となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 category C を functor によって別の category に写すことができる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 例えば List がなす category がある。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 まずHaskell において List を定義する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 List は任意の型 a を取り、 List a とする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 空の List は Nil とし、List a に対して a の値を Cons で追加することによって List を構築するとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 ここで List が Functor であると定義する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 fmap は a を取りbを返す関数を取り、List a を取って List b を返す関数である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 つまり、関数を取ってList の全ての要素に適用することで実現できる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 定義した結果がリスト\ref{src:list_in_haskell} である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 \lstinputlisting[label=src:list_in_haskell, caption=Haskell におけるListの例] {src/list.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 Int型を持つ値x と、Intから Bool返す関数 even を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 even を x に適用すると Bool となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 この際、x を持つ List の型は List Int であり、 fmap によって even を List Int に適用すると List Bool となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 Haskell における実行結果はリスト\ref{src:exec_list_in_haskell} のようになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 \lstinputlisting[label=src:exec_list_in_haskell, caption=Haskell における List の実行例] {src/exec_list_in_haskell.txt}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 なお、 Haskell において型Aを持つ値xは $ x :: A $ のように記述される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 x と even からなるプログラムから、型List と fmap を用いることにより List におけるプログラムでも同じように Bool が得られる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 これを通常のプログラムから List のプログラムへの functor とみなす。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 このように、型引数を持つ型とfmapによる関数の変換を定義することによってプログラムにおける functor を実現する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 可換図で表現すると図\ref{fig:functor_in_haskell}となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 \begin{figure}[htbp]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 \begin{center}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 \includegraphics[scale=0.8]{fig/functor_in_haskell.pdf}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 \caption{Haskell における Functor の例がなす可換図}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 \label{fig:functor_in_haskell}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 \end{center}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 \end{figure}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 functor の定義にあたり、\ref{section:functor}節で示したように Functor則を満たすようにデータ型と fmap を定義しなくてはならない。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 Haskell における Functor則はリスト\ref{src:functor_laws_in_haskell}のように表される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 \lstinputlisting[label=src:functor_laws_in_haskell, caption=Haskellにおける Functor則] {src/functor_laws_in_haskell.txt}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 1行目がid の保存に、2行目が関数の合成の保存に対応している。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 なお、 Haskell における関数合成は \verb/./ によって行なわれる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 % }}}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 % {{{ Natural Transformation
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 \section{Natural Transformation}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 \label{section:natural_transformation_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 \ref{section:functor_in_program}節ではプログラムにおける functor を定義した。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 \ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 natural transformation は functor と functor 間の変換である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 プログラムにおいて functor は型引数を持つデータ構造であったため、データ構造からデータ構造への変換となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 natural transformationは図\ref{fig:natural_transformation}で示したような可換図が可換になるような t であった。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 プログラムにおける natural transformation は t は図\ref{fig:natural_transformation}を満たすような関数として表現される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 \lstinputlisting[label=src:natural_transformation_in_haskell, caption=List の先頭を除いた List を返す tail 関数] {src/natural_transformation_list.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 100, 200, 300 の数値を持つ List Int を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 この List が functor f に相当する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 Int を取り Bool を返す関数 even を fmap により適用すると List Bool が得られる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 ここで natural transformation tail を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193 tail は List a から List a への関数であるため、 functor f,g は両方とも List である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 natural transformation の定義から、 tail を行なってから fmap even しても、 fmap even を行なってら tail を行なっても結果が同じであれば良い。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 実行した結果がリスト\ref{src:exec_tail}である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 \lstinputlisting[label=src:exec_tail, caption=tail の実行例] {src/exec_tail_in_haskell.txt}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 tail (fmap even list) と fmap even (tail list) の型が同じように List Bool であり、値も等しいことが分かる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 なお、 tail は同一名の関数が既に定義されているため、 Main.tail として名前を指定している。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 List の値を変換してから先頭を除いても、List の先頭を除いてから値を変換しても結果が同じであることは直感的にも正しいように思える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 これがプログラムにおける natural transformation である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 図で表すと、図\ref{fig:natural_transformation_in_program}のような可換図となり、これは可換である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209 \begin{figure}[htbp]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 \begin{center}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
211 \includegraphics[scale=1.0]{fig/natural_transformation_in_haskell.pdf}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
212 \caption{natural transformation tail の可換図}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
213 \label{fig:natural_transformation_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214 \end{center}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 \end{figure}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 % }}}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 % {{{ Monad
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221 \section{Monad}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222 \label{section:monads_in_program}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
223
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 \ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
225 \ref{section:monads_in_program}節ではプログラムにおける Monad について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
226
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
227 Monad とは 図\ref{fig:monad_laws}の可換図を満たす $ triple (T, \eta, \mu) $ であった。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
228 T は functorであり、$ \eta $ は $ A \rightarrow T A $ 、 $ \mu $ は $ T^2 A \rightarrow T $ の natural transformation であった。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
229
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
230 Haskell において functor は型引数を持つ型とfmapで表現され、 natural transformation は図\ref{fig:natural_transformation}の可換図を満たす関数であった。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
231 つまり、型と fmap、2つの関数を適切に定義することによって表現される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
233 Haskell において、 $ \eta $ と $ \mu $ の型は以下のようになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
234
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
235 \begin{itemize}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
236 \item eta : \verb/A -> T A/
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
237
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
238 ここで、 T は functor である型引数を持つ型
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
239
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
240 \item mu : \verb/T (T A) -> T A/
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
241
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
242 本来の $ \mu $ は $ T^2 \rightarrow T $ であるため、 T によって2度 mapping された値から T によって mapping された値への関数になる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
243 \end{itemize}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
244
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
245 Monad 則により、Tに対する演算は単位元のように振る舞わせることと、演算の可換性を持つ。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
246 ここでメタ計算を T に対する演算として定義する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
247 そうすることで、型Aを持つ値に対する計算から functor Tにより T の計算へと変換し、メタ計算部分は T に対する演算として行なうことで任意のAに対応するメタ計算を行なうことができるようになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
248 これがプログラムにおける monad を通したデータ型とメタ計算の対応である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
249 そして、 Monad 則はメタ計算をTに対して $ \eta $ と $ \mu $ で定義する際に満たすべき制約として機能する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
250
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
251 Haskell において List は monad としても振る舞う。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
252 List は nondeterminism (非決定性)を表現するデータ構造である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
253 List に対する演算を行なう際、結果としてありうる値を全て列挙することにより非決定性を表現しようとするものである。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
254
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
255 List において非決定性を表現する時、$ \eta $ は通常の値から List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
256 $ \mu $ で何故非決定性を表現できるかと述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
257 まず、List a と、 a から List a を返す関数を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
258 List a がありうる値の集合で、関数が値から取りうる値を計算して返すものだとする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
259 List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
260 この際、 List a に対して a から List a を返す関数を適用するために List a を持つ List が構築される。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
261 ネストされた List を、全ての取りうる値として通常の List に戻すために concat を用いる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
262
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
263 ここで、Haskell における monad の型クラスを振り返る(リスト\ref{src:monad_class})。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
264 Haskell においては monad は Monad 型クラスとして提供されているが、$ \eta $ と $ \mu $ による記述はされていない。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
265 これは、Haskell がメタ計算との対応として Kleisli Category の triple を採用しているからである。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
266 monad と Kleisli category は互いに同型であるために相互に変換することができる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
267 また、 category や program の文脈が変わることで $ \eta $ を unit と呼んだり、 $ \mu $ を join と呼んだり、 \verb/>>=/ を bind と呼んだりする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
268 しかし今までの解説には $ \eta $ と $ \mu $ を用いているために、このまま $ \eta $ と $ \mu $ で解説していくこととする。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
269
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
270 なお、monad と Kleisli triple との変換は Haskell においてはリスト \ref{src:monad_and_bind} のようになる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
271
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
272 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
273 \lstinputlisting[label=src:monad_and_bind, caption=Haskell における monad と Kleisli triple との変換] {src/monad_and_bind.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
274 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
275
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
276 では List を用いて非決定性を表現した例を示す。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
277
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
278 まずは List を monad とする(リスト\ref{src:list_monad})。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
279
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
280 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
281 \lstinputlisting[label=src:list_monad, caption= Haskell における List に対する monad の定義] {src/list_monad.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
282 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
283
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
284 先程述べたように、 $ \eta $ は値を List とする関数、 $ \mu $ はList を内包する List を全て結合する関数である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
285
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
286 この List Monad を実行する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
287 まずはありうる値のリストとして100, 200, 400 を持つ List の x を考える。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
288 次に、値から取りうる計算結果を返す関数として f を定義する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
289 取りうる計算結果として、1加算した結果、10加算した結果、2乗した結果が存在するとし、結果は List として返す。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
290
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
291 この x と f から全ての取りうる値を計算した結果がリスト\ref{src:exec_list_monad}である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
292
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
293 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
294 \lstinputlisting[label=src:exec_list_monad, caption= Haskell において List を monad として実行した例] {src/exec_list_monad.txt}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
295 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
296
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
297 3つのありうる値に対して、取りうる3つの計算結果から生成された9つの値が全て計算されている。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
298 このように、ある性質を持つデータ型と、そのデータ型を返す関数の演算によって通常の計算に加えてメタ計算を実現することができた。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
299
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
300 これがプログラムにおける Monad であり、結果としてメタ計算とデータ型の対応が得られる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
301
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
302 なお、 Haskell においても Monad 則は存在し、リスト\ref{src:monad_laws_in_haskell}の性質を満たすよう $ \eta $ や $ \mu $ を定義しなくてはならない。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
303
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
304 \begin{table}[html]
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
305 \lstinputlisting[label=src:monad_laws_in_haskell, caption=Haskell における Monad 則] {src/monad_laws_in_haskell.hs}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
306 \end{table}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
307
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
308 1つめの則が図\ref{fig:monad_laws}における左側の可換図に対応し、Tに対する演算の可換性を示す。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
309 2つめの則が図\ref{fig:monad_laws}における右側の可換図に対応し、Tに対する演算における単位元のような振舞いを強制する。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
310 3つめの則が eta に対する natural transformation の要請であり、4つめの則が mu に対する natural transformation の要請である。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
311
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
312 % }}}
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
313