\chapter{プログラムの変更を表現する Delta Monad}
\label{chapter:delta}

Monad を用いてプログラムの変更を形式化していく。
第\ref{chapter:delta}章ではプログラムの変更を表す Delta Monad を定義し、その使用例とメタ計算の例を示す。
なお、Monad についての定義と解説は第\ref{chapter:category}章と第\ref{chapter:functional_programming}章にて行なう。

% {{{ Monad とメタ計算
\section{Monad とメタ計算}
\label{section:monad_with_meta_computation}

まずはプログラムを定義する。
プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。
プログラムの実行は関数の値への適用とし、入出力といった、値や関数で表現できない計算はメタ計算とする。
メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力処理を実現する。
メタ計算とデータ構造の対応に用いる性質が Monad である。

例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。

\begin{equation}
    T A = A_{ \bot } (i.e. A + \left\{ \bot \right\})
    \label{exp:partiality}
\end{equation}

型 A の値に対応するメタ計算 T A は、A と $ \bot $ の論理和として表現できる。
計算に成功した際は型 A の値を返し、失敗した場合は $ \bot $ を返す。

ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させる。
プログラムは型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。

\begin{equation}
    g ( f ( x ))
    \label{exp:non_failure_program}
\end{equation}

ここで関数f は失敗する可能性がある時、f をメタ計算によって拡張することで失敗を実現する。

式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。
$ \bot $ となった時点で計算を中断するメタ計算を定義すれば、失敗を含めた関数を表現できる。
計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。

型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。

\begin{equation}
    g^{*} ( f^{*} ( x' ))
    \label{exp:failure_program}
\end{equation}

ここで重要な点は、元の関数 $ f $ と $g$ から $f^{*}$ と $g^{*}$ が導けることである。
メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。
このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。

% }}}

% {{{ Delta Monad の定義

\section{Delta Monad の定義}

プログラムとメタ計算の関係としての Monad について述べたところで、プログラムの変更をメタ計算として記述することを考える。

プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。
最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。

\begin{equation}
    T A = V_A
    \label{exp:meta_computation_definition}
\end{equation}

V はプログラムの全てバージョンの集合であり、$ V_A $ とすることでAに対応する値の集合を返すものとする。

式\ref{exp:meta_computation_definition}のメタ計算として、全ての変更単位で変更されたプログラムを保存する計算を提案する。
このメタ計算を Delta Monad と呼ぶ。
なお、この Delta Monadが Monad であることの証明は \ref{chapter:proof_delta} 章で行なう

% }}}

% {{{ Haskell における Delta Monad の実装例

\section{Haskell における Delta Monad の実装例}

式\ref{exp:meta_computation_definition}のメタ計算をプログラミング言語 Haskell を実装し、プログラムの変更が表現できることを示す。

まずは全てのプログラムのバージョンを表わすデータ型 Delta を考える。
Delta の定義はリスト\ref{src:delta_constructor} とする。

\begin{table}[html]
    \lstinputlisting[label=src:delta_constructor, caption=Haskellにおけるデータ型Deltaの定義]{src/delta_constructor.hs}
\end{table}

データ型 Delta はコンストラクタ Delta もしくは Mono によって構成される。
バージョンが1である値は Mono によって構成される。
プログラムを変更する際には、コンストラクタ Delta を用いて記述し、変更後の値と前のバージョンを持つ。
Delta で記述することで、プログラムの変更に沿った長さ1以上のリスト構造が構築される。
なお、a とは任意の型であり、Delta が任意の型の値に対してもデータ型を構築できることを示す。

Haskell においてメタ計算とデータ型の対応は Monad によって行なうため、 Monad という型クラスが用意されている(リスト\ref{src:monad_class})。

\begin{table}[html]
    \lstinputlisting[label=src:monad_class, caption=Haskell における Monad 型クラス]
        {src/monad_class.hs}
\end{table}

型クラスとは特定の性質を持つ型をまとめるための制約であり、制約はデータ型に対して関数の定義を要請する。
要請する関数の定義は where 句の後に記述し、関数名と型を定義する。
型クラスCが要請した関数を型 a 対してに定義することを「型aは型クラスCのインスタンスである」と言う。


型クラス Monad に属するために要請される関数は return と \verb/>>=/ である。
\verb/::/ は型注釈であり、 $ term :: type $ のように記述する。
なお、関数型は \verb/ a -> b / のように引数の型と返り値の型を \verb/->/で挟んで記述し、引数が2つ以上の関数は \verb/ a -> b ->  ... -> d / のように \verb/->/を増やす。

関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。
\verb/>>=/ は中置関数であり、left operand と right operand を取る。
left operand にメタ計算と対応された値と、right operand にメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。

データ型 Delta に対応するメタ計算を Monad を用いてリスト\ref{src:delta_instance_monad}のように定義する。

\begin{table}[html]
    \lstinputlisting[label=src:delta_instance_monad, caption=Haskell におけるデータ型Deltaとメタ計算の関連付け]
        {src/delta_instance_monad.hs}
\end{table}

\begin{itemize}
    \item 関数 return

        通常の値をメタ計算と対応させるため、値をバージョン1の値とする。
        そのためにコンストラクタ Mono を用いる。

    \item 中置関数 \verb/>>=/

        メタ計算を含んだ関数の適用である。
        通常の関数の適用に加え、バージョンを含んだ計算も行なう。
        値と関数のそれぞれにおいて同じバージョン選択し、関数を適用する。
        もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。
        もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。
        その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。
\end{itemize}

なお、中置関数 \verb/>>=/ や headDelta関数などで用いたコンストラクタによる処理の分岐はパターンマッチと呼ばれる。
Haskell ではコンストラクタごとに関数を記述することでパターンマッチを実現する。

% }}}

% {{{ Delta Monad を用いたプログラムの変更の記述例

\section{Delta Monad を用いたプログラムの変更の記述例}
\label{section:delta_example}
プログラムの変更を表現するメタ計算に対応するデータ型 Delta が記述できた。
2つのバージョンを持つプログラムを Delta によって表現した例を述べる。

まずは Delta を用いずに記述したプログラムを示す(リスト\ref{src:numberCount1})。

\begin{table}[html]
    \lstinputlisting[label=src:numberCount1, caption= numberCount バージョン1] {src/numberCount1.hs}
\end{table}

1からnの間の整数に含まれる特定の数の個数を調べるプログラム numberCount である。
このプログラムは以下の3つの関数により定義される。

\begin{itemize}
    \item generator

        1からnの間の整数を生成する関数である。
        nを渡すことにより1からnの間の整数のリストを返す。

    \item numberFilter

        数のリストから特定の数のみを絞り込む関数である。
        バージョン1では素数の数のみを絞り込む。

    \item count

        数の個数を数える関数である。
        整数はリストで与えられるため、リストの長さが個数であるとした。
\end{itemize}

ここで numberFilter 関数の定義を変更し、素数による絞り込みから偶数による絞り込みにする。
変更後の numberCount プログラムをリスト\ref{src:numberCount2}に示す。

\begin{table}[html]
    \lstinputlisting[label=src:numberCount2, caption= numberCount バージョン2] {src/numberCount2.hs}
\end{table}

変更は下線の部分で、filter する条件を isPrime から even とした。

 numberCount プログラムを Delta によって変更も含めて記述する(リスト \ref{src:delta_example})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_example, caption=Deltaを用いたプログラムの例] {src/delta_example.hs}
\end{table}

変更が無い関数 generator と count の値はバージョン1であることを示すために Mono を用いる。
変更が存在する numberFiler 関数は Delta を用いて2種類の処理を保存している。
それぞれのプログラムに対応する部分は下線で示した部分である。

これらの関数3つをMonad の \verb/=<</ によってメタ計算を含む関数呼び出しとして実行する。
中置関数 \verb/=<</ は \verb/>>=/ の左右のオペランドを交換したものである。
2つのバージョンを含めた numberCount を実行すると \ref{txt:delta_example_result}のように、全てのバージョンの結果が得られる。

\begin{table}[html]
    \lstinputlisting[label=txt:delta_example_result, caption=numberCountプログラムの実行結果] {src/delta_example_result.txt}
\end{table}

これは numberCount プログラムに1000を与えた結果である。
バージョン1の時は素数の数を求めるため計算結果は168であり、バージョン2の時は偶数の数を求めるために計算結果は500となる。
Delta によりプログラムの変更を表現し、かつ同時に実行することができた。

なお、Delta Monad はプログラムの変更に対する計算もメタ計算としてHaskellで実行している。
よってメタ計算を変更することで、変更に対する計算を任意に定義し実行する可能となった。
つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。
メタ計算を変更することでプログラムの実行時にバージョン間の挙動の比較することも可能となる。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.8]{fig/non_delta_example.pdf}
        \caption{Deltaを用いない通常のプログラムの例}
        \label{fig:non_delta_example}
    \end{center}
\end{figure}

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.8]{fig/delta_example.pdf}
        \caption{Deltaを用いたプログラムの例}
        \label{fig:delta_example}
    \end{center}
\end{figure}

% }}}

