Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 28:6e6d646d7722

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split basic functions to file
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Oct 2014 14:55:40 +0900
parents 742e62fc63e4
children e0ba1bf564dd
comparison
equal deleted inserted replaced
27:742e62fc63e4 28:6e6d646d7722
1 open import list 1 open import list
2 open import basic
2 open import Relation.Binary.PropositionalEquality 3 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning 4 open ≡-Reasoning
4 5
5 module similar where 6 module similar where
6 7
7 id : {A : Set} -> A -> A
8 id x = x
9
10 postulate String : Set
11 postulate show : {A : Set} -> A -> String
12
13 data Similar (A : Set) : Set where 8 data Similar (A : Set) : Set where
14 similar : List String -> A -> List String -> A -> Similar A 9 similar : List String -> A -> List String -> A -> Similar A
15 10
16
17 fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B) 11 fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B)
18 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) 12 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
19
20 13
21 mu : {A : Set} -> Similar (Similar A) -> Similar A 14 mu : {A : Set} -> Similar (Similar A) -> Similar A
22 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y 15 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
23 16
24 return : {A : Set} -> A -> Similar A 17 return : {A : Set} -> A -> Similar A
28 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 21 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
29 22
30 returnSS : {A : Set} -> A -> A -> Similar A 23 returnSS : {A : Set} -> A -> A -> Similar A
31 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y 24 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
32 25
33
34 _∙_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C)
35 f ∙ g = \x -> g (f x)
36 26
37 monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu 27 monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
38 monad-law-1 = {!!} 28 monad-law-1 = {!!}
39 29
40 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id 30 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id