\chapter{Monads in Functional Programming}
\label{chapter:functional_programming}
第\ref{chapter:category} 章では category による Monad の定義を述べた。
第\ref{chapter:functional_programming}章ではプログラミングにおける Monad について述べる。
プログラムがなす category と functor, natural transformation を定義し、Monad を用いたデータとメタ計算との対応について述べる。

% {{{ Category

\section{Category}
\label{section:category_in_program}
\ref{section:monad}節では Monad の定義について述べた。
\ref{section:category_in_program}節はプログラムと category の対応について述べる。

プログラムには値と関数のみが存在する。

任意の値は型付けられるとする。
変数x が型 A を持つ時、式\ref{exp:value_in_program}のように記述する。

\begin{equation}
    \label{exp:value_in_program}
    x : A
\end{equation}

関数は値を受けとり値を返すものとする。
A を取り B を返す関数f の型は式\ref{exp:function_in_program}のように記述する。

\begin{equation}
    \label{exp:function_in_program}
    f : A \rightarrow B
\end{equation}

そして、引数と返り値の型が等しい関数は関数結合できるとする。
関数結合の記号には $ \circ $ を用いる。
例えば、 A を取り B を返す関数 f と、 B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。

\begin{eqnarray}
    \label{exp:function_compose_in_program}
    f : A \rightarrow B \\ \nonumber
    g : B \rightarrow C \\ \nonumber
    g \circ f : A \rightarrow C
\end{eqnarray}

この時、型を object とし、関数を morphism とする category が構成できる。

この category が category が満たすべき法則を満たしているか確認する。

\begin{itemize}
    \item 全ての object について identity mapping が存在する

        任意の型 A に対し $ A \rightarrow A $ である関数 id が定義できれば identitiy mapping が存在することになる。
        任意の型の値x を受けとり、その値をそのまま返す関数が id となる。

    \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。

        morphism は関数である。
        つまり domain は引数の型であり、 codomain は返り値の型となる。
        morphism の合成は関数合成に相当し、合成の順序によらず引数と返り値の型は同じとなる。
\end{itemize}

プログラムに対応する category が構成できた。
特に例として用いているプログラミング言語 Haskell では値と関数は型を持つため、 category との対応が分かりやすい。
よって例題には Haskell のプログラムを用いることとする。

% }}}

% {{{ Functor

\section{Functor}
\label{section:functor_in_program}
\ref{section:category_in_program}節ではプログラムとcategoryが対応していることを述べた。
\ref{section:functor_in_program}節ではプログラムにおけるfunctor について述べる。

プログラムにおけるfunctor は型引数を持つことのできるデータ型に対応する。
型引数を持つデータ型とは、任意のデータ型に対して構成可能なデータ構造であり、List などが相当する。

たとえば、List は数値の List であっても Bool の List であっても構成可能である。
この List を、型を受けとり型を返す型であると考えると、渡す型が引数のように振る舞う。
この引数が型引数である。

\begin{eqnarray}
    \label{exp:functor_type}
    A : Type       \\ \nonumber
    List A : Type  \\ \nonumber
    List : Type \rightarrow Type
\end{eqnarray}

つまり、型と関数から構成される category から List 型と List に対応する関数からなる category へと置きかえるような functor が存在すれば良い。

Haskell では functor はリスト \ref{src:functor_in_haskell} のように型クラスとして提供される。

\begin{table}[html]
    \lstinputlisting[label=src:functor_in_haskell, caption=Haskell における Functor の定義] {src/functor_class.hs}
\end{table}

functor であることを保証したい型は f として表される。
そしてデータ型が functor であることを示すためには、 fmap という関数を定義すれば良いことが分かる。
fmap は型a から型bへの関数を取り、f a を取り f b を返す。
つまり、f でない型への演算をfの型においても適用するために変換する関数である。
プログラムにおいて morpshim は関数であるため、fmap は $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っている。
なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。

また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。
ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。
よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。

functor の例として、型がInt である変数 x と Int から Bool を返す even 関数を考える。
このプログラムがなす category C は object が Int であり、 morphism が even となる。
category C を functor によって別の category に写すことができる。

例えば List がなす category Dがある。

まずHaskell において List を定義する。
List は任意の型 a を取り、 List a とする。
空の List は Nil とし、List a に対して a の値を Cons で追加することによって List を構築するとする。

ここで List が Functor であると定義する。
fmap は a を取りbを返す関数を取り、List a を取って List b を返す関数である。
つまり、関数を取ってList の全ての要素に適用することで実現できる。

定義した結果がリスト\ref{src:list_in_haskell} である。

\begin{table}[html]
    \lstinputlisting[label=src:list_in_haskell, caption=Haskell におけるListの例] {src/list.hs}
\end{table}

Int型を持つ値x と、Intから Bool返す関数 even を考える。
even を x に適用すると Bool となる。

この際、x を持つ List の型は List Int であり、 fmap によって even を List Int に適用すると List Bool となる。
Haskell における実行結果はリスト\ref{src:exec_list_in_haskell} のようになる。

\begin{table}[html]
    \lstinputlisting[label=src:exec_list_in_haskell, caption=Haskell における List の実行例] {src/exec_list_in_haskell.txt}
\end{table}

x と even からなるプログラムから、型List と fmap を用いることにより List におけるプログラムでも同じように Bool が得られる。
これを通常のプログラムから List のプログラムへの functor とみなす。

このように、型引数を持つ型とfmapによる関数の変換を定義することによってプログラムにおける functor を実現する。
可換図で表現すると図\ref{fig:functor_in_haskell}となる。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.8]{fig/functor_in_haskell.pdf}
        \caption{Haskell における Functor の例がなす可換図}
        \label{fig:functor_in_haskell}
    \end{center}
\end{figure}

functor の定義にあたり、\ref{section:functor}節で示したように Functor則を満たすようにデータ型と fmap を定義しなくてはならない。

Haskell における Functor則はリスト\ref{src:functor_laws_in_haskell}のように表される~\cite{JonesDuponcheel93}。

\begin{table}[html]
    \lstinputlisting[label=src:functor_laws_in_haskell, caption=Haskellにおける Functor則] {src/functor_laws_in_haskell.txt}
\end{table}

1行目がid の保存に、2行目が関数の合成の保存に対応している。
なお、 Haskell における関数合成は \verb/./ によって行なわれる。

% }}}

