Mercurial > hg > Members > atton > delta_monad
annotate agda/similar.agda @ 27:742e62fc63e4
Define Monad-law 1-4
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 14:53:56 +0900 |
parents | 5ba82f107a95 |
children | 6e6d646d7722 |
rev | line source |
---|---|
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import list |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
3 open ≡-Reasoning |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module similar where |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
7 id : {A : Set} -> A -> A |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
8 id x = x |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
9 |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 postulate String : Set |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 postulate show : {A : Set} -> A -> String |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 data Similar (A : Set) : Set where |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 similar : List String -> A -> List String -> A -> Similar A |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B) |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 mu : {A : Set} -> Similar (Similar A) -> Similar A |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
24 return : {A : Set} -> A -> Similar A |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
25 return x = similar [] x [] x |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
26 |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 returnS : {A : Set} -> A -> Similar A |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 returnSS : {A : Set} -> A -> A -> Similar A |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
34 _∙_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C) |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
35 f ∙ g = \x -> g (f x) |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
36 |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
37 monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
38 monad-law-1 = {!!} |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
39 |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
40 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
41 monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
42 monad-law-2-1 = {!!} |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
43 |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
44 monad-law-2-2 : mu ∙ return ≡ id |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
45 monad-law-2-2 = {!!} |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
46 |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
47 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
48 monad-law-3 = {!!} |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
49 |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
50 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
51 monad-law-4 = {!!} |