Mercurial > hg > Members > atton > delta_monad

diff agda/deltaM.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte type dependencie in Monad record for escape implicit type conflict
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 14:08:46 +0900
parents 29c54b0197fb
children ebd0d6e2772c
line wrap: on
line diff
--- a/agda/deltaM.agda	Sun Jan 25 12:16:34 2015 +0900
+++ b/agda/deltaM.agda	Mon Jan 26 14:08:46 2015 +0900
@@ -13,7 +13,7 @@
 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}
+            {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM}
             (A : Set l)
             : Set l where
    deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A
@@ -24,7 +24,7 @@
 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}
+             {monadM : {l' : Level} -> Monad {l'} M functorM}
              -> DeltaM M {functorM} {monadM} A -> M A
 headDeltaM (deltaM d) = headDelta d
 
@@ -32,7 +32,7 @@
 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}                                                                 
+             {monadM : {l' : Level}  -> Monad {l'} M functorM}                                                                 
              -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
 tailDeltaM (deltaM d)    = deltaM (tailDelta d)
 
@@ -40,7 +40,7 @@
 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}
+             {monadM : {l' : Level}  -> Monad {l'} 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)
 
@@ -48,7 +48,7 @@
 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}
+           {monadM : {l' : Level} -> Monad {l'} M functorM}
          -> Nat -> DeltaM M {functorM} {monadM} A -> M A
 checkOut O     (deltaM (mono x))    = x
 checkOut O     (deltaM (delta x _)) = x
@@ -62,7 +62,7 @@
 deltaM-fmap : {l : Level} {A B : 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}
+              {monadM : {l' : Level} -> Monad {l'}  M functorM}
               -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B
 deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d)
 
@@ -70,18 +70,18 @@
 open Monad
 deltaM-eta : {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}
+                                        {monadM   : {l' : Level}  -> Monad {l'}  M functorM}
             -> A -> (DeltaM M {functorM} {monadM} A)
-deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x))
+deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta monadM x))
 
 deltaM-mu : {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}
+                                        {monadM   : {l' : Level} -> Monad {l'}  M functorM}
             -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
-deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x))               = deltaM (mono (mu {l} {A} monadM (fmap functorM  headDeltaM x)))
-deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx)))    = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM)))
+deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x))               = deltaM (mono (mu monadM (fmap functorM headDeltaM x)))
+deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx)))    = appendDeltaM (deltaM (mono (bind  monadM x headDeltaM)))
                                                                                          (deltaM-mu (deltaM (mono xx)))
-deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM)))
+deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l}  monadM x headDeltaM)))
                                                                                          (deltaM-mu (deltaM  d))
 -- original deltaM-mu definitions. but it's cannot termination checking.
 -- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu.
@@ -92,6 +92,6 @@
 
 deltaM-bind : {l : Level} {A B : 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}
+                                        {monadM   : {l' : Level} -> Monad {l'} M functorM}
             -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B
 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d    f = deltaM-mu (deltaM-fmap f d)