# HG changeset patch # User Yasutaka Higa # Date 1414329043 -32400 # Node ID ffbe1bfc412c538bb5bc82b43e846d628676a01c # Parent de0aa29cc3d545876afba6c87767882d49359e8a wrote bachelor middle draft diff -r de0aa29cc3d5 -r ffbe1bfc412c bachelor_middle_draft/bachelor_middle_draft.tex --- a/bachelor_middle_draft/bachelor_middle_draft.tex Sun Oct 26 19:21:30 2014 +0900 +++ b/bachelor_middle_draft/bachelor_middle_draft.tex Sun Oct 26 22:10:43 2014 +0900 @@ -3,6 +3,7 @@ \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{} @@ -64,18 +65,8 @@ Monadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。 プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。 -型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。 -このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。 -変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。 -文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。 -計算そのものに対しては影響しない。 -この型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する。(図\ref{diff-monad-instance-definition}) -TODO:ここまで - -また、型Diffが Monad則(\ref{haskell-monad-law})を満たしていることをAgdaによって証明した。 - -% {{{ source codes +% {{{ Definiton Diff \begin{breakbox} \verb/ data Diff a = Diff [String] a [String] a/ @@ -83,26 +74,47 @@ \label{diff-monad-definition} \end{breakbox} +% }}} + +型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。 +このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。 +変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。 +文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。 +計算そのものに対しては影響しない。 + +型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。 +% {{{ instance Monad Diff + \begin{breakbox} \begin{verbatim} -mu :: Similar (Similar a) -> Similar a -mu (Similar lx (Similar llx x _ _) - ly (Similar _ _ lly y)) = \ - Similar (lx ++ llx) x (ly ++ lly) y +mu (Diff lx (Diff llx x _ _) + ly (Diff _ _ lly y)) = + Diff (lx ++ llx) x (ly ++ lly) y -instance Monad Similar where - return x = Similar [] x [] x - s >>= f = mu $ fmap f s +instance Monad Diff where + return x = Diff [] x [] x + d >>= f = mu $ fmap f d \end{verbatim} \caption{Diff を Monad のインスタンスとして定義する} \label{diff-monad-instance-definition} \end{breakbox} +% }}} + +return はデータをMonadにするためのものであり、型aから型T aへの変換である。 +\verb/>>=/ は型aから型T bに変換するための関数を用いてT aから T b への変換を定義する。 +\verb/>>=/ によって計算が行なわれる際に型Diff が持っている2つ変数に対する計算を行なう。 +片方はプログラム変更前の値を持ち、もう片方は変更後の値を持つようにする。 + +また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることをAgdaによって証明した。 + +% {{{ Monad-laws + \begin{breakbox} \begin{verbatim} return a >>= k = k a m >>= return = m - m >>= (\\x -> k x >>= h) = (m >>= k) >>= h + m >>= (\x -> k x >>= h) = (m >>= k) >>= h \end{verbatim} \caption{Haskell における Monad則} \label{haskell-monad-law} @@ -110,24 +122,99 @@ % }}} +% }}} + +\section{Diff Monadを用いたプログラムの実行} +Diff Monad を用いたHaskellのプログラムを示す(図\ref{diff-program})。 + +% {{{ diff.hs + +\begin{breakbox} +{\scriptsize +\begin{verbatim} +generator :: Int -> Diff [Int] +generator x = let intList = [1..x] in + returnD intList + +primeFilter :: [Int] -> Diff [Int] +primeFilter xs = let primeList = filter isPrime xs + refactorList = filter even xs in + returnDD primeList refactorList + +count :: [Int] -> Diff Int +count xs = let primeCount = length xs in + returnD primeCount + +primeCount :: Int -> Diff Int +primeCount x = generator x >>= primeFilter >>= count +\end{verbatim} +} +\caption{Diff Monadを用いたプログラムの例} +\label{diff-program} +\end{breakbox} % }}} -\section{Diff Monadを用いたプログラムの実行} -TODO: 実行例 +このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。 +1からnまでの整数の個数を調べるprimeCount 関数は3つの関数からなる + +\begin{itemize} + \item 1 から n までの整数を返す関数 generator + \item 整数のリストから素数であるもののみを残したリストを返す関数 primeFilter + \item リストの中に存在する要素の個数を返す関数 count +\end{itemize} + +このプログラムの primeFilter 関数が返す Diff Monad を変更する。 +本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。 +変更後のプログラムを実行した例が図\ref{diff-result}である。 + +% {{{ results + +\begin{breakbox} +{\small +\begin{verbatim} +*Main> primeCount 10 +Diff ["[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{Diff Monad を用いたプログラムの実行例} +\label{diff-result} +\end{breakbox} + +% }}} + +変更前のプログラムの実行順序が上側の実行結果である。 +\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 には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。 +よって、変更後のプログラムのみを計算する場合は変更前の計算は行なわれない。 +遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。 % {{{ まとめと課題 \section{まとめと課題} -Monad によるプログラムの変更を行なった。 -このことにより、変更前のプログラムを保存しながら変更後のプログラムとして実行することが可能となった。 +Diff Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとして実行することが可能となった。 -課題としては大きく2つある。変更の個数の拡張と Monad によってプログラムを変更することの意味論を調べることである。 +今後の課題としては大きく2つある。 +変更の個数の拡張と Monad によってプログラムを変更することの意味を調べることである。 現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。 変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表したい。 -また、プログラムに対する変更がMonadによって表される場合に圏論の視点からどのような意味が捉えられるか調査したい。 +また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査したい。 Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。 Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。 @@ -137,7 +224,8 @@ \begin{thebibliography}{9} -\bibitem{moggi} Notion of Computation and Monads(TODO:あとで) +\bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads (1991) +\bibitem{monad-laws} Monad - HaskellWiki \url{http://www.haskell.org/haskellwiki/Monad} \end{thebibliography} \end{document}