Mercurial > hg > Members > atton > delta_monad
annotate agda/laws.agda @ 103:a271f3ff1922
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 |
rev | line source |
---|---|
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Relation.Binary.PropositionalEquality |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import basic |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module laws where |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
7 record Functor {l : Level} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 field |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 field |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
14 |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open Functor |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
17 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
18 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
19 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
20 (natural-transformation : {A : Set l} -> F A -> G A) |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
21 : Set (suc l) where |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
22 field |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
23 commute : {A B : Set l} -> (f : A -> B) -> (x : F A) -> |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
24 natural-transformation (fmapF f x) ≡ fmapG f (natural-transformation x) |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
25 open NaturalTransformation |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
32 record Monad {l : Level} (M : {ll : Level} -> Set ll -> Set ll) |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
33 (functorM : Functor {l} M) |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 : Set (suc l) where |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
35 field -- category |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
36 mu : {A : Set l} -> M (M A) -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
37 eta : {A : Set l} -> A -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
38 field -- haskell |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
39 return : {A : Set l} -> A -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
40 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
41 field -- category laws |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
42 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x |
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
43 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x |
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
44 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
97
diff
changeset
|
45 field -- natural transformations |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
46 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
97
diff
changeset
|
47 |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
49 open Monad |