Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 96:dfe8c67390bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unify Levels in delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 20 Jan 2015 16:25:53 +0900
parents bcd4fe52a504
children a271f3ff1922
comparison
equal deleted inserted replaced
95:cf372fbcebd8 96:dfe8c67390bd
126 headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ 126 headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩
127 headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds)))) 127 headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds))))
128 ∎ 128 ∎
129 129
130 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (delta-mu d) ≡ (headDelta (headDelta d)) 130 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (delta-mu d) ≡ (headDelta (headDelta d))
131 monad-law-1-2 (mono _) = refl 131 monad-law-1-2 (mono _) = refl
132 monad-law-1-2 (delta _ _) = refl 132 monad-law-1-2 (delta _ _) = refl
133 133
134 monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) -> 134 monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) ->
135 delta-bind (delta-fmap delta-mu d) (n-tail n) ≡ delta-bind (delta-bind d (n-tail n)) (n-tail n) 135 delta-bind (delta-fmap delta-mu d) (n-tail n) ≡ delta-bind (delta-bind d (n-tail n)) (n-tail n)
136 monad-law-1-3 O (mono d) = refl 136 monad-law-1-3 O (mono d) = refl
263 -- monad-law-3 : return . f = delta-fmap f . return 263 -- monad-law-3 : return . f = delta-fmap f . return
264 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (delta-eta ∙ f) x ≡ (delta-fmap f ∙ delta-eta) x 264 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (delta-eta ∙ f) x ≡ (delta-fmap f ∙ delta-eta) x
265 monad-law-3 f x = refl 265 monad-law-3 f x = refl
266 266
267 267
268 monad-law-4-1 : {l ll : Level} {A : Set l} {B : Set ll} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) -> 268 monad-law-4-1 : {l : Level} {A B : Set l} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) ->
269 delta-bind (delta-fmap (delta-fmap f) ds) (n-tail n) ≡ delta-fmap f (delta-bind ds (n-tail n)) 269 delta-bind (delta-fmap (delta-fmap f) ds) (n-tail n) ≡ delta-fmap f (delta-bind ds (n-tail n))
270 monad-law-4-1 O f (mono d) = refl 270 monad-law-4-1 O f (mono d) = refl
271 monad-law-4-1 O f (delta d ds) = begin 271 monad-law-4-1 O f (delta d ds) = begin
272 delta-bind (delta-fmap (delta-fmap f) (delta d ds)) (n-tail O) ≡⟨ refl ⟩ 272 delta-bind (delta-fmap (delta-fmap f) (delta d ds)) (n-tail O) ≡⟨ refl ⟩
273 delta-bind (delta (delta-fmap f d) (delta-fmap (delta-fmap f) ds)) (n-tail O) ≡⟨ refl ⟩ 273 delta-bind (delta (delta-fmap f d) (delta-fmap (delta-fmap f) ds)) (n-tail O) ≡⟨ refl ⟩
330 association-law = monad-law-1; 330 association-law = monad-law-1;
331 left-unity-law = monad-law-2; 331 left-unity-law = monad-law-2;
332 right-unity-law = monad-law-2' } 332 right-unity-law = monad-law-2' }
333 333
334 334
335
335 {- 336 {-
337
336 -- Monad-laws (Haskell) 338 -- Monad-laws (Haskell)
337 -- monad-law-h-1 : return a >>= k = k a 339 -- monad-law-h-1 : return a >>= k = k a
338 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} -> 340 monad-law-h-1 : {l : Level} {A B : Set l} ->
339 (a : A) -> (k : A -> (Delta B)) -> 341 (a : A) -> (k : A -> (Delta B)) ->
340 (return a >>= k) ≡ (k a) 342 (delta-return a >>= k) ≡ (k a)
341 monad-law-h-1 a k = refl 343 monad-law-h-1 a k = refl
342 344
343 345
344 346
345 -- monad-law-h-2 : m >>= return = m 347 -- monad-law-h-2 : m >>= return = m
346 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= return) ≡ m 348 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= delta-return) ≡ m
347 monad-law-h-2 (mono x) = refl 349 monad-law-h-2 (mono x) = refl
348 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d) 350 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
349 351
350 352
351 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h 353
352 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> 354 -- monad-law-h-3 : m >>= (\x -> f x >>= g) = (m >>= f) >>= g
353 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) -> 355 monad-law-h-3 : {l : Level} {A B C : Set l} ->
354 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h) 356 (m : Delta A) -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) ->
355 monad-law-h-3 (mono x) k h = refl 357 (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g)
356 monad-law-h-3 (delta x d) k h = {!!} 358 monad-law-h-3 (mono x) f g = refl
359 monad-law-h-3 (delta x d) f g = begin
360 (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩
361 (delta-bind (delta-bind (delta x d) f) g) ∎
362
363
364
357 365
358 -} 366 -}
359