Mercurial > hg > Members > atton > delta_monad
diff agda/laws.agda @ 94:bcd4fe52a504
Rewrite monad definitions for delta/deltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 17:10:29 +0900 |
parents | 55d11ce7e223 |
children | f26a954cd068 |
line wrap: on
line diff
--- a/agda/laws.agda Mon Jan 19 15:21:29 2015 +0900 +++ b/agda/laws.agda Mon Jan 19 17:10:29 2015 +0900 @@ -32,12 +32,15 @@ (M : {ll : Level} -> Set ll -> Set ll) (functorM : Functor M) : Set (suc l) where - field - mu : {A : Set l} -> M (M A) -> M A - eta : {A : Set l} -> A -> M A - field + 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 + field -- category laws association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x -open Monad \ No newline at end of file +open Monad