Mercurial > hg > Papers > 2015 > atton-thesis

annotate delta_with_monad.tex @ 51:801be6f676bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Future work
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 21:46:38 +0900
parents 37a832dff044
children 43213dcf8d24
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
46
1b688e70f2a8 Move proofs to appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{任意の Monad と Delta の組み合せ}
49
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
2 \label{chapter:delta_with_monad}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
3 第\ref{chapter:proof_delta}章ではプログラムの変更を表現する Delta Monad が Monad であることを証明した。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
4 第\ref{chapter:delta_with_monad}章では、Delta Monad と、他の Monad との組み合せを考える。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
5 特に他の Monad のメタ計算も同時に実行できるようなデータ DeltaM を定義し、利用例を示す。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
6
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
7 % {{{ Monad と組み合せた Delta である DeltaM
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
8
47
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
9 \section{Monad と組み合せた Delta である DeltaM}
49
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
10 \label{section:deltaM}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
11 functional programming における monad とはデータ構造をメタ計算の対応付けであった。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
12 プログラミング言語 Haskell においては入出力や非決定性演算といった処理が monad として提供される。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
13 そのため、プログラムの変更を表現する Delta Monad では他の monad と組み合せることが可能でなくてはならない。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
14 Delta Monad を拡張し、Delta Monad の内部の monad のメタ計算を実行するデータ型 DeltaM を Haskell で定義する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
15
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
16 データ型 DeltaM と、DeltaM に対する Monad の instance 定義を示す(リスト\ref{src:deltaM_definition})。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
17
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
18 \begin{table}[html]
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
19 \lstinputlisting[label=src:deltaM_definition,
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
20 caption= DeltaM の定義と Monad の instance 定義,
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
21 escapechar=&]
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
22 {src/deltaM_definition.hs}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
23 \end{table}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
24
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
25 データ型 DeltaM は2つの型引数を持つ。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
26 型引数a と型引数を持つ型引数 m である。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
27 m に対して a を適用した型を持つ DeltaM から DeltaM コンストラクタを用いて DeltaM 型を構成できる。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
28 型名とコンストラクタ名が同一になっているので注意が必要である。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
29 m が Monad であり、 a が Monad が内包する型を表す。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
30
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
31 次にいくつかの関数を定義する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
32 unDeltaM は DeltaM から Delta へと戻す関数である。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
33 headDeltaM はDelta から先頭の値を取り出す。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
34 バージョン管理された Delta から最新のバージョンを取り出すことに相当する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
35 tailDeltaM はDelta から先頭の値を取り除く。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
36 これはバージョン管理された Delta から最新以外のバージョンに対して処理を行う時に用いる。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
37
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
38 DeltaM の instance 定義では \verb/>>=/ ではなく mu を介して行なう。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
39 ここで2つの新たな記法を解説する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
40
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
41 \begin{itemize}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
42 \item \verb/ (Functor m) => ... /
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
43
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
44 mu や Monad の instance 宣言に利用されている記法で、型制約を示す記号である。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
45 ある型 m が Functor の instance であることを示す。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
46 例えば、 mu に記述されている \verb/(Functor m, Monad m) => ... / は型 m が Functor と Monad の instance である時に mu に適用できることを示す。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
47 型制約により、型 m a は Functor である保証がつくため、 m a の値に対して fmap をかけることできる。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
48
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
49 \item \verb/ d@(DeltaM (Mono ...)) /
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
50
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
51 パターンマッチにおける記法で、asパターンと呼ばれる。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
52 パターンマッチにおいてコンストラクタを指定したのち、全体の値を \verb/@/ の前の変数に束縛する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
53 例えば \verb/ m@(Mono x) / と指定すると、 \verb/Mono x/ が m に束縛される。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
54 この記法を採用するメリットは、コンストラクタでパターンマッチしたものの、値はコンストラクタを含んだまま処理したい時にタイプ数を省略できることにある。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
55 \end{itemize}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
56
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
57 関数 mu ではDelta におけるバージョンの管理と内部の Monad のメタ計算の両方を一度に行なう。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
58
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
59 バージョンが1であった場合は内部の DeltaM から fmap headDeltaM を用いて値を取り出し、 \verb/>>= id/ で内部の Monad のメタ計算を行なう。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
60 同じように、バージョンが1以上であった場合は先頭のバージョンに対しメタ計算を行なってから、残りのバージョンに対して再帰的に mu を行なう。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
61
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
62 mu が定義できたので、 DeltaM を Monad の instance とする。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
63 m が Functor と Monad である時のみ、 DeltaM は Monad となる。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
64
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
65 return は通常の値を内部の Monad の return でメタ計算に対応させ、バージョン1である Mono としてから DeltaM とする。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
66 中置関数 \verb/>>=/ は fmap と mu を用いて定義する。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
67
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
68 以上で Delta Monad と 他の Monad を組み合せるための DeltaM が定義できた。
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
69
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
70 % }}}
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
71
50
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
72 % {{{ DeltaM を用いたプログラムの例
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
73
46
1b688e70f2a8 Move proofs to appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 \section{DeltaM を用いたプログラムの例}
49
ba7f0b5454ab Add description for DeltaM definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
75 \label{section:deltaM_example}
50
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
76 DeltaM を用いてプログラムを記述する。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
77 今回は簡易的なプログラムのトレースとして、実行時の値を文字列として残すこととする。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
78 Haskell では処理に対するログなどを残すための Monad として Writer という Monad を提供している。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
79 リスト\ref{src:delta_example} で示した numberCount プログラムに対し、Writer Monad と Delta Monad を組み合せてトレースの比較を組込む(リスト\ref{src:deltaM_example})。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
80
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
81
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
82 \begin{table}[html]
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
83 \lstinputlisting[label=src:deltaM_example, caption= DeltaM を用いたプログラムの例] {src/deltaM_example.hs}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
84 \end{table}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
85
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
86 Writer と組み合せた Delta を DeltaWithLog 型として定義する。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
87 型の定義には type 構文を用い、ある型の別名として再定義する。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
88 まず、 Writer で記録する型を String の List とし、その型を DeltaLog とする。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
89 DeltaLog を内包する DeltaM として DeltaWithLog 型定義した。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
90
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
91 また、値をログとするために関数 returnW を定義した。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
92 これは通常の値から DeltaLog を生成するための関数である。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
93 tell 関数を用いてログを Writer に書き込み、値を return で保持する。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
94
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
95 処理を簡易化するために、リストから Delta を作成する関数 deltaFromList を定義しておく。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
96
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
97 numberCountM プログラムは numberCount プログラムとほとんど違いは無い。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
98 以下の3つの関数の組み合せで作成されている。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
99
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
100 \begin{itemize}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
101 \item generatorM
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
102
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
103 n を取り、1から nまでのリストを返す
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
104 バージョン1とバージョン2に違いは無い。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
105
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
106 \item numberCountM
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
107
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
108 整数のリストを取り、特定の条件によって絞り込む。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
109 バージョン1では素数のみを絞り込み、バージョン2では偶数を絞り込む。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
110
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
111
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
112 \item countM
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
113
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
114 リストを取り、その要素の個数を返す。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
115 バージョン1とバージョン2に違いは無い。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
116
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
117 \end{itemize}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
118
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
119 唯一の違いは関数が最後に返す Deltaに対して returnW 関数が適用されていることである。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
120 returnW を用いることで簡易的な値のトレースが得られる。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
121
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
122
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
123 実行した結果はリスト\ref{src:numberCountM_result}である。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
124
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
125 \begin{table}[html]
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
126 \lstinputlisting[label=src:numberCountM_result, caption= NumberCountM プログラムの実行例] {src/numberCountM_result.txt}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
127 \end{table}
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
128
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
129 numberCountM プログラムに対して20を与えて実行した結果である。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
130 なお、結果は読み易いように整形してある。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
131 ここで注目して欲しいのが、それぞれがどのような計算結果を辿ったのかを Writer が保持していることである。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
132
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
133 2つの結果とも、まずは generatorM 関数により1から20までのリストを作る。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
134 次に numberFilterM 関数によってフィルタされ、それぞれの結果による値が導かれる。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
135 バージョン1では素数の個数を数えるために8であり、バージョン2では偶数の個数を数えるために10となる。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
136
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
137 このように、Monad と組み合せることでトレースを得ることができた。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
138 Writer 以外にも任意の Monad に対して DeltaM が Monad 則を満たす。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
139 この証明は非常に長いので付録に載せるものとする。% TODO ref
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
140
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
141 DeltaM を定義した結果、Delta Monadと Monad を組み合せることができた。
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
142
37a832dff044 Add DeltaM example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
143 % }}}