Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 29:e0ba1bf564dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Apply level to some functions
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Oct 2014 15:09:17 +0900
parents 6e6d646d7722
children c2f40b6d4027
comparison
equal deleted inserted replaced
28:6e6d646d7722 29:e0ba1bf564dd
1 open import list 1 open import list
2 open import basic 2 open import basic
3
4 open import Level
3 open import Relation.Binary.PropositionalEquality 5 open import Relation.Binary.PropositionalEquality
4 open ≡-Reasoning 6 open ≡-Reasoning
5 7
6 module similar where 8 module similar where
7 9
8 data Similar (A : Set) : Set where 10 data Similar {l : Level} (A : Set l) : (Set (suc l)) where
9 similar : List String -> A -> List String -> A -> Similar A 11 similar : List String -> A -> List String -> A -> Similar A
10 12
11 fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B) 13 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Similar A) -> (Similar B)
12 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) 14 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
13 15
14 mu : {A : Set} -> Similar (Similar A) -> Similar A 16 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A
15 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y 17 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
16 18
17 return : {A : Set} -> A -> Similar A 19 return : {A : Set} -> A -> Similar A
18 return x = similar [] x [] x 20 return x = similar [] x [] x
19 21
21 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 23 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
22 24
23 returnSS : {A : Set} -> A -> A -> Similar A 25 returnSS : {A : Set} -> A -> A -> Similar A
24 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y 26 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
25 27
28 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
26 29
27 monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu 30 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
28 monad-law-1 = {!!} 31 monad-law-1 s = begin
32 ((mu ∙ (fmap mu)) s)
33 ≡⟨⟩
34 mu (fmap mu s)
35 ≡⟨ {!!} ⟩
36 mu (mu s)
37 ≡⟨⟩
38 ((mu ∙ mu) s)
39 ∎
29 40
41
42
43
44 {-
30 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id 45 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id
31 monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return 46 monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return
32 monad-law-2-1 = {!!} 47 monad-law-2-1 = {!!}
33 48
34 monad-law-2-2 : mu ∙ return ≡ id 49 monad-law-2-2 : mu ∙ return ≡ id
35 monad-law-2-2 = {!!} 50 monad-law-2-2 = {!!}
36 51
37 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return 52 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
38 monad-law-3 = {!!} 53 monad-law-3 = {!!}
39 54
40 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu 55 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu
41 monad-law-4 = {!!} 56 monad-law-4 = {!!}
57 -}