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

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

\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}



そして2つの法則を満たす。
\begin{itemize}
    \item 全ての object について identity mapping が存在する

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

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

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

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

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

        \begin{eqnarray}
            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
            \label{exp:morphism_composition_law}
        \end{eqnarray}
\end{itemize}

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

% TODO: simple category figure


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

% TODO: morphism_composition_law


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


\section{Functor}
\section{Natural Transformation}
\section{Monad}
\section{Monads in Functional Programming}