Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 94:bcd4fe52a504

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rewrite monad definitions for delta/deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 17:10:29 +0900
parents 55d11ce7e223
children dfe8c67390bd
comparison
equal deleted inserted replaced
93:8d92ed54a94f 94:bcd4fe52a504
37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) 37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
38 38
39 39
40 40
41 -- Monad (Category) 41 -- Monad (Category)
42 eta : {l : Level} {A : Set l} -> A -> Delta A 42 delta-eta : {l : Level} {A : Set l} -> A -> Delta A
43 eta x = mono x 43 delta-eta x = mono x
44 44
45 bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B 45 delta-bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B
46 bind (mono x) f = f x 46 delta-bind (mono x) f = f x
47 bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f)) 47 delta-bind (delta x d) f = delta (headDelta (f x)) (delta-bind d (tailDelta ∙ f))
48 48
49 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 49 delta-mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
50 mu d = bind d id 50 delta-mu d = delta-bind d id
51 51
52 returnS : {l : Level} {A : Set l} -> A -> Delta A
53 returnS x = mono x
54
55 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
56 returnSS x y = deltaAppend (returnS x) (returnS y)
57 52
58 53
59 -- Monad (Haskell) 54 -- Monad (Haskell)
60 return : {l : Level} {A : Set l} -> A -> Delta A 55 delta-return : {l : Level} {A : Set l} -> A -> Delta A
61 return = eta 56 delta-return = delta-eta
62 57
63 _>>=_ : {l : Level} {A B : Set l} -> 58 _>>=_ : {l : Level} {A B : Set l} ->
64 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) 59 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
65 (mono x) >>= f = f x 60 (mono x) >>= f = f x
66 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f)) 61 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
67 62
68 63
69 64
70 -- proofs 65 -- proofs