view delta_with_monad.tex @ 57:5f0e13923cfd

Fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 16 Feb 2015 16:24:42 +0900
parents 43213dcf8d24
children
line wrap: on
line source

\chapter{任意の Monad と Delta の組み合せ}
\label{chapter:delta_with_monad}
第\ref{chapter:proof_delta}章ではプログラムの変更を表現する Delta Monad が Monad であることを証明した。
第\ref{chapter:delta_with_monad}章では、Delta Monad と、他の Monad との組み合せを考える。
特に他の Monad のメタ計算も同時に実行できるようなデータ DeltaM を定義し、利用例を示す。

% {{{ Monad と組み合せた Delta である DeltaM

\section{Monad と組み合せた Delta である DeltaM}
\label{section:deltaM}
functional programming における monad とはデータ構造をメタ計算の対応付けであった。
プログラミング言語 Haskell においては入出力や非決定性演算といった処理が monad として提供される。
そのため、プログラムの変更を表現する Delta Monad では他の monad と組み合せることが可能でなくてはならない。
Delta Monad を拡張し、Delta Monad の内部の monad のメタ計算を実行するデータ型 DeltaM を Haskell で定義する。

データ型 DeltaM と、DeltaM に対する Monad の instance 定義を示す(リスト\ref{src:deltaM_definition})。

\begin{table}[html]
    \lstinputlisting[label=src:deltaM_definition,
                     caption= DeltaM の定義と Monad の instance 定義,
                     escapechar=&]
                     {src/deltaM_definition.hs}
\end{table}

データ型 DeltaM は2つの型引数を持つ。
型引数a と型引数を持つ型引数 m である。
m が Monad であり、 a が Monad が内包する型を表す。
m a 型を内部に持つ Delta から DeltaM コンストラクタを用いて DeltaM 型を構成できる。
型名とコンストラクタ名が同一になっているので注意が必要である。

次にいくつかの関数を定義する。
unDeltaM は DeltaM から Delta へと戻す関数である。
headDeltaM はDeltaM から先頭の値を取り出す。
バージョン管理された Delta から最新のバージョンを取り出すことに相当する。
tailDeltaM はDeltaM から先頭の値を取り除く。
これはバージョン管理された Delta から最新以外のバージョンに対して処理を行う時に用いる。

DeltaM の instance 定義では \verb/>>=/ ではなく mu を介して行なう。
ここで2つの新たな記法を解説する。

\begin{itemize}
    \item \verb/ (Functor m) => ... /

        mu や Monad の instance 宣言に利用されている記法で、型制約を示す記号である。
        ある型 m が Functor の instance であることを示す。
        例えば、 mu に記述されている \verb/(Functor m, Monad m) => ... / は型 m が Functor と Monad の instance である時に mu に適用できることを示す。
        型制約により、型 m a は Functor である保証がつくため、 m a の値に対して fmap をかけることできる。

    \item \verb/ d@(DeltaM (Mono ...))  /

        パターンマッチにおける記法で、asパターンと呼ばれる。
        パターンマッチにおいてコンストラクタを指定したのち、全体の値を \verb/@/ の前の変数に束縛する。
        例えば \verb/ m@(Mono x) / と指定すると、 \verb/Mono x/ が m に束縛される。
        この記法を採用するメリットは、コンストラクタでパターンマッチしたものの、値はコンストラクタを含んだまま処理したい時にタイプ数を省略できることにある。
\end{itemize}

関数 mu ではDelta におけるバージョンの管理と内部の Monad のメタ計算の両方を一度に行なう。

バージョンが1であった場合は内部の DeltaM から fmap headDeltaM を用いて値を取り出し、 \verb/>>= id/ で内部の Monad のメタ計算を行なう。
同じように、バージョンが1以上であった場合は先頭のバージョンに対しメタ計算を行なってから、残りのバージョンに対して再帰的に mu を行なう。

mu が定義できたので、 DeltaM を Monad の instance とする。
m が Functor と Monad である時のみ、 DeltaM は Monad となる。

return は通常の値を内部の Monad の return でメタ計算に対応させ、バージョン1である Mono としてから DeltaM とする。
中置関数 \verb/>>=/ は fmap と mu を用いて定義する。

以上で Delta Monad と 他の Monad を組み合せるための DeltaM が定義できた。

% }}}

% {{{ DeltaM を用いたプログラムの例

\section{DeltaM を用いたプログラムの例}
\label{section:deltaM_example}
DeltaM を用いてプログラムを記述する。
今回は簡易的なプログラムのトレースとして、実行時の値を文字列として残すこととする。
Haskell では処理に対するログなどを残すための Monad として Writer という Monad を提供している。
リスト\ref{src:delta_example} で示した numberCount プログラムに対し、Writer Monad と Delta Monad を組み合せてトレースの比較を組込む(リスト\ref{src:deltaM_example})。


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

Writer と組み合せた DeltaM を DeltaWithLog 型として定義する。
型の定義には type 構文を用い、ある型の別名として再定義する。
まず、 Writer で記録する型を String の List とし、その型を DeltaLog とする。
DeltaLog を内包する DeltaM として DeltaWithLog 型定義した。

また、値を文字列のログとするために関数 returnW を定義した。
これは通常の値から DeltaLog を生成するための関数である。
tell 関数を用いてログを Writer に書き込み、値を return で保持する。

処理を簡易化するために、リストから Delta を作成する関数 deltaFromList を定義しておく。

numberCountM プログラムは numberCount プログラムとほとんど違いは無い。
以下の3つの関数の組み合せで作成されている。

\begin{itemize}
    \item generatorM

        n を取り、1から nまでのリストを返す
        バージョン1とバージョン2に違いは無い。

    \item numberCountM

        整数のリストを取り、特定の条件によって絞り込む。
        バージョン1では素数のみを絞り込み、バージョン2では偶数を絞り込む。


    \item countM

        リストを取り、その要素の個数を返す。
        バージョン1とバージョン2に違いは無い。

\end{itemize}

唯一の違いは関数が最後に返す Deltaに対して returnW 関数が適用されていることである。
returnW を用いることで簡易的な値のトレースが得られる。


実行した結果はリスト\ref{src:numberCountM_result}である。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountM_result, caption= NumberCountM プログラムの実行例] {src/numberCountM_result.txt}
\end{table}

numberCountM プログラムに対して20を与えて実行した結果である。
なお、結果は読み易いように整形してある。
ここで注目して欲しいのが、それぞれがどのような計算結果を辿ったのかを Writer が保持していることである。

2つの結果とも、まずは generatorM 関数により1から20までのリストを作る。
次に numberFilterM 関数によってフィルタされ、それぞれの結果による値が導かれる。
バージョン1では素数の個数を数えるために8であり、バージョン2では偶数の個数を数えるために10となる。

このように、Monad と組み合せることでトレースを得ることができた。
Writer 以外にも任意の Monad に対して DeltaM が Monad 則を満たす。
この証明は非常に長いので付録\ref{section:proof_deltaM}に載せるものとする。

DeltaM を定義した結果、Delta Monadと Monad を組み合せることができた。

% }}}