% {{{ Natural Transformation

\section{Natural Transformation}
\label{section:natural_transformation_in_program}
\ref{section:functor_in_program}節ではプログラムにおける functor を定義した。
\ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べる。

natural transformation は functor と functor 間の変換である。
プログラムにおいて functor は型引数を持つデータ構造であったため、データ構造からデータ構造への変換となる。

natural transformationは図\ref{fig:natural_transformation}で示したような可換図が可換になるような t であった。
つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。

プログラムにおける natural transformation t は図\ref{fig:natural_transformation}を満たすような関数として表現される。
Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。

List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。
tail 関数を Functor List から Functor List への natural transformation とみなすのである。

\begin{table}[html]
    \lstinputlisting[label=src:natural_transformation_in_haskell, caption=List の先頭を除いた List を返す tail 関数] {src/natural_transformation_list.hs}
\end{table}

100, 200, 300 の数値を持つ List Int を考える。
この List が functor f に相当する。
Int を取り Bool を返す関数 even を fmap により適用すると List Bool が得られる。

ここで natural transformation tail を考える。
tail は List a から List a への関数であるため、 functor f,g は両方とも List である。
natural transformation の定義から、 tail を行なってから fmap even しても、 fmap even を行なってら tail を行なっても結果が同じであれば良い。
実行した結果がリスト\ref{src:exec_tail}である。

\begin{table}[html]
    \lstinputlisting[label=src:exec_tail, caption=tail の実行例] {src/exec_tail_in_haskell.txt}
\end{table}

tail (fmap even list) と fmap even (tail list) の型が同じように List Bool であり、値も等しいことが分かる。
なお、 tail は同一名の関数が既に定義されているため、 Main.tail として名前を指定している。
List の値を変換してから先頭を除いても、List の先頭を除いてから値を変換しても結果が同じであることは直感的にも正しいように思える。

これがプログラムにおける natural transformation である。

図で表すと、図\ref{fig:natural_transformation_in_program}のような可換図となり、これは可換である。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=1.0]{fig/natural_transformation_in_haskell.pdf}
        \caption{natural transformation tail の可換図}
        \label{fig:natural_transformation_in_program}
    \end{center}
\end{figure}

% }}}

