Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.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 9c62373bd474
children 0a3b6cb91a05
comparison
equal deleted inserted replaced
102:9c62373bd474 103:a271f3ff1922
27 27
28 28
29 29
30 30
31 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. 31 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
32 record Monad {l : Level} {A : Set l} 32 record Monad {l : Level} (M : {ll : Level} -> Set ll -> Set ll)
33 (M : {ll : Level} -> Set ll -> Set ll)
34 (functorM : Functor {l} M) 33 (functorM : Functor {l} M)
35 : Set (suc l) where 34 : Set (suc l) where
36 field -- category 35 field -- category
37 mu : {A : Set l} -> M (M A) -> M A 36 mu : {A : Set l} -> M (M A) -> M A
38 eta : {A : Set l} -> A -> M A 37 eta : {A : Set l} -> A -> M A
39 field -- haskell 38 field -- haskell
40 return : {A : Set l} -> A -> M A 39 return : {A : Set l} -> A -> M A
41 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B 40 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B
42 field -- category laws 41 field -- category laws
43 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x 42 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
44 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x 43 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x
45 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x 44 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x
46 field -- natural transformations 45 field -- natural transformations
47 eta-is-nt : {B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) 46 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
48 47
49 48
50 open Monad 49 open Monad