% Delta を用いた信頼性向上 {{{

\section{Delta を用いた信頼性向上}
\label{section:delta_merit}
\ref{section:delta_example}節ではプログラムの変更に対して、変更前と変更後の挙動を保存した例を述べた。
プログラムの変更形式化することによって可能となる信頼性向上手法について\ref{section:delta_merit}節で述べる。

プログラムの変更を保存することで、以下のようなことが可能となる。

\begin{itemize}

    \item 異なるバージョンを同時に実行する

        プログラムの変更列から任意のバージョン2つを取り出し、同時に実行するプログラムを構成する。
        プログラムを同時に実行することで以下のようなメリットがある。
        なお、任意の要素どうしの組み合せは category において product として表現されるため、 product と対応があると考えている。

        \begin{itemize}
            \item 実行系とサブの実行系を実行する

                例えば、あるバージョンでリリースしたプログラムがあるとする。
                変更を加え、ベータ版としてリリースしたいが動作が不安定である。
                そこで、リリースしたプログラムからベータ版への変更から、2つのプログラムが同時に動くようなプログラムを構築する。
                見掛け上は安定版として動作するが、安定版の実際の入出力を用いてベータ版をテストすることが可能となる。

            \item バージョン依存のプロトコル間で互換を持つようなプログラムが作成できる

                異なるバージョン間でプロトコルに互換が無いプログラムを考える。
                バージョン間の互換を含めてメタ計算として定義し、全てのバージョンに対して互換を持つプログラムを構築する。
                そうすることで、どのバージョンのプロトコルとも互換を持つような変換器を作成できる。

        \end{itemize}

    \item バージョン間の動作の比較

        プログラムの各バージョンにつき、挙動を示すユニークなトレースが得られるとする。
        トレースの比較をすることでバージョン間の動作を比較することができる。
        トレースの比較により以下のようなものを検出できると考えている。

        \begin{itemize}
            \item 過去のバージョンの挙動を破壊する時を検出する

                プログラムの変更の際、トレースを変えてはいけない部分を指定する。
                変更の際にトレースが保存される変更のみを受けつけるようにする。

            \item トレースが変化していないことを確認する

                プログラムの変更にはいくつかの種類がある。
                例えば機能拡張の変更などであればトレースは変化するのが正しい。
                しかしリファクタリングではプログラムが変更されてもトレースが変わらないのが望ましい。
                トレース全体が変わらないような変更のみを受けつけることにより、リファクタリングを支援することができる。
        \end{itemize}

    \item Version Control System との対応

        全ての変更を保存し、任意のバージョンを生成可能であるようなメタ計算を考える。
        そうした時、プログラムの変更を蓄積するものは git や mercurial といった Version Control System の Repository に相当すると考えられる。
        Delta により Repository を定義することがでるのならば、 branch や merge といった Version Control System の処理に対して形式的な定義を与えることができる。
        また、 category における colimit と対応があると考えている。

    \item 変更単位を用いた処理

        変更を適用する際に、特定の処理を実行することもできる。
        例えばプログラムの変更単位に対してテストを行なうことで、変更に応じてテストの結果の変動が確認できる。
        プログラム全体に対応するテストを定義し、変更の際にテストが通る変更のみ受け付けるようにすることでテストベースの信頼性を確保できる。
\end{itemize}

他にもプログラムの変更そのものを処理するプログラムを定義することもできる。
この機構を言語処理系に組込むことにより、言語の仕様にプログラムの変更方法も含めることができる。
例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を加えることが可能となる。
さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。
その処理系ではこれまでに挙げた全てのメタ計算の例を自由に使用、追加することが可能となる。

このように、プログラムの変更を形式化し、変更に基いたメタ計算を定義することで信頼性を向上できる。

% }}}