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

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

% {{{ 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 が同じobject を指す morphism のことである。
        identity mapping は id と略する。
        id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。

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

        morphism の合成には記号 $ \circ $ を用いる。
        object B から C への morphism 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 への morphism を持つ 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 である時、morphism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを 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=0.9]{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) $ に強制することとなる。

% }}}