# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423817517 -32400
# Node ID b7e693b6d7d976bfff0fb11463d5bf4c24c4f082
# Parent  4cc65012412f6369eb1ff585a9500cd9970db77d
Add defintion monad-laws in agda

diff -r 4cc65012412f -r b7e693b6d7d9 proof_delta.tex
--- a/proof_delta.tex	Fri Feb 13 17:13:23 2015 +0900
+++ b/proof_delta.tex	Fri Feb 13 17:51:57 2015 +0900
@@ -127,7 +127,7 @@
         リスト\ref{src:delta_preserve_id}に証明を示す。
 
         \begin{table}[html]
-            \lstinputlisting[label=src:delta_preserve_id, caption= Delta における fmap も id を保存する] {src/delta_preserve_id.agda.replaced}
+            \lstinputlisting[label=src:delta_preserve_id, caption= Delta における fmap も id を保存する証明] {src/delta_preserve_id.agda.replaced}
         \end{table}
 
 
@@ -143,7 +143,7 @@
         リスト\ref{src:delta_covariant}に証明を示す。
 
         \begin{table}[html]
-            \lstinputlisting[label=src:delta_covariant, caption= Delta における fmap も関数の合成を保存する] {src/delta_covariant.agda.replaced}
+            \lstinputlisting[label=src:delta_covariant, caption= Delta における fmap も関数の合成を保存する証明] {src/delta_covariant.agda.replaced}
         \end{table}
 
         id の保存のように、コンストラクタによるパターンマッチを行なう。
@@ -154,7 +154,7 @@
 
 
 \begin{table}[html]
-    \lstinputlisting[label=src:delta_is_functor, caption= Delta の定義と証明から Functor record を構成する] {src/delta_is_functor.agda.replaced}
+    \lstinputlisting[label=src:delta_is_functor, caption= Delta が Functor則を満たすことの証明] {src/delta_is_functor.agda.replaced}
 \end{table}
 
 record が正しく構成できたため、Delta は Functor 則を満たす。
@@ -162,5 +162,43 @@
 
 % }}}
 
+% {{{ Agda における Monad 則
+
 \section{Agda における Monad 則}
+\label{section:monad_laws_in_agda}
+\ref{section:functor_in_agda}節と\ref{section:delta_is_functor}節では Delta が Functor 則を満たすことの証明を行なった。
+\ref{section:monad_laws_in_agda}節では同じように Monad 則の定義を行ない、\ref{section:delta_is_monad}節で証明を行なう。
+
+まずは Monad則の定義を行なう(リスト\ref{src:monad_laws_in_agda})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:monad_laws_in_agda, caption= AgdaにおけるMonad則の定義] {src/monad_laws.agda.replaced}
+\end{table}
+
+Monad 則とは $ triple(T, \eta, \mu) $ に対して課すべき制約であった。
+そのためまず要素として $ T $ , $ \eta $, $ \mu $ が存在する。
+T は Set l を取り Set l を返す型であり、Functor則を満たす。
+$ \eta $ は T を増やす関数であり、 $ \mu $ は T を減らす関数である。
+これら Monad の構成要素を定義する field である。
+
+次に、$ \eta $ と $ \mu $ は natural transformation である必要がある。
+よって field に制約として $ \eta $ と $ \mu $ の natural transformation を定義する。
+なお、 field という予約語は複数書いても2つ目以降は無いものとして振る舞う。
+
+ここで、 \verb/ fmap F / という項に注目して欲しい。
+値F は Functor T 型を持ち、fmap や2つの証明を内包する。
+fmap や証明へのアクセスは \verb/ field-name record-value / と記述する。
+例えば、リスト\ref{src:delta_is_functor}で定義した Functor Delta の型を持つ値 \verb/delta-is-functor/ に対して \verb/ fmap delta-is-functor/ とすると関数 delta-fmap が得られる。
+つまり、\verb/fmap F f/ とするのは Functor則が証明された F の fmap に関数fを適用することとなる。
+
+最後に $ triple (T, \eta, \mu) $ に対する Monad 則に相当する等式を記述する。
+Monad則は可換図として与えられたTに対する演算の可換性と、Tに対する演算の単位元を強制するものであった。
+Tに対する演算の可換性は association-law として、単位元の強制は unity-law として記述できる。
+unity-law はTに対する演算が右側からか左側からかの二種類があるため、 right-unity-law と left-unity-law に分割した。
+
+これら全ての field を満たすような証明を記述できれば、 $ triple (T, \eta, \mu) $ は Monad であると言える。
+
+% }}}
+
 \section{Delta が Monad 則を満たす証明}
