Mercurial > hg > Papers > 2015 > atton-thesis

changeset 21:7d94faaeb448

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add natural transformation in program
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 09 Feb 2015 09:47:09 +0900
parents beebe0ffbcad
children fc44782929a7
files appendix.tex category.tex fig/delta_example.xbb fig/functor.xbb fig/functor_in_haskell.xbb fig/monad_laws.xbb fig/morphism_composition_law.xbb fig/natural_transformation.xbb fig/non_delta_example.xbb fig/ryukyu.xbb fig/simple_category.xbb
diffstat 11 files changed, 66 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/appendix.tex	Sun Feb 08 22:34:58 2015 +0900
+++ b/appendix.tex	Mon Feb 09 09:47:09 2015 +0900
@@ -1,1 +1,2 @@
 % TODO: 実験環境
+% TODO: Delta と DeltaM の本体
--- a/category.tex	Sun Feb 08 22:34:58 2015 +0900
+++ b/category.tex	Mon Feb 09 09:47:09 2015 +0900
@@ -428,6 +428,60 @@
 
 % }}}
 
-\section{Monads in Functional Programming}
+% {{{ Natural Transformation in Functional Programming
+
+\section{Natural Transformation in Functional Programming}
+\label{section:natural_transformation_in_program}
+\ref{section:functor_in_program}節ではプログラムにおける functor を定義した。
+\ref{section:natural_transformation_in_program}節ではプログラムにおける natural transformation について述べる。
+
+natural transformation は functor と functor 間の変換である。
+プログラムにおいて functor は型引数を持つデータ構造であったため、データ構造からデータ構造への変換となる。
+
+natural transformationは図\ref{fig:natural_transformation}で示したような可換図が可換になるような t であった。
+つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。
+
+プログラムにおける natural transformation は t は図\ref{fig:natural_transformation}を満たすような関数として表現される。
+Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。
+
+List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:natural_transformation_in_haskell, caption=List の先頭を除いた List を返す tail 関数] {src/natural_transformation_list.hs}
+\end{table}
+
+100, 200, 300 の数値を持つ List Int を考える。
+この List が functor f に相当する。
+Int を取り Bool を返す関数 even を fmap により適用すると List Bool が得られる。
 
-プログラムにおける
+ここで natural transformation tail を考える。
+tail は List a から List a への関数であるため、 functor f,g は両方とも List である。
+natural transformation の定義から、 tail を行なってから fmap even しても、 fmap even を行なってら tail を行なっても結果が同じであれば良い。
+実行した結果がリスト\ref{src:exec_tail}である。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:exec_tail, caption=tail の実行例] {src/exec_tail_in_haskell.txt}
+\end{table}
+
+tail (fmap even list) と fmap even (tail list) の型が同じように List Bool であり、値も等しいことが分かる。
+なお、 tail は同一名の関数が既に定義されているため、 Main.tail として名前を指定している。
+List の値を変換してから先頭を除いても、List の先頭を除いてから値を変換しても結果が同じであることは直感的にも正しいように思える。
+
+これがプログラムにおける natural transformation である。
+
+図で表すと、図\ref{fig:natural_transformation_in_program}のような可換図となり、これは可換である。
+
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics[scale=1.0]{fig/natural_transformation_in_haskell.pdf}
+        \caption{natural transformation tail の可換図}
+        \label{fig:natural_transformation_in_program}
+    \end{center}
+\end{figure}
+
+% }}}
+
+
+\section{Monads in Functional Programming}
+\label{section:monads_in_program}
+
--- a/fig/delta_example.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/delta_example.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 559.000000 279.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/functor.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/functor.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 545.000000 456.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/functor_in_haskell.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/functor_in_haskell.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 324.000000 176.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/monad_laws.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/monad_laws.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 464.000000 137.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/morphism_composition_law.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/morphism_composition_law.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 412.000000 273.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/natural_transformation.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/natural_transformation.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 211.000000 136.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/non_delta_example.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/non_delta_example.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 504.000000 244.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/ryukyu.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/ryukyu.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015
 
--- a/fig/simple_category.xbb	Sun Feb 08 22:34:58 2015 +0900
+++ b/fig/simple_category.xbb	Mon Feb 09 09:47:09 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 205.000000 82.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  8 21:05:26 2015
+%%CreationDate: Mon Feb  9 09:44:36 2015