Mercurial > hg > Members > atton > delta_monad

changeset 121:673e1ca0d1a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Refactor monad definition
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 12:11:24 +0900
parents 0f9ecd118a03
children e1900c89dea9
files agda/laws.agda
diffstat 1 files changed, 12 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/agda/laws.agda	Mon Feb 02 12:07:51 2015 +0900
+++ b/agda/laws.agda	Mon Feb 02 12:11:24 2015 +0900
@@ -13,7 +13,7 @@
                     -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
 open Functor
 
-record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')
+record NaturalTransformation {l : Level} (F G : Set l -> Set l)
                                          {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
                                          {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}
                                          (natural-transformation : {A : Set l}  -> F A -> G A)
@@ -27,23 +27,18 @@
 
 
 
--- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
-record Monad {l : Level} (M : Set l -> Set l)
-                         (functorM : Functor M)
-                         : Set (suc l)  where
+-- Categorical Monad definition. without haskell-laws (bind)
+record Monad {l : Level} (T : Set l -> Set l) (F : Functor T) : Set (suc l)  where
   field -- category
-    mu  :  {A : Set l} -> M (M A) -> M A
-    eta :  {A : Set l} -> A -> M A
-  field -- haskell
-    return : {A : Set l} -> A -> M A
-    bind   : {A B : Set l} -> M A -> (A -> (M B)) -> M B
+    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 : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
-    left-unity-law  : {A : Set l} -> (x : M A) -> (mu  ∙ (fmap functorM eta)) x ≡ id x
-    right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x
-  field -- natural transformations
-    eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
-    mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : M (M A)) -> mu (fmap functorM (fmap functorM f) x) ≡ fmap functorM f (mu x)
+    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
 
 
-open Monad
\ No newline at end of file
+open Monad