+\label{section:delta_is_monad}
diff -r 4cc65012412f -r b7e693b6d7d9 src/delta_monad_definition.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_monad_definition.agda	Fri Feb 13 17:51:57 2015 +0900
@@ -0,0 +1,186 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+open import basic
+open import delta
+open import delta.functor
+open import nat
+open import laws
+
+module delta.monad where
+
+tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                  (f : A -> B) -> (d : Delta A (S (S n))) ->
+                  (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
+tailDelta-is-nt f (delta x d) = refl
+
+
+tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m  : Nat)
+                       (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
+                   delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d)
+tailDelta-to-tail-nt O O f (mono (delta x d)) = refl
+tailDelta-to-tail-nt O (S m) f (mono (delta x d)) = refl
+tailDelta-to-tail-nt (S n) O f (delta (delta x (mono xx)) d) = begin
+  delta (mono (f xx))
+    (delta-fmap tailDelta (delta-fmap (delta-fmap f) d))
+  ≡⟨ cong (\de -> delta (mono (f xx)) de) (tailDelta-to-tail-nt n O f d) ⟩
+  delta (mono (f xx))
+    (delta-fmap (delta-fmap f) (delta-fmap tailDelta d))
+  ∎
+tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin
+  delta (delta (f xx) (delta-fmap f d))
+    (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))
+  ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩
+  delta (delta (f xx) (delta-fmap f d))
+    (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))
+  ∎
+
+
+delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
+                  (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
+delta-eta-is-nt {n = O}   f x = refl
+delta-eta-is-nt {n = S O} f x = refl
+delta-eta-is-nt {n = S n} f x = begin
+  (delta-eta ∙ f) x                        ≡⟨ refl ⟩
+  delta-eta (f x)                          ≡⟨ refl ⟩
+  delta (f x) (delta-eta (f x))            ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
+  delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
+  delta-fmap f (delta x (delta-eta x))     ≡⟨ refl ⟩
+  delta-fmap f (delta-eta x)               ∎
+
+
+delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n))
+               -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d)
+delta-mu-is-nt {n = O} f (mono d) = refl
+delta-mu-is-nt {n = S n} f (delta (delta x d) ds) = begin
+  delta (f x) (delta-mu (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)))
+  ≡⟨ cong (\de -> delta (f x) (delta-mu de)) (tailDelta-to-tail-nt n n f ds ) ⟩
+  delta (f x) (delta-mu (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)))
+  ≡⟨ cong (\de -> delta (f x) de) (delta-mu-is-nt f (delta-fmap tailDelta ds)) ⟩
+  delta (f x) (delta-fmap f (delta-mu (delta-fmap tailDelta ds)))
+  ∎
+
+
+delta-fmap-mu-to-tail : {l : Level} {A : Set l} (n m : Nat) (d : Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)) ->
+  delta-fmap tailDelta (delta-fmap delta-mu d)
+  ≡
+  (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d)))
+delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl
+delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl
+delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin
+  delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds))
+  ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩
+  delta (mono dxx)
+    (delta-fmap delta-mu
+     (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
+  ∎
+delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
+  delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
+    (delta-fmap tailDelta (delta-fmap delta-mu dds))
+  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩
+  delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
+    (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds)))
+  ∎
+
+
+
+-- Monad-laws (Category)
+-- association-law : join . delta-fmap join = join . join
+delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
+              ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
+delta-association-law {n =       O} (mono d)                          = refl
+delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
+  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
+  ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
+  delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
+  ≡⟨ cong (\de -> delta x de) (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
+  delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
+  ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩
+  delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
+  ∎
+
+
+delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
+delta-right-unity-law (mono x)    = refl
+delta-right-unity-law (delta x d) = begin
+  (delta-mu ∙ delta-eta) (delta x d)
+  ≡⟨ refl ⟩
+  delta-mu (delta-eta (delta x d))
+  ≡⟨ refl ⟩
+  delta-mu (delta (delta x d) (delta-eta (delta x d)))
+  ≡⟨ refl ⟩
+  delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
+  ≡⟨ refl ⟩
+  delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
+  ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt  tailDelta (delta x d))) ⟩
+  delta x (delta-mu (delta-eta (tailDelta (delta x d))))
+  ≡⟨ refl ⟩
+  delta x (delta-mu (delta-eta d))
+  ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
+  delta x d
+  ≡⟨ refl ⟩
+  id (delta x d)  ∎
+
+
+delta-left-unity-law  : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
+                                             (delta-mu  ∙ (delta-fmap delta-eta)) d ≡ id d
+delta-left-unity-law (mono x)    = refl
+delta-left-unity-law {n = (S n)} (delta x d) = begin
+  (delta-mu ∙ delta-fmap delta-eta) (delta x d)            ≡⟨ refl ⟩
+  delta-mu ( delta-fmap delta-eta (delta x d))             ≡⟨ refl ⟩
+  delta-mu (delta (delta-eta x) (delta-fmap delta-eta d))  ≡⟨ refl ⟩
+  delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))  ≡⟨ refl ⟩
+  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
+  ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩
+  delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d))  ≡⟨ refl ⟩
+  delta x (delta-mu (delta-fmap (delta-eta {n = n}) d))  ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
+  delta x d ≡⟨ refl ⟩
+  id (delta x d)  ∎
+
+
+
+delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n))  delta-is-functor
+delta-is-monad = record { eta    = delta-eta;
+                          mu     = delta-mu;
+                          eta-is-nt = delta-eta-is-nt;
+                          mu-is-nt = delta-mu-is-nt;
+                          association-law = delta-association-law;
+                          left-unity-law  = delta-left-unity-law ;
+                          right-unity-law = \x -> (sym (delta-right-unity-law x)) }
+
+
+
+
+
+{-
+
+-- Monad-laws (Haskell)
+-- monad-law-h-1 : return a >>= k  =  k a
+monad-law-h-1 : {l : Level} {A B : Set l} ->
+                (a : A) -> (k : A -> (Delta B)) ->
+                (delta-return a >>= k)  ≡ (k a)
+monad-law-h-1 a k = refl
+
+
+
+-- monad-law-h-2 : m >>= return  =  m
+monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= delta-return)  ≡ m
+monad-law-h-2 (mono x)    = refl
+monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
+
+
+
+-- monad-law-h-3 : m >>= (\x -> f x >>= g)  =  (m >>= f) >>= g
+monad-law-h-3 : {l : Level} {A B C : Set l} ->
+                (m : Delta A)  -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) ->
+                (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g)
+monad-law-h-3 (mono x) f g     = refl
+monad-law-h-3 (delta x d) f g = begin
+  (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩
+  (delta-bind (delta-bind (delta x d) f) g) ∎
+
+
+
+
+-}
diff -r 4cc65012412f -r b7e693b6d7d9 src/monad_laws.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/monad_laws.agda	Fri Feb 13 17:51:57 2015 +0900
@@ -0,0 +1,21 @@
+record Monad {l : Level} (T : Set l -> Set l) (F : Functor T)
+        : Set (suc l)  where
+
+  field -- category
+    mu  :  {A : Set l} -> T (T A) -> T A
+    eta :  {A : Set l} -> A -> T A
+
+  field -- natural transformations
+    eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A)       ->
+                (eta ∙ f) x ≡ fmap F f (eta x)
+    mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) ->
+                mu (fmap F (fmap F f) x) ≡ fmap F f (mu x)
+
+  field -- category laws
+    association-law : {A : Set l} -> (x : (T (T (T A)))) ->
+                      (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x
+    left-unity-law  : {A : Set l} -> (x : T A)           ->
+                      (mu ∙ (fmap F eta)) x ≡ id x
+    right-unity-law : {A : Set l} -> (x : T A)           ->
+                      id x ≡ (mu ∙ eta) x
+