Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 105:e6499a50ccbd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Retrying prove monad-laws for delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 27 Jan 2015 17:49:25 +0900
parents ebd0d6e2772c
children d205ff1e406f
comparison
equal deleted inserted replaced
104:ebd0d6e2772c 105:e6499a50ccbd
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
5 open import laws 4 open import laws
6 5
7 open import Level 6 open import Level
8 open import Relation.Binary.PropositionalEquality 7 open import Relation.Binary.PropositionalEquality
9 open ≡-Reasoning 8 open ≡-Reasoning
10 9
11 module delta where 10 module delta where
12 11
13 data Delta {l : Level} (A : Set l) : (Rev -> (Set l)) where 12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where
14 mono : A -> Delta A init 13 mono : A -> Delta A (S O)
15 delta : {v : Rev} -> A -> Delta A v -> Delta A (commit v) 14 delta : {n : Nat} -> A -> Delta A (S n) -> Delta A (S (S n))
16 15
17 deltaAppend : {l : Level} {A : Set l} {n m : Rev} -> Delta A n -> Delta A m -> Delta A (merge n m) 16 deltaAppend : {l : Level} {A : Set l} {n m : Nat} -> Delta A (S n) -> Delta A (S m) -> Delta A ((S n) + (S m))
18 deltaAppend (mono x) d = delta x d 17 deltaAppend (mono x) d = delta x d
19 deltaAppend (delta x d) ds = delta x (deltaAppend d ds) 18 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
20 19
21 headDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A n -> A 20 headDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S n) -> A
22 headDelta (mono x) = x 21 headDelta (mono x) = x
23 headDelta (delta x _) = x 22 headDelta (delta x _) = x
24 23
25 tailDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A (commit n) -> Delta A n 24 tailDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S (S n)) -> Delta A (S n)
26 tailDelta (delta _ d) = d 25 tailDelta (delta _ d) = d
27 26
28 27
29 28
30 -- Functor 29 -- Functor
31 delta-fmap : {l : Level} {A B : Set l} {n : Rev} -> (A -> B) -> (Delta A n) -> (Delta B n) 30 delta-fmap : {l : Level} {A B : Set l} {n : Nat} -> (A -> B) -> (Delta A (S n)) -> (Delta B (S n))
32 delta-fmap f (mono x) = mono (f x) 31 delta-fmap f (mono x) = mono (f x)
33 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) 32 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
34 33
35 34
36 35
37 -- Monad (Category) 36 -- Monad (Category)
38 delta-eta : {l : Level} {A : Set l} {v : Rev} -> A -> Delta A v 37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n)
39 delta-eta {v = init} x = mono x 38 delta-eta {n = O} x = mono x
40 delta-eta {v = commit v} x = delta x (delta-eta {v = v} x) 39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x)
41 40
42 delta-bind : {l : Level} {A B : Set l} {n : Rev} -> (Delta A n) -> (A -> Delta B n) -> Delta B n
43 delta-bind (mono x) f = f x
44 delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x))
45 41
46 delta-mu : {l : Level} {A : Set l} {n : Rev} -> (Delta (Delta A n) n) -> Delta A n
47 delta-mu d = delta-bind d id
48 42
43
44 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n)
45 delta-mu (mono x) = x
46 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d))
47
48 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n)
49 delta-bind d f = delta-mu (delta-fmap f d)
50
51 --delta-bind (mono x) f = f x
52 --delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x))
49 53
50 54
51 {- 55 {-
52 -- Monad (Haskell) 56 -- Monad (Haskell)
53 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) 57 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O)