Mercurial > hg > Members > atton > similar_monad

comparison agda/similar.agda @ 40:a7cd7740f33e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Haskell style Monad-laws and Proof Monad-laws-h-1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 19 Oct 2014 16:17:46 +0900
parents b9b26b470cc2
children 23474bf242c6
comparison
equal deleted inserted replaced
39:b9b26b470cc2 40:a7cd7740f33e
14 -- Functor 14 -- Functor
15 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Similar A) -> (Similar B) 15 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Similar A) -> (Similar B)
16 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) 16 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
17 17
18 18
19 -- Monad 19 -- Monad (Category)
20 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A 20 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A
21 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y 21 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
22 22
23 return : {l : Level} {A : Set l} -> A -> Similar A 23 eta : {l : Level} {A : Set l} -> A -> Similar A
24 return x = similar [] x [] x 24 eta x = similar [] x [] x
25 25
26 returnS : {l : Level} {A : Set l} -> A -> Similar A 26 returnS : {l : Level} {A : Set l} -> A -> Similar A
27 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 27 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
28 28
29 returnSS : {l : Level} {A : Set l} -> A -> A -> Similar A 29 returnSS : {l : Level} {A : Set l} -> A -> A -> Similar A
30 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y 30 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
31
32
33 -- Monad (Haskell)
34 return : {l : Level} {A : Set l} -> A -> Similar A
35 return = eta
36
37 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
38 (x : Similar A) -> (f : A -> (Similar B)) -> (Similar B)
39 x >>= f = mu (fmap f x)
31 40
32 41
33 42
34 -- proofs 43 -- proofs
35 44
63 72
64 73
65 -- monad-law-2 : join . fmap return = join . return = id 74 -- monad-law-2 : join . fmap return = join . return = id
66 -- monad-law-2-1 join . fmap return = join . return 75 -- monad-law-2-1 join . fmap return = join . return
67 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Similar A) -> 76 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Similar A) ->
68 (mu ∙ fmap return) s ≡ (mu ∙ return) s 77 (mu ∙ fmap eta) s ≡ (mu ∙ eta) s
69 monad-law-2-1 (similar lx x ly y) = begin 78 monad-law-2-1 (similar lx x ly y) = begin
70 similar (lx ++ []) x (ly ++ []) y 79 similar (lx ++ []) x (ly ++ []) y
71 ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩ 80 ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩
72 similar lx x (ly ++ []) y 81 similar lx x (ly ++ []) y
73 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩ 82 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
74 similar lx x ly y 83 similar lx x ly y
75 ∎ 84 ∎
76 85
77 -- monad-law-2-2 : join . return = id 86 -- monad-law-2-2 : join . return = id
78 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Similar A) -> (mu ∙ return) s ≡ id s 87 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Similar A) -> (mu ∙ eta) s ≡ id s
79 monad-law-2-2 (similar lx x ly y) = refl 88 monad-law-2-2 (similar lx x ly y) = refl
80 89
81 -- monad-law-3 : return . f = fmap f . return 90 -- monad-law-3 : return . f = fmap f . return
82 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (return ∙ f) x ≡ (fmap f ∙ return) x 91 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
83 monad-law-3 f x = refl 92 monad-law-3 f x = refl
84 93
85 -- monad-law-4 : join . fmap (fmap f) = fmap f . join 94 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
86 monad-law-4 : {l : Level} {A B : Set l} (f : A -> B) (s : Similar (Similar A)) -> 95 monad-law-4 : {l : Level} {A B : Set l} (f : A -> B) (s : Similar (Similar A)) ->
87 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s 96 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
88 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl 97 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl
98
99
100 -- Monad-laws (Haskell)
101 -- monad-law-h-1 : return a >>= k = k a
102 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
103 (a : A) -> (k : A -> (Similar B)) ->
104 (return a >>= k) ≡ (k a)
105 monad-law-h-1 a k = begin
106 return a >>= k
107 ≡⟨ refl ⟩
108 mu (fmap k (return a))
109 ≡⟨ refl ⟩
110 mu (return (k a))
111 ≡⟨ refl ⟩
112 (mu ∙ return) (k a)
113 ≡⟨ refl ⟩
114 (mu ∙ eta) (k a)
115 ≡⟨ (monad-law-2-2 (k a)) ⟩
116 id (k a)
117 ≡⟨ refl ⟩
118 k a
119 ∎
120
121 -- monad-law-h-2 : m >>= return = m
122 -- monad-law-h-3 : m >>= (× -> k x >>= h) = (m >>= k) >>= h