Mercurial > hg > Members > atton > delta_monad
comparison 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 |
comparison
equal
deleted
inserted
replaced
26:5ba82f107a95 | 27:742e62fc63e4 |
---|---|
1 open import list | 1 open import list |
2 open import Relation.Binary.PropositionalEquality | |
3 open ≡-Reasoning | |
2 | 4 |
3 module similar where | 5 module similar where |
6 | |
7 id : {A : Set} -> A -> A | |
8 id x = x | |
4 | 9 |
5 postulate String : Set | 10 postulate String : Set |
6 postulate show : {A : Set} -> A -> String | 11 postulate show : {A : Set} -> A -> String |
7 | 12 |
8 data Similar (A : Set) : Set where | 13 data Similar (A : Set) : Set where |
14 | 19 |
15 | 20 |
16 mu : {A : Set} -> Similar (Similar A) -> Similar A | 21 mu : {A : Set} -> Similar (Similar A) -> Similar A |
17 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y | 22 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y |
18 | 23 |
24 return : {A : Set} -> A -> Similar A | |
25 return x = similar [] x [] x | |
26 | |
19 returnS : {A : Set} -> A -> Similar A | 27 returnS : {A : Set} -> A -> Similar A |
20 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x | 28 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x |
21 | 29 |
22 returnSS : {A : Set} -> A -> A -> Similar A | 30 returnSS : {A : Set} -> A -> A -> Similar A |
23 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y | 31 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y |
24 | 32 |
25 | 33 |
34 _∙_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C) | |
35 f ∙ g = \x -> g (f x) | |
36 | |
37 monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu | |
38 monad-law-1 = {!!} | |
39 | |
40 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id | |
41 monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return | |
42 monad-law-2-1 = {!!} | |
43 | |
44 monad-law-2-2 : mu ∙ return ≡ id | |
45 monad-law-2-2 = {!!} | |
46 | |
47 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return | |
48 monad-law-3 = {!!} | |
49 | |
50 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu | |
51 monad-law-4 = {!!} |