Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 43:90b171e3a73e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename to Delta from Similar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 01 Nov 2014 15:19:04 +0900
parents agda/similar.agda@1df4f9d88025
children 9bb7c9bee94f
comparison
equal deleted inserted replaced
42:1df4f9d88025 43:90b171e3a73e
1 open import list
2 open import basic
3
4 open import Level
5 open import Relation.Binary.PropositionalEquality
6 open ≡-Reasoning
7
8 module delta where
9
10 data Delta {l : Level} (A : Set l) : (Set (suc l)) where
11 similar : List String -> A -> List String -> A -> Delta A
12
13
14 -- Functor
15 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
16 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
17
18
19 -- Monad (Category)
20 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
21 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
22
23 eta : {l : Level} {A : Set l} -> A -> Delta A
24 eta x = similar [] x [] x
25
26 returnS : {l : Level} {A : Set l} -> A -> Delta A
27 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
28
29 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
30 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
31
32
33 -- Monad (Haskell)
34 return : {l : Level} {A : Set l} -> A -> Delta A
35 return = eta
36
37
38 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
39 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
40 x >>= f = mu (fmap f x)
41
42
43
44 -- proofs
45
46
47 -- Functor-laws
48
49 -- Functor-law-1 : T(id) = id'
50 functor-law-1 : {l : Level} {A : Set l} -> (s : Delta A) -> (fmap id) s ≡ id s
51 functor-law-1 (similar lx x ly y) = refl
52
53 -- Functor-law-2 : T(f . g) = T(f) . T(g)
54 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
55 (f : B -> C) -> (g : A -> B) -> (s : Delta A) ->
56 (fmap (f ∙ g)) s ≡ ((fmap f) ∙ (fmap g)) s
57 functor-law-2 f g (similar lx x ly y) = refl
58
59
60
61 -- Monad-laws (Category)
62
63 -- monad-law-1 : join . fmap join = join . join
64 monad-law-1 : {l : Level} {A : Set l} -> (s : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
65 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _))
66 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin
67 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
68 ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩
69 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y
70 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩
71 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
72 ∎
73
74
75 -- monad-law-2 : join . fmap return = join . return = id
76 -- monad-law-2-1 join . fmap return = join . return
77 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Delta A) ->
78 (mu ∙ fmap eta) s ≡ (mu ∙ eta) s
79 monad-law-2-1 (similar lx x ly y) = begin
80 similar (lx ++ []) x (ly ++ []) y
81 ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩
82 similar lx x (ly ++ []) y
83 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
84 similar lx x ly y
85 ∎
86
87 -- monad-law-2-2 : join . return = id
88 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s
89 monad-law-2-2 (similar lx x ly y) = refl
90
91 -- monad-law-3 : return . f = fmap f . return
92 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
93 monad-law-3 f x = refl
94
95 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
96 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (s : Delta (Delta A)) ->
97 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
98 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl
99
100
101 -- Monad-laws (Haskell)
102 -- monad-law-h-1 : return a >>= k = k a
103 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
104 (a : A) -> (k : A -> (Delta B)) ->
105 (return a >>= k) ≡ (k a)
106 monad-law-h-1 a k = begin
107 return a >>= k
108 ≡⟨ refl ⟩
109 mu (fmap k (return a))
110 ≡⟨ refl ⟩
111 mu (return (k a))
112 ≡⟨ refl ⟩
113 (mu ∙ return) (k a)
114 ≡⟨ refl ⟩
115 (mu ∙ eta) (k a)
116 ≡⟨ (monad-law-2-2 (k a)) ⟩
117 id (k a)
118 ≡⟨ refl ⟩
119 k a
120 ∎
121
122 -- monad-law-h-2 : m >>= return = m
123 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= return) ≡ m
124 monad-law-h-2 (similar lx x ly y) = monad-law-2-1 (similar lx x ly y)
125
126 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h
127 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
128 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
129 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
130 monad-law-h-3 (similar lx x ly y) k h = begin
131 ((similar lx x ly y) >>= (\x -> (k x) >>= h))
132 ≡⟨ refl ⟩
133 mu (fmap (\x -> k x >>= h) (similar lx x ly y))
134 ≡⟨ refl ⟩
135 (mu ∙ fmap (\x -> k x >>= h)) (similar lx x ly y)
136 ≡⟨ refl ⟩
137 (mu ∙ fmap (\x -> mu (fmap h (k x)))) (similar lx x ly y)
138 ≡⟨ refl ⟩
139 (mu ∙ fmap (mu ∙ (\x -> fmap h (k x)))) (similar lx x ly y)
140 ≡⟨ refl ⟩
141 (mu ∙ (fmap mu ∙ (fmap (\x -> fmap h (k x))))) (similar lx x ly y)
142 ≡⟨ refl ⟩
143 (mu ∙ (fmap mu)) ((fmap (\x -> fmap h (k x))) (similar lx x ly y))
144 ≡⟨ monad-law-1 (((fmap (\x -> fmap h (k x))) (similar lx x ly y))) ⟩
145 (mu ∙ mu) ((fmap (\x -> fmap h (k x))) (similar lx x ly y))
146 ≡⟨ refl ⟩
147 (mu ∙ (mu ∙ (fmap (\x -> fmap h (k x))))) (similar lx x ly y)
148 ≡⟨ refl ⟩
149 (mu ∙ (mu ∙ (fmap ((fmap h) ∙ k)))) (similar lx x ly y)
150 ≡⟨ refl ⟩
151 (mu ∙ (mu ∙ ((fmap (fmap h)) ∙ (fmap k)))) (similar lx x ly y)
152 ≡⟨ refl ⟩
153 (mu ∙ (mu ∙ (fmap (fmap h)))) (fmap k (similar lx x ly y))
154 ≡⟨ refl ⟩
155 mu ((mu ∙ (fmap (fmap h))) (fmap k (similar lx x ly y)))
156 ≡⟨ cong (\fx -> mu fx) (monad-law-4 h (fmap k (similar lx x ly y))) ⟩
157 mu (fmap h (mu (similar lx (k x) ly (k y))))
158 ≡⟨ refl ⟩
159 (mu ∙ fmap h) (mu (fmap k (similar lx x ly y)))
160 ≡⟨ refl ⟩
161 mu (fmap h (mu (fmap k (similar lx x ly y))))
162 ≡⟨ refl ⟩
163 (mu (fmap k (similar lx x ly y))) >>= h
164 ≡⟨ refl ⟩
165 ((similar lx x ly y) >>= k) >>= h
166 ∎