Mercurial > hg > Members > atton > delta_monad
comparison 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 |
comparison
equal
deleted
inserted
replaced
93:8d92ed54a94f | 94:bcd4fe52a504 |
---|---|
30 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. | 30 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. |
31 record Monad {l : Level} {A : Set l} | 31 record Monad {l : Level} {A : Set l} |
32 (M : {ll : Level} -> Set ll -> Set ll) | 32 (M : {ll : Level} -> Set ll -> Set ll) |
33 (functorM : Functor M) | 33 (functorM : Functor M) |
34 : Set (suc l) where | 34 : Set (suc l) where |
35 field | 35 field -- category |
36 mu : {A : Set l} -> M (M A) -> M A | 36 mu : {A : Set l} -> M (M A) -> M A |
37 eta : {A : Set l} -> A -> M A | 37 eta : {A : Set l} -> A -> M A |
38 field | 38 field -- haskell |
39 return : {A : Set l} -> A -> M A | |
40 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B | |
41 field -- category laws | |
39 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x | 42 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x |
40 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x | 43 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x |
41 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x | 44 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x |
42 | 45 |
43 open Monad | 46 open Monad |