Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 104:ebd0d6e2772c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying redenition Delta with length constraints
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 23:00:05 +0900
parents a271f3ff1922
children e6499a50ccbd
comparison
equal deleted inserted replaced
103:a271f3ff1922 104:ebd0d6e2772c
1 open import basic 1 open import basic
2 open import delta 2 open import delta
3 open import delta.functor 3 open import delta.functor
4 open import nat 4 open import nat
5 open import laws 5 open import laws
6 open import revision
6 7
7 8
8 open import Level 9 open import Level
9 open import Relation.Binary.PropositionalEquality 10 open import Relation.Binary.PropositionalEquality
10 open ≡-Reasoning 11 open ≡-Reasoning
11 12
12 module delta.monad where 13 module delta.monad where
13 14
14 15
15 -- Monad-laws (Category) 16 -- Monad-laws (Category)
17 {-
16 18
17 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> 19 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
18 n-tail n (delta-bind ds (n-tail m)) ≡ delta-bind (n-tail n ds) (n-tail (m + n)) 20 n-tail n (delta-bind ds (n-tail m)) ≡ delta-bind (n-tail n ds) (n-tail (m + n))
19 monad-law-1-5 O O ds = refl 21 monad-law-1-5 O O ds = refl
20 monad-law-1-5 O (S n) (mono ds) = begin 22 monad-law-1-5 O (S n) (mono ds) = begin
320 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩ 322 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩
321 delta-fmap f (delta (headDelta (delta x d)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩ 323 delta-fmap f (delta (headDelta (delta x d)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
322 delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩ 324 delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩
323 (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎ 325 (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎
324 326
325 delta-is-monad : {l : Level} -> Monad {l} Delta delta-is-functor 327 -}
328 -- monad-law-1 : join . delta-fmap join = join . join
329 monad-law-1 : {l : Level} {A : Set l} {a : Rev} -> (d : Delta (Delta (Delta A a) a) a) ->
330 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
331 monad-law-1 (mono d) = refl
332 monad-law-1 (delta d ds) = {!!}
333
334 delta-is-monad : {l : Level} {v : Rev} -> Monad {l} (\A -> Delta A v) delta-is-functor
335
336
326 delta-is-monad = record { eta = delta-eta; 337 delta-is-monad = record { eta = delta-eta;
327 mu = delta-mu; 338 mu = delta-mu;
328 return = delta-eta; 339 return = delta-eta;
329 bind = delta-bind; 340 bind = delta-bind;
330 association-law = monad-law-1; 341 association-law = monad-law-1 }
331 left-unity-law = monad-law-2; 342 -- left-unity-law = monad-law-2;
332 right-unity-law = monad-law-2' } 343 -- right-unity-law = monad-law-2' }
344
345
333 346
334 347
335 348
336 {- 349 {-
337 350