% {{{ Monad

\section{Monad}
\label{section:monads_in_program}

\ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べた。
\ref{section:monads_in_program}節ではプログラムにおける Monad について述べる。

Monad とは 図\ref{fig:monad_laws}の可換図を満たす $ triple (T, \eta, \mu) $ であった。
T は functorであり、$ \eta $ は $ A \rightarrow T A $ 、 $ \mu $ は $ T^2 A \rightarrow T $ の natural transformation であった。

Haskell において functor は型引数を持つ型とfmapで表現され、 natural transformation は図\ref{fig:natural_transformation}の可換図を満たす関数であった。
つまり、型と fmap、2つの関数を適切に定義することによって表現される。

Haskell において、 $ \eta $ と $ \mu $ の型は以下のようになる。

\begin{itemize}
    \item eta : \verb/A -> T A/

        ここで、 T は functor である型引数を持つ型

    \item mu : \verb/T (T A) -> T A/

        本来の $ \mu $ は $ T^2 \rightarrow T $ であるため、 T によって2度 mapping された値から T によって mapping された値への関数になる。
\end{itemize}

Monad 則により、Tに対する演算は単位元のように振る舞わせることと、演算の可換性を持つ。
ここでメタ計算を T に対する演算として定義する。
そうすることで、型Aを持つ値に対する計算から functor Tにより T の計算へと変換し、メタ計算部分は T に対する演算として行なうことで任意のAに対応するメタ計算を行なうことができるようになる。
これがプログラムにおける monad を通したデータ型とメタ計算の対応である。
そして、 Monad 則はメタ計算をTに対して $ \eta $ と $ \mu $ で定義する際に満たすべき制約として機能する。

Haskell において List は monad としても振る舞う。
List は nondeterminism (非決定性)を表現するデータ構造である。
List に対する演算を行なう際、結果としてありうる値を全て列挙することにより非決定性を表現しようとするものである。

List において非決定性を表現する時、$ \eta $ は値から長さ1の List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。

この $ \eta $ と $ \mu $ を用いて非決定性を表現する。
List a はありうる値の集合であるとする。
関数は値を取り、値から取りうる値をList として返す。
この関数を List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。
この際、 List a に対して a から List a を返す関数を適用するために List a を持つ List が構築される。
ネストされた List を、全ての取りうる値として通常の List に戻すために concat を用いる。
concat することで、値と関数から全ての取りうる値が計算できた。

ここで concat は ネストした List から List への関数であるため、 $ TT A \rightarrow T A $ に相当する $ \mu $ となっている。
$ \eta $ は長さ1の List を返すため、 $ A \rightarrow T A $ となっている。
このように、非決定性演算は List データ型と $ \eta $ と $ \mu $ として Monad を用いて定義できる。

Haskell における monad の型クラスを振り返る(リスト\ref{src:monad_class})。
Haskell においては monad は Monad 型クラスとして提供されているが、$ \eta $ と $ \mu $ による記述はされていない。
これは、Haskell がメタ計算との対応として Kleisli Category の triple を採用しているからである。
monad と Kleisli triple は互いに同型であるために相互に変換することができる。
また、 category や program の文脈が変わることで $ \eta $ を unit と呼んだり、 $ \mu $ を join と呼んだり、 \verb/>>=/ を bind と呼んだりする。
しかし今までの解説には $ \eta $ と $ \mu $ を用いているために、このまま $ \eta $ と $ \mu $ で解説していくこととする。

なお、monad と Kleisli triple との変換は Haskell においてはリスト \ref{src:monad_and_bind} のようになる。

\begin{table}[html]
    \lstinputlisting[label=src:monad_and_bind, caption=Haskell における monad と Kleisli triple との変換] {src/monad_and_bind.hs}
\end{table}

では List を用いて非決定性を表現した例を示す。

まずは List を Monad 型クラスのインスタンスとする(リスト\ref{src:list_monad})。

\begin{table}[html]
    \lstinputlisting[label=src:list_monad, caption= Haskell における List に対する monad の定義] {src/list_monad.hs}
\end{table}

先程述べたように、 $ \eta $ は値を List とする関数、 $ \mu $ はList を内包する List を全て結合する関数である。

この List Monad を実行する。
まずはありうる値のリストとして100, 200, 400 を持つ List の x を考える。
次に、値から取りうる計算結果を返す関数として f を定義する。
取りうる計算結果として、1加算した結果、10加算した結果、2乗した結果が存在するとし、結果は List として返す。

この x と f から全ての取りうる値を計算した結果がリスト\ref{src:exec_list_monad}である。

\begin{table}[html]
    \lstinputlisting[label=src:exec_list_monad, caption= Haskell において List を monad として実行した例] {src/exec_list_monad.txt}
\end{table}

3つのありうる値に対して、取りうる3つの計算結果から生成された9つの値が全て計算されている。
このように、ある性質を持つデータ型と、そのデータ型を返す関数の演算によって通常の計算に加えてメタ計算を実現することができた。

これがプログラムにおける Monad であり、結果としてメタ計算とデータ型の対応が得られる。

なお、 Haskell においても Monad 則は存在し、リスト\ref{src:monad_laws_in_haskell}の性質を満たすよう $ \eta $ や $ \mu $ を定義しなくてはならない。

\begin{table}[html]
    \lstinputlisting[label=src:monad_laws_in_haskell, caption=Haskell における Monad 則] {src/monad_laws_in_haskell.hs}
\end{table}

1つめの則が図\ref{fig:monad_laws}における左側の可換図に対応し、Tに対する演算の可換性を示す。
2つめの則が図\ref{fig:monad_laws}における右側の可換図に対応し、Tに対する演算における単位元のような振舞いを強制する。
3つめの則が eta に対する natural transformation の要請であり、4つめの則が mu に対する natural transformation の要請である。

% }}}