Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.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 dfe8c67390bd
children e6499a50ccbd
comparison
equal deleted inserted replaced
103:a271f3ff1922 104:ebd0d6e2772c
1 open import list 1 open import list
2 open import basic 2 open import basic
3 open import nat 3 open import nat
4 open import revision
4 open import laws 5 open import laws
5 6
6 open import Level 7 open import Level
7 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
8 open ≡-Reasoning 9 open ≡-Reasoning
9 10
10 module delta where 11 module delta where
11 12
13 data Delta {l : Level} (A : Set l) : (Rev -> (Set l)) where
14 mono : A -> Delta A init
15 delta : {v : Rev} -> A -> Delta A v -> Delta A (commit v)
12 16
13 data Delta {l : Level} (A : Set l) : (Set l) where 17 deltaAppend : {l : Level} {A : Set l} {n m : Rev} -> Delta A n -> Delta A m -> Delta A (merge n m)
14 mono : A -> Delta A
15 delta : A -> Delta A -> Delta A
16
17 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
18 deltaAppend (mono x) d = delta x d 18 deltaAppend (mono x) d = delta x d
19 deltaAppend (delta x d) ds = delta x (deltaAppend d ds) 19 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
20 20
21 headDelta : {l : Level} {A : Set l} -> Delta A -> A 21 headDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A n -> A
22 headDelta (mono x) = x 22 headDelta (mono x) = x
23 headDelta (delta x _) = x 23 headDelta (delta x _) = x
24 24
25 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A 25 tailDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A (commit n) -> Delta A n
26 tailDelta (mono x) = mono x
27 tailDelta (delta _ d) = d 26 tailDelta (delta _ d) = d
28 27
29 n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A))
30 n-tail O = id
31 n-tail (S n) = tailDelta ∙ (n-tail n)
32 28
33 29
34 -- Functor 30 -- Functor
35 delta-fmap : {l : Level} {A B : Set l} -> (A -> B) -> (Delta A) -> (Delta B) 31 delta-fmap : {l : Level} {A B : Set l} {n : Rev} -> (A -> B) -> (Delta A n) -> (Delta B n)
36 delta-fmap f (mono x) = mono (f x) 32 delta-fmap f (mono x) = mono (f x)
37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) 33 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
38 34
39 35
40 36
41 -- Monad (Category) 37 -- Monad (Category)
42 delta-eta : {l : Level} {A : Set l} -> A -> Delta A 38 delta-eta : {l : Level} {A : Set l} {v : Rev} -> A -> Delta A v
43 delta-eta x = mono x 39 delta-eta {v = init} x = mono x
40 delta-eta {v = commit v} x = delta x (delta-eta {v = v} x)
44 41
45 delta-bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B 42 delta-bind : {l : Level} {A B : Set l} {n : Rev} -> (Delta A n) -> (A -> Delta B n) -> Delta B n
46 delta-bind (mono x) f = f x 43 delta-bind (mono x) f = f x
47 delta-bind (delta x d) f = delta (headDelta (f x)) (delta-bind d (tailDelta ∙ f)) 44 delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x))
48 45
49 delta-mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 46 delta-mu : {l : Level} {A : Set l} {n : Rev} -> (Delta (Delta A n) n) -> Delta A n
50 delta-mu d = delta-bind d id 47 delta-mu d = delta-bind d id
51 48
52 49
53 50
51 {-
54 -- Monad (Haskell) 52 -- Monad (Haskell)
55 delta-return : {l : Level} {A : Set l} -> A -> Delta A 53 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O)
56 delta-return = delta-eta 54 delta-return = delta-eta
57 55
58 _>>=_ : {l : Level} {A B : Set l} -> 56 _>>=_ : {l : Level} {A B : Set l} {n : Nat} ->
59 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) 57 (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n)
60 (mono x) >>= f = f x 58 d >>= f = delta-bind d f
61 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
62 59
60 -}
63 61
64 62 {-
65 -- proofs 63 -- proofs
66 64
67 -- sub-proofs 65 -- sub-proofs
68 66
69 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) 67 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n)
120 ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩ 118 ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩
121 n-tail n (delta-fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩ 119 n-tail n (delta-fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩
122 delta-fmap f (n-tail n d) ≡⟨ refl ⟩ 120 delta-fmap f (n-tail n d) ≡⟨ refl ⟩
123 delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩ 121 delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩
124 delta-fmap f (n-tail (S n) (delta x d)) ∎ 122 delta-fmap f (n-tail (S n) (delta x d)) ∎
123 -}