\chapter{Categorical Definitions of Monad}
\label{chapter:category}

\ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。
ここで Monad の定義と要請されるMonad則について述べる。
また、定義は Monad の解説に必要な部分についてのみ解説する。

% {{{ Category

\section{Category}
\label{section:category}
まずは Monad の定義に必要な Category (圏)について述べる。

category は2つの要素を持つ。

\begin{itemize}
    \item object (要素)

    \item morphism (射, arrow)

        object から object へのマッピング。

        morphism によってマップされる対象を domain と呼び、マップした先の対象を codomain と呼ぶ。
        つまり domain から codomain への object をマップするものが morphism である。
        domain A と codomain B を持つ morphism f は式\ref{exp:morphism}のように書くこととする。

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

\end{itemize}

そして category は object と moprhism に対して2つの法則を満たす。

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

        identity mapping とは domain と codomain が同じ morphism のことである。
        identity mappping は id と略する。
        id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。

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

        morphism の合成には記号 $ \circ $ を用いる。
        object B から C への morpshim f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morphism_compose}となる。

        \begin{equation}
            f \circ g : A \rightarrow C
            \label{exp:morphism_compose}
        \end{equation}

        改めて、morphism の合成の順序が結果に影響しないことを式にすると式\ref{exp:morphism_composition_law}のようになる。

        \begin{eqnarray}
            \label{exp:morphism_composition_law}
            f : C \rightarrow D \nonumber \\
            g : B \rightarrow C \nonumber \\
            h : A \rightarrow B \nonumber \\
            (f \circ g) \circ h = f \circ (g \circ h) : A \rightarrow D
        \end{eqnarray}
\end{itemize}

例えば、object A,B と A から B への moprhism を持つ category は図\ref{fig:simple_category}のようになる。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=1.0]{fig/simple_category.pdf}
        \caption{object A,B と morpshim f を持つ category}
        \label{fig:simple_category}
    \end{center}
\end{figure}

なお、id は全ての object に存在するために省略して書くことが多いため、これからは省略する。

object を点、morphism を線とした図を commutative diagram (可換図式) と呼ぶ。
ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。
例えば、式\ref{exp:morphism_composition_law}の category の commutative diagram は図\ref{fig:morphism_composition_law}のようになる。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.8]{fig/morphism_composition_law.pdf}
        \caption{式\ref{exp:morphism_composition_law} の morphism の合成法則の category がなす commutative diagram}
        \label{fig:morphism_composition_law}
    \end{center}
\end{figure}


commutative diagram が commutative である時、moprhism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。
ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。

% }}}

