\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{cprotect}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage{eclbkbox}
\usepackage{url}
%\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}

\begin{document}
\title{Modify Program by Monad}
\author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy}

% {{{ プログラムの変更を表すMonad

\section{プログラムの変更を表すMonad}
プログラムを変更するとプログラムの実行結果も変化する。
しかし、変更後のプログラムが正しい実行結果でない場合も存在する。
そこで、プログラムに対する変更をMonadとして記述する。
Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。
ひいては、プログラムを変更することの意味や性質などを解析する。

% }}}

% {{{ 限定されたプログラムの変更を表す Delta Monad

\section{限定されたプログラムの変更を表す Delta Monad}
Monad を用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。
Haskell におけるMonadとはメタ計算を内包したデータ型である。
Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。

Haskell において限定されたプログラムの変更を表すことができる Delta Monad を定義した。
Delta Monad におけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。
また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。

データ型Delta の定義を示す(図\ref{delta-monad-definition})。

% {{{ Definiton Delta

\begin{breakbox}
\verb/ data Delta a = Delta [String] a [String] a/
\caption{型変数を持つ型 Delta の定義(Haskell)}
\label{delta-monad-definition}
\end{breakbox}

% }}}

データ型 Delta は任意の型aの変数を持つことができる。
型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。
このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数 return と \verb/>>=/ を定義する必要がある(図\ref{monad-class})。

% {{{ Definiton Delta

\begin{breakbox}
\begin{verbatim}
  return :: Monad m => a -> m a
  (>>=) :: Monad m => m a -> (a -> m b) -> m b
\end{verbatim}
\caption{データ型をMonadとするために必要な関数}
\label{monad-class}
\end{breakbox}

% }}}

図\ref{monad-class} の定義は関数の型のみ記述している。
m は Monad であり、m a は任意の型 a を内包するMonadである。
return は任意の型aからm aの値を返す関数 return がある。
return は任意の型の値をMonadに内包するために利用する。
中置関数\verb/(>>=)/ はMonadの値 m a と、aを取って m b を返す関数を取り、m b の値を返す。
\verb/(>>=)/の定義がMonadに対するメタ計算の定義となる。

Delta におけるreturnと\verb/>>=/の定義を図\ref{monad-instance-delta}に示す。

% {{{ instance Monad Delta

\begin{breakbox}
\begin{verbatim}
mu (Delta lx (Delta llx x _ _)
          ly (Delta _ _ lly y)) =
    Delta (lx ++ llx) x (ly ++ lly) y

instance Monad Delta where
    return x = Delta [] x [] x
    d >>= f  = mu $ fmap f d
\end{verbatim}
\cprotect\caption{Delta に対する return と\verb/(>>=)/ の定義}
\label{monad-instance-delta}
\end{breakbox}

% }}}

return においては実行履歴が存在しない空の文字列を含んだMonadを返す。
型a の値xは2つに複製され、異なる実行結果を得るために利用する。
\verb/(>>=)/においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。

これらの関数returnと\verb/>>=/は満たすべきMonad則が存在する。
型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda\cite{agda}によって証明した。

% }}}

% {{{ Delta Monad におけるプログラムの変更例

\section{Delta Monad におけるプログラムの変更例}
変更例となるHaskellのプログラムを示す(図\ref{raw-program-before})。

% {{{ raw-program-before

\begin{breakbox}
{\scriptsize
\begin{verbatim}
generator :: Int -> [Int]
generator x = [1..x]

primeFilter :: [Int] -> [Int]
primeFilter xs = filter isPrime xs

count :: [Int] -> Int
count xs = length xs

primeCount :: Int -> Int
primeCount x = count . primeFilter . generator $ x
\end{verbatim}
}
\caption{変更前のHaskellプログラム}
\label{raw-program-before}
\end{breakbox}

% }}}


このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。
1からnまでの整数の個数を調べる primeCount 関数は3つの関数からなる。

\begin{itemize}
    \item 1 から n までの整数を返す関数 generator
    \item 整数のリストから素数である整数のみを残したリストを返す関数 primeFilter
    \item リストの中に存在する要素の個数を返す関数 count
\end{itemize}

ここで、 primeFilter 関数を変更する。
素数である整数を残すのではなく、偶数を残すようにする。
Delta Monad を使わずに primeFilter 関数を変更すると図\ref{raw-program-after}のプログラムとなる。

% {{{ raw-program-after

\begin{breakbox}
{\tt
primeFilter :: [Int] -> [Int]

primeFilter xs = filter \underline{even} xs
}
\caption{変更後の primeFilter 関数(変更点は下線)}
\label{raw-program-after}
\end{breakbox}

% }}}

プログラム(図\ref{raw-program-before})に対する図\ref{raw-program-after}の変更を Delta Monad で記述したものが図\ref{delta-program}のプログラムである。

% {{{ delta-program

\begin{breakbox}
{\scriptsize
\begin{verbatim}
generator :: Int -> Delta [Int]
generator x = let intList = [1..x] in
                  returnD intList

primeFilter :: [Int] -> Delta [Int]
primeFilter xs = let primeList    = filter isPrime xs
                     refactorList = filter even xs    in
                 returnDD primeList refactorList

count :: [Int] -> Delta Int
count xs = let primeCount = length xs in
           returnD primeCount

primeCount :: Int -> Delta Int
primeCount x = generator x >>= primeFilter >>= count
\end{verbatim}
}
\cprotect\caption{図\ref{raw-program-before}のプログラムに対する図\ref{raw-program-after}の変更を Delta Monad で記述した例}
\label{delta-program}
\end{breakbox}

% }}}

Delta Monad を用いたプログラムでは全ての関数はDelta Monadを返す関数として記述される。
変更される primeFilter 関数は、素数によるフィルタと偶数によるフィルタの両方の結果を持ったDelta Monad を返すよう変更する。
図\ref{delta-program}のプログラムを実行した例が図\ref{delta-result}である。

% {{{ results

\begin{breakbox}
{\small
\begin{verbatim}
*Main> primeCount 10
Delta
  ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
  ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
\end{verbatim}
}
\caption{Delta Monad を用いたプログラムの実行例}
\label{delta-result}
\end{breakbox}

% }}}

Delta Monad による実行結果は2つの実行結果が存在する。
変更前のプログラムの実行順序が上側の実行結果である。
\begin{itemize}
    \item 1 から 10 までのリストを作成し
    \item 素数のみを残すために 2,3,5,7 が残り
    \item その個数を数えるために4となる
\end{itemize}
変更後のプログラムの実行順序が下側の実行結果である。
\begin{itemize}
    \item 1 から 10 までのリストを作成し
    \item 偶数のみを残すために 2,4,6,8,10 が残り
    \item その個数を数えるために5となる
\end{itemize}

変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。

今回は検証のために変更前と変更後の両方のプログラムを実行した。
しかし、必ず両方実行しなくてはならない訳では無い。
Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。

% }}}

% {{{ まとめと課題

\section{まとめと課題}
Delta Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。
さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。

今回定義したDelta Monad はプログラムの変更を保持できるのは1つのMonadにつき2つまでという制約がある。
Delta Monad を拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。
さらに、Monad によってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。

% }}}

\begin{thebibliography}{9}

\bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads(1991)
\bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)
\bibitem{category} Michael Barr and Chariles Wells, Category Theory for Computing Science
\bibitem{agda} The Agda Wiki - Agda \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}

\end{thebibliography}
\end{document}