Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 89:5411ce26d525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Defining DeltaM in Agda...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 11:48:41 +0900
parents
children 55d11ce7e223
comparison
equal deleted inserted replaced
88:526186c4f298 89:5411ce26d525
1 open import Level
2
3 open import delta
4 open import delta.functor
5 open import nat
6 open import laws
7
8 module deltaM where
9
10 -- DeltaM definitions
11
12 data DeltaM {l : Level}
13 (M : {l' : Level} -> Set l' -> Set l')
14 {functorM : {l' : Level} -> Functor {l'} M}
15 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
16 (A : Set l)
17 : Set l where
18 deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A
19
20
21 -- DeltaM utils
22
23 headDeltaM : {l : Level} {A : Set l}
24 {M : {l' : Level} -> Set l' -> Set l'}
25 {functorM : {l' : Level} -> Functor {l'} M}
26 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
27 -> DeltaM M {functorM} {monadM} A -> M A
28 headDeltaM (deltaM (mono x)) = x
29 headDeltaM (deltaM (delta x _)) = x
30
31 tailDeltaM : {l : Level} {A : Set l}
32 {M : {l' : Level} -> Set l' -> Set l'}
33 {functorM : {l' : Level} -> Functor {l'} M}
34 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
35 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
36 tailDeltaM (deltaM (mono x)) = deltaM (mono x)
37 tailDeltaM (deltaM (delta _ d)) = deltaM d
38
39 appendDeltaM : {l : Level} {A : Set l}
40 {M : {l' : Level} -> Set l' -> Set l'}
41 {functorM : {l' : Level} -> Functor {l'} M}
42 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
43 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
44 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd)
45
46
47 checkOut : {l : Level} {A : Set l}
48 {M : {l' : Level} -> Set l' -> Set l'}
49 {functorM : {l' : Level} -> Functor {l'} M}
50 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
51 -> Nat -> DeltaM M {functorM} {monadM} A -> M A
52 checkOut O (deltaM (mono x)) = x
53 checkOut O (deltaM (delta x _)) = x
54 checkOut (S n) (deltaM (mono x)) = x
55 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d)
56
57 {-
58 deltaM-fmap : {l ll : Level} {A : Set l} {B : Set ll}
59 {M : {l' : Level} -> Set l' -> Set l'}
60 {functorM : {l' : Level} -> Functor {l'} M}
61 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
62 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B
63 deltaM-fmap {l} {ll} {A} {B} {M} {functorM} f (deltaM d) = deltaM (Functor.fmap delta-is-functor (Functor.fmap functorM f) d)
64 -}