% {{{ Functor

\section{Functor}
\label{section:functor}
\ref{section:category} 節では category を定義した。
\ref{section:functor} 節では category から category への mapping である Functor (関手)について解説する。

functor F とはある category C から D への mapping である。
functor F を用いて category C の object もしくは morphism である x を category D の object もしくは morphism に対応させることを式\ref{exp:apply_functor}のように記述する。

\begin{equation}
    F(x)
    \label{exp:apply_functor}
\end{equation}

functor は以下の functor 則を満たす。

\begin{itemize}
    \item id を保存する

        category C における object A への id $ 1_A $ は F A においても id として振る舞う。

        \begin{equation}
            F(1_A) = 1_{F(A)}
        \end{equation}

    \item morphism の合成を保存する

        category C における morphism f g の合成を考える。
        合成された $ f \circ g $ を F により mapping することと、f と g を個別に F により mapping した後に合成した結果は同じである。

        \begin{equation}
            F(f \circ g) = F(f) \circ F(g)
        \end{equation}
\end{itemize}

functor の例を挙げる。
まず、 3つの object A,B,C と morphism f,g,h を持つ category C を考える。
category C の morphism は式\ref{exp:functor_categoryC}であるとする。

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

次に、 2 つの object A', B' と morphism f', g' を持つ category D を考える。
category D の morphism は式\ref{exp:functor_categoryD}であるとする。

\begin{eqnarray}
    \label{exp:functor_categoryD}
    f : B' \rightarrow A' \\ \nonumber
    g : A' \rightarrow B' \\ \nonumber
\end{eqnarray}

C から D への functor F は式\ref{exp:functorF}のようなものがある。

要素数が異なるため一見正しく mapping できないように思えるが、正しく Functor 則を満たしている。

\begin{eqnarray}
    \label{exp:functorF}
    F(A) = A' \\ \nonumber
    F(B) = B' \\ \nonumber
    F(C) = A' \\ \nonumber
    F(id_A) = F(id_{A'}) \\ \nonumber
    F(id_B) = F(id_{B'}) \\ \nonumber
    F(id_C) = F(id_{A'}) \\ \nonumber
    F(f) = id_{A'} \\ \nonumber
    F(g) = g' \\ \nonumber
    F(h) = f' \\ \nonumber
    F(h \circ g) = F(h) \circ F(g) = f' \circ g' = id_{A'} = F(f)
\end{eqnarray}

functor F を用いて category C を category D へと mapping した図が図\ref{fig:functor}である。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.8]{fig/functor.pdf}
        \caption{Functor の例}
        \label{fig:functor}
    \end{center}
\end{figure}

functor により category から category への mapping を考えることが可能となった。

% }}}

% {{{ Natural Transformation

\section{Natural Transformation}
\label{section:natural_transformation}
\ref{section:functor}節では category から category への mapping である functor について述べた。
\ref{section:natural_transformation}節では functor と functor の関係である Natural Transformation(自然変換)について述べる。

category C から D への functor F, G が存在する時、F から G への変換 t を考える。

t は category C の A に対し、F(A) から G(A) への変換を提供する(式\ref{exp:trans})。

\begin{equation}
    t(A) : F(A) \rightarrow G(A)
    \label{exp:trans}
\end{equation}

t が 式\ref{exp:natural_transformation}を満たす時、t を natural transformation を呼ぶ。

\begin{eqnarray}
    \label{exp:natural_transformation}
    f : A \rightarrow B \\ \nonumber
    G(f)t(A) = t(B)F(f)
\end{eqnarray}

t が natural transformation である時、 category A における A を functor F で移したのちに morphism を適用しても、 functor G で移した後に morphism を適用しても良いという可換性が得られる。
式\ref{exp:natural_transformation}の可換図は図\ref{fig:natural_transformation}となる。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=1.0]{fig/natural_transformation.pdf}
        \caption{自然変換の可換図(式\ref{exp:natural_transformation})}
        \label{fig:natural_transformation}
    \end{center}
\end{figure}

% }}}

% {{{ Monad

\section{Monad}
\label{section:monad}
\ref{section:natural_transformation}節では functor 間の可換性 natural transformation について述べた。

category, functor, natural transformation を用いて Monad を定義する。

category C における monad とは以下の性質を持つ $ triple (T, \eta, \mu) $ である。

\begin{itemize}
    \item $ T : C \rightarrow C $

        category C から C への functor T

    \item $ \eta : id_C \rightarrow T $

        C から T への natural transformation $ \eta $

    \item $ \mu : T^2 \rightarrow T $

        $ T^2 $ から $ T $ への natural transformation $ \mu $

        なお、 $ T^2 $ とは $ TT $ と同義であるとする。つまり functor T による mapping を2回行なうものである。
        回数を n 回とすることで $ T^n $ と記述する。
\end{itemize}

この $ triple (T, \eta, \mu) $ が図\ref{fig:monad_laws}の可換図を満たす。
なお、Aに対する $ \mu $ を $ \mu_A $ と記述する。
同じように A に対する $ \eta $ を $ \eta_A $ と記述する

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=1.0]{fig/monad_laws.pdf}
        \caption{$ triple (T, \eta, \mu) $ が Monad であるために満たすべき可換図}
        \label{fig:monad_laws}
    \end{center}
\end{figure}

図\ref{fig:monad_laws} で示した可換図は monad が満たすべき Monad則であり、T に対する演算の可換性を強制する。
$ \eta $ は T を1つ増やすオペレーションであり、$ \mu $ は T を 2 つから1つに減らすオペレーションである。

左側の可換図は T が 3つある場合の可換性である。
TTT に対して、 (TT)T のよう外側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても、 T(TT) のように内側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても可換であることを示す。
つまり、TTTを減らす演算は左から行なっても右から行なっても良いことを示す。

そして右側の可換図は T が1つである場合の可換性である。
T A に対して $ \eta $ を行ない TT A としてから $ \mu $ を行なっても、T A の内部の A に対して $ \eta $ を行ない TT A としてか $ \mu $ を行なっても、 T A の id と同じであることを示している。
つまり、Tに対する演算における左右の単位元となるような性質を $ triple (T, \eta, \mu) $ に強制することとなる。

% }}}

% {{{ Category in Functional Programming

\section{Category in Functional Programming}
\label{section:category_in_program}
\ref{section:monad}節では 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は合成することができ、合成の順番は結果に影響しない。

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

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

% }}}

% {{{ Functor in Functional Programming

\section{Functor in Functional Programming}
\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 は関数であるため、 $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っていることが分かる。
よって morphism を morphism へと mapping することができるため functor となる。

また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。
ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。
よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。
なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。

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

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

まず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}

なお、 Haskell において型Aを持つ値xは $ x :: A $ のように記述される。
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}のように表される。

\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/./ によって行なわれる。

% }}}

\section{Monads in Functional Programming}

プログラムにおける