Mercurial > hg > Members > atton > delta_monad
comparison agda/laws.agda @ 121:673e1ca0d1a9
Refactor monad definition
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 02 Feb 2015 12:11:24 +0900 |
parents | e6bcc7467335 |
children | 5902b2a24abf |
comparison
equal
deleted
inserted
replaced
120:0f9ecd118a03 | 121:673e1ca0d1a9 |
---|---|
11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x | 11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x |
12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) | 12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) |
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x | 13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x |
14 open Functor | 14 open Functor |
15 | 15 |
16 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') | 16 record NaturalTransformation {l : Level} (F G : Set l -> Set l) |
17 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} | 17 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} |
18 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} | 18 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} |
19 (natural-transformation : {A : Set l} -> F A -> G A) | 19 (natural-transformation : {A : Set l} -> F A -> G A) |
20 : Set (suc l) where | 20 : Set (suc l) where |
21 field | 21 field |
25 | 25 |
26 | 26 |
27 | 27 |
28 | 28 |
29 | 29 |
30 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. | 30 -- Categorical Monad definition. without haskell-laws (bind) |
31 record Monad {l : Level} (M : Set l -> Set l) | 31 record Monad {l : Level} (T : Set l -> Set l) (F : Functor T) : Set (suc l) where |
32 (functorM : Functor M) | |
33 : Set (suc l) where | |
34 field -- category | 32 field -- category |
35 mu : {A : Set l} -> M (M A) -> M A | 33 mu : {A : Set l} -> T (T A) -> T A |
36 eta : {A : Set l} -> A -> M A | 34 eta : {A : Set l} -> A -> T A |
37 field -- haskell | 35 field -- natural transformations |
38 return : {A : Set l} -> A -> M A | 36 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap F f (eta x) |
39 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B | 37 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) |
40 field -- category laws | 38 field -- category laws |
41 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x | 39 association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x |
42 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x | 40 left-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x |
43 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x | 41 right-unity-law : {A : Set l} -> (x : T A) -> id x ≡ (mu ∙ eta) x |
44 field -- natural transformations | |
45 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) | |
46 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) | |
47 | 42 |
48 | 43 |
49 open Monad | 44 open Monad |