Mercurial > hg > Members > atton > delta_monad

changeset 89:5411ce26d525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Defining DeltaM in Agda...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 11:48:41 +0900
parents 526186c4f298
children 55d11ce7e223
files agda/delta.agda agda/delta/functor.agda agda/deltaM.agda
diffstat 3 files changed, 82 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/agda/delta.agda	Mon Jan 19 11:10:58 2015 +0900
+++ b/agda/delta.agda	Mon Jan 19 11:48:41 2015 +0900
@@ -32,9 +32,9 @@
 
 
 -- Functor
-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
-fmap f (mono x)    = mono  (f x)
-fmap f (delta x d) = delta (f x) (fmap f d)
+delta-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
+delta-fmap f (mono x)    = mono  (f x)
+delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
 
 
 
@@ -106,29 +106,24 @@
   mono x                          ∎
 
 head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll}
-  -> (f : A -> B) -> (d : Delta A) -> headDelta (fmap f d) ≡ f (headDelta d)
+  -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d)
 head-delta-natural-transformation f (mono x)    = refl
 head-delta-natural-transformation f (delta x d) = refl
 
 n-tail-natural-transformation  : {l ll : Level} {A : Set l} {B : Set ll}
-  -> (n : Nat) -> (f : A -> B) -> (d : Delta A) ->  n-tail n (fmap f d) ≡ fmap f (n-tail n d)
+  -> (n : Nat) -> (f : A -> B) -> (d : Delta A) ->  n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d)
 n-tail-natural-transformation O f d            = refl
 n-tail-natural-transformation (S n) f (mono x) = begin
-  n-tail (S n) (fmap f (mono x))  ≡⟨ refl ⟩
+  n-tail (S n) (delta-fmap f (mono x))  ≡⟨ refl ⟩
   n-tail (S n) (mono (f x))       ≡⟨ tail-delta-to-mono (S n) (f x) ⟩
   (mono (f x))                    ≡⟨ refl ⟩
-  fmap f (mono x)                 ≡⟨ cong (\d -> fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩
-  fmap f (n-tail (S n) (mono x))  ∎
+  delta-fmap f (mono x)                 ≡⟨ cong (\d -> delta-fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩
+  delta-fmap f (n-tail (S n) (mono x))  ∎
 n-tail-natural-transformation (S n) f (delta x d) = begin
-  n-tail (S n) (fmap f (delta x d))                 ≡⟨ refl ⟩
-  n-tail (S n) (delta (f x) (fmap f d))             ≡⟨ cong (\t -> t (delta (f x) (fmap f d))) (sym (n-tail-plus n)) ⟩
-  ((n-tail n) ∙ tailDelta) (delta (f x) (fmap f d)) ≡⟨ refl ⟩
-  n-tail n (fmap f d)                               ≡⟨ n-tail-natural-transformation n f d ⟩
-  fmap f (n-tail n d)                               ≡⟨ refl ⟩
-  fmap f (((n-tail n) ∙ tailDelta) (delta x d))     ≡⟨ cong (\t -> fmap f (t (delta x d))) (n-tail-plus n) ⟩
-  fmap f (n-tail (S n) (delta x d))                 ∎
-
-
-
-
-
+  n-tail (S n) (delta-fmap f (delta x d))                 ≡⟨ refl ⟩
+  n-tail (S n) (delta (f x) (delta-fmap f d))             ≡⟨ cong (\t -> t (delta (f x) (delta-fmap f d))) (sym (n-tail-plus n)) ⟩
+  ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩
+  n-tail n (delta-fmap f d)                               ≡⟨ n-tail-natural-transformation n f d ⟩
+  delta-fmap f (n-tail n d)                               ≡⟨ refl ⟩
+  delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d))     ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩
+  delta-fmap f (n-tail (S n) (delta x d))                 ∎
--- a/agda/delta/functor.agda	Mon Jan 19 11:10:58 2015 +0900
+++ b/agda/delta/functor.agda	Mon Jan 19 11:48:41 2015 +0900
@@ -11,18 +11,18 @@
 -- Functor-laws
 
 -- Functor-law-1 : T(id) = id'
-functor-law-1 :  {l : Level} {A : Set l} ->  (d : Delta A) -> (fmap id) d ≡ id d
+functor-law-1 :  {l : Level} {A : Set l} ->  (d : Delta A) -> (delta-fmap id) d ≡ id d
 functor-law-1 (mono x)    = refl
 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
 
 -- Functor-law-2 : T(f . g) = T(f) . T(g)
 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
                 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
-                (fmap (f ∙ g)) d ≡ (fmap f) (fmap g d)
+                (delta-fmap (f ∙ g)) d ≡ (delta-fmap f) (delta-fmap g d)
 functor-law-2 f g (mono x)    = refl
 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
 
 delta-is-functor : {l : Level} -> Functor (Delta {l})
-delta-is-functor = record {  fmap = fmap ;
+delta-is-functor = record {  fmap = delta-fmap ;
                              preserve-id = functor-law-1;
                              covariant  = \f g -> functor-law-2 g f}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/deltaM.agda	Mon Jan 19 11:48:41 2015 +0900
@@ -0,0 +1,64 @@
+open import Level
+
+open import delta
+open import delta.functor
+open import nat
+open import laws
+
+module deltaM where
+
+-- DeltaM definitions
+
+data DeltaM {l : Level}
+            (M : {l' : Level} -> Set l' -> Set l')
+            {functorM : {l' : Level} -> Functor {l'} M}
+            {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+            (A : Set l)
+            : Set l where
+   deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A
+
+
+-- DeltaM utils
+
+headDeltaM : {l : Level} {A : Set l}
+             {M : {l' : Level} -> Set l' -> Set l'}
+             {functorM : {l' : Level} -> Functor {l'} M}
+             {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+             -> DeltaM M {functorM} {monadM} A -> M A
+headDeltaM (deltaM (mono x))    = x
+headDeltaM (deltaM (delta x _)) = x
+
+tailDeltaM :  {l : Level} {A : Set l}
+             {M : {l' : Level} -> Set l' -> Set l'}
+             {functorM : {l' : Level} -> Functor {l'} M}
+             {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}                                                                 
+             -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
+tailDeltaM (deltaM (mono x))    = deltaM (mono x)
+tailDeltaM (deltaM (delta _ d)) = deltaM d
+
+appendDeltaM : {l : Level} {A : Set l}
+             {M : {l' : Level} -> Set l' -> Set l'}
+             {functorM : {l' : Level} -> Functor {l'} M}
+             {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+             -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A               
+appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd)
+
+
+checkOut : {l : Level} {A : Set l}
+           {M : {l' : Level} -> Set l' -> Set l'}
+           {functorM : {l' : Level} -> Functor {l'} M}
+           {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+         -> Nat -> DeltaM M {functorM} {monadM} A -> M A
+checkOut O     (deltaM (mono x))    = x
+checkOut O     (deltaM (delta x _)) = x
+checkOut (S n) (deltaM (mono x))    = x
+checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d)
+
+{-
+deltaM-fmap : {l ll : Level} {A : Set l} {B : Set ll} 
+           {M : {l' : Level} -> Set l' -> Set l'}
+           {functorM : {l' : Level} -> Functor {l'} M}
+           {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+           -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B
+deltaM-fmap {l} {ll} {A} {B} {M} {functorM} f (deltaM d) = deltaM (Functor.fmap delta-is-functor (Functor.fmap functorM f) d)
+-}
\ No newline at end of file