Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 90:55d11ce7e223

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unify levels on data type. only use suc to proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 12:11:38 +0900
parents 5411ce26d525
children bcd4fe52a504
comparison
equal deleted inserted replaced
89:5411ce26d525 90:55d11ce7e223
40 40
41 -- Monad (Category) 41 -- Monad (Category)
42 eta : {l : Level} {A : Set l} -> A -> Delta A 42 eta : {l : Level} {A : Set l} -> A -> Delta A
43 eta x = mono x 43 eta x = mono x
44 44
45 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B 45 bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B
46 bind (mono x) f = f x 46 bind (mono x) f = f x
47 bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f)) 47 bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f))
48 48
49 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 49 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
50 mu d = bind d id 50 mu d = bind d id
58 58
59 -- Monad (Haskell) 59 -- Monad (Haskell)
60 return : {l : Level} {A : Set l} -> A -> Delta A 60 return : {l : Level} {A : Set l} -> A -> Delta A
61 return = eta 61 return = eta
62 62
63 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} -> 63 _>>=_ : {l : Level} {A B : Set l} ->
64 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) 64 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
65 (mono x) >>= f = f x 65 (mono x) >>= f = f x
66 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f)) 66 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
67 67
68 68