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