Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 57:dfcd72dc697e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ReDefine Delta used non-empty-list for infinite changes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 22 Nov 2014 12:29:32 +0900
parents bfb6be9a689d
children 46b15f368905
comparison
equal deleted inserted replaced
56:bfb6be9a689d 57:dfcd72dc697e
5 open import Relation.Binary.PropositionalEquality 5 open import Relation.Binary.PropositionalEquality
6 open ≡-Reasoning 6 open ≡-Reasoning
7 7
8 module delta where 8 module delta where
9 9
10 DeltaLog : Set
11 DeltaLog = List String
12 10
13 data Delta {l : Level} (A : Set l) : (Set (suc l)) where 11 data Delta {l : Level} (A : Set l) : (Set (suc l)) where
14 mono : DeltaLog -> A -> Delta A 12 mono : A -> Delta A
15 delta : DeltaLog -> A -> Delta A -> Delta A 13 delta : A -> Delta A -> Delta A
16
17 logAppend : {l : Level} {A : Set l} -> DeltaLog -> Delta A -> Delta A
18 logAppend l (mono lx x) = mono (l ++ lx) x
19 logAppend l (delta lx x d) = delta (l ++ lx) x (logAppend l d)
20 14
21 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A 15 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
22 deltaAppend (mono lx x) d = delta lx x d 16 deltaAppend (mono x) d = delta x d
23 deltaAppend (delta lx x d) ds = delta lx x (deltaAppend d ds) 17 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
24 18
25 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A 19 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
26 headDelta (mono lx x) = mono lx x 20 headDelta (mono x) = mono x
27 headDelta (delta lx x _) = mono lx x 21 headDelta (delta x _) = mono x
28 22
29 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A 23 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
30 tailDelta (mono lx x) = mono lx x 24 tailDelta (mono x) = mono x
31 tailDelta (delta _ _ d) = d 25 tailDelta (delta _ d) = d
32 26
33 27
34 -- Functor 28 -- Functor
35 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B) 29 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
36 fmap f (mono lx x) = mono lx (f x) 30 fmap f (mono x) = mono (f x)
37 fmap f (delta lx x d) = delta lx (f x) (fmap f d) 31 fmap f (delta x d) = delta (f x) (fmap f d)
38 32
39 33
40 {-# NO_TERMINATION_CHECK #-} 34
41 -- Monad (Category) 35 -- Monad (Category)
42 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 36
43 mu (mono ld d) = logAppend ld d 37 -- TODO: mu
44 mu (delta ld d ds) = deltaAppend (logAppend ld (headDelta d)) (mu (fmap tailDelta ds)) 38 -- TODO: bind
39
45 40
46 eta : {l : Level} {A : Set l} -> A -> Delta A 41 eta : {l : Level} {A : Set l} -> A -> Delta A
47 eta x = mono [] x 42 eta x = mono x
48 43
49 returnS : {l : Level} {A : Set l} -> A -> Delta A 44 returnS : {l : Level} {A : Set l} -> A -> Delta A
50 returnS x = mono [[ (show x) ]] x 45 returnS x = mono x
51 46
52 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A 47 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
53 returnSS x y = delta [[ (show x) ]] x (mono [[ (show y) ]] y) 48 returnSS x y = deltaAppend (returnS x) (returnS y)
54 49
55 50
56 -- Monad (Haskell) 51 -- Monad (Haskell)
57 return : {l : Level} {A : Set l} -> A -> Delta A 52 return : {l : Level} {A : Set l} -> A -> Delta A
58 return = eta 53 return = eta
59 54
60 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} -> 55 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
61 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) 56 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
62 x >>= f = mu (fmap f x) 57 (mono x) >>= f = f x
58 (delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f))
63 59
64 60
65 61
66 -- proofs 62 -- proofs
67
68 -- sub proofs
69 twice-log-append : {l : Level} {A : Set l} -> (l : List String) -> (ll : List String) -> (d : Delta A) ->
70 logAppend l (logAppend ll d) ≡ logAppend (l ++ ll) d
71 twice-log-append l ll (mono lx x) = begin
72 mono (l ++ (ll ++ lx)) x
73 ≡⟨ cong (\l -> mono l x) (list-associative l ll lx) ⟩
74 mono (l ++ ll ++ lx) x
75 ∎
76 twice-log-append l ll (delta lx x d) = begin
77 delta (l ++ (ll ++ lx)) x (logAppend l (logAppend ll d))
78 ≡⟨ cong (\lx -> delta lx x (logAppend l (logAppend ll d))) (list-associative l ll lx) ⟩
79 delta (l ++ ll ++ lx) x (logAppend l (logAppend ll d))
80 ≡⟨ cong (delta (l ++ ll ++ lx) x) (twice-log-append l ll d) ⟩
81 delta (l ++ ll ++ lx) x (logAppend (l ++ ll) d)
82 ∎
83 63
84 64
85 -- Functor-laws 65 -- Functor-laws
86 66
87 -- Functor-law-1 : T(id) = id' 67 -- Functor-law-1 : T(id) = id'
88 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d 68 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
89 functor-law-1 (mono lx x) = refl 69 functor-law-1 (mono x) = refl
90 functor-law-1 (delta lx x d) = cong (delta lx x) (functor-law-1 d) 70 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
91 71
92 -- Functor-law-2 : T(f . g) = T(f) . T(g) 72 -- Functor-law-2 : T(f . g) = T(f) . T(g)
93 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> 73 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
94 (f : B -> C) -> (g : A -> B) -> (d : Delta A) -> 74 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
95 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d 75 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
96 functor-law-2 f g (mono lx x) = refl 76 functor-law-2 f g (mono x) = refl
97 functor-law-2 f g (delta lx x d) = cong (delta lx (f (g x))) (functor-law-2 f g d) 77 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
98 78
99 79
100 80
101 -- Monad-laws (Category) 81 -- Monad-laws (Category)
102 82
103 -- monad-law-1 : join . fmap join = join . join 83 -- monad-law-1 : join . fmap join = join . join
104 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) 84 --monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
105 monad-law-1 (mono lx (mono llx (mono lllx x))) = begin
106 mono (lx ++ (llx ++ lllx)) x
107 ≡⟨ cong (\l -> mono l x) (list-associative lx llx lllx) ⟩
108 mono (lx ++ llx ++ lllx) x
109 ∎
110 monad-law-1 (mono lx (mono llx (delta lllx x d))) = begin
111 delta (lx ++ (llx ++ lllx)) x (logAppend lx (logAppend llx d))
112 ≡⟨ cong (\l -> delta l x (logAppend lx (logAppend llx d))) (list-associative lx llx lllx) ⟩
113 delta (lx ++ llx ++ lllx) x (logAppend lx (logAppend llx d))
114 ≡⟨ cong (\d -> delta (lx ++ llx ++ lllx) x d) (twice-log-append lx llx d) ⟩
115 delta (lx ++ llx ++ lllx) x (logAppend (lx ++ llx) d)
116 ∎
117 monad-law-1 (mono lx (delta ld (mono x x₁) (mono x₂ (mono x₃ x₄)))) = begin
118 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₂ ++ x₃)) x₄)
119 ≡⟨ cong (\l -> delta l x₁(mono (lx ++ (x₂ ++ x₃)) x₄)) (list-associative lx ld x) ⟩
120 delta (lx ++ ld ++ x) x₁ (mono (lx ++ (x₂ ++ x₃)) x₄)
121 ≡⟨ cong (\l -> delta (lx ++ ld ++ x) x₁ (mono l x₄)) (list-associative lx x₂ x₃) ⟩
122 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₂ ++ x₃) x₄)
123 ∎
124 monad-law-1 (mono lx (delta ld (mono x x₁) (mono x₂ (delta x₃ x₄ ds)))) = begin
125 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₂ ds))
126 ≡⟨ cong (\l -> delta l x₁ (logAppend lx (logAppend x₂ ds))) (list-associative lx ld x) ⟩
127 delta (lx ++ ld ++ x) x₁ (logAppend lx (logAppend x₂ ds))
128 ≡⟨ cong (\d -> delta (lx ++ ld ++ x) x₁ d) (twice-log-append lx x₂ ds) ⟩
129 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₂) ds)
130 ∎
131 monad-law-1 (mono lx (delta ld (delta x x₁ (mono x₂ x₃)) (mono x₄ (mono x₅ x₆)))) = begin
132 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)
133 ≡⟨ cong (\l -> delta l x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)) (list-associative lx ld x ) ⟩
134 delta (lx ++ ld ++ x) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)
135 ≡⟨ cong (\l -> delta (lx ++ ld ++ x) x₁ (mono l x₆)) (list-associative lx x₄ x₅)⟩
136 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆)
137 ∎
138 monad-law-1 (mono lx (delta ld (delta x x₁ (mono x₂ x₃)) (mono x₄ (delta x₅ x₆ ds)))) = begin
139 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds))
140 ≡⟨ cong (\l -> delta l x₁(logAppend lx (logAppend x₄ ds))) (list-associative lx ld x ) ⟩
141 delta (lx ++ ld ++ x) x₁ (logAppend lx (logAppend x₄ ds))
142 ≡⟨ cong (\d -> delta (lx ++ ld ++ x) x₁ d) (twice-log-append lx x₄ ds ) ⟩
143 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds)
144 ∎
145
146 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (mono x₂ x₃))) (mono x₄ (mono x₅ x₆)))) = begin
147 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)
148 ≡⟨ {!!} ⟩
149 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆)
150 ∎
151 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (mono x₂ x₃))) (mono x₄ (delta x₅ x₆ ds)))) = begin
152 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds))
153 ≡⟨ {!!} ⟩
154 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds)
155 ∎
156 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (delta x₂ x₃ d))) (mono x₄ (mono x₅ x₆)))) = begin
157 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)
158 ≡⟨ {!!} ⟩
159 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆)
160 ∎
161 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (delta x₂ x₃ d))) (mono x₄ (delta x₅ x₆ ds)))) = begin
162 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds))
163 ≡⟨ {!!} ⟩
164 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds)
165 ∎
166
167 85
168 86
169
170 monad-law-1 (mono lx (delta ld d (delta x ds ds₁))) = {!!}
171
172
173
174 monad-law-1 (delta lx x d) = {!!}
175
176 {- 87 {-
177 -- monad-law-2 : join . fmap return = join . return = id
178 -- monad-law-2-1 join . fmap return = join . return
179 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Delta A) ->
180 (mu ∙ fmap eta) s ≡ (mu ∙ eta) s
181 monad-law-2-1 (similar lx x ly y) = begin
182 similar (lx ++ []) x (ly ++ []) y
183 ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩
184 similar lx x (ly ++ []) y
185 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
186 similar lx x ly y
187 ∎
188
189 -- monad-law-2-2 : join . return = id 88 -- monad-law-2-2 : join . return = id
190 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s 89 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s
191 monad-law-2-2 (similar lx x ly y) = refl 90 monad-law-2-2 (similar lx x ly y) = refl
192 91
193 -- monad-law-3 : return . f = fmap f . return 92 -- monad-law-3 : return . f = fmap f . return
264 ≡⟨ refl ⟩ 163 ≡⟨ refl ⟩
265 (mu (fmap k (similar lx x ly y))) >>= h 164 (mu (fmap k (similar lx x ly y))) >>= h
266 ≡⟨ refl ⟩ 165 ≡⟨ refl ⟩
267 ((similar lx x ly y) >>= k) >>= h 166 ((similar lx x ly y) >>= k) >>= h
268 ∎ 167 ∎
168
269 -} 169 -}