Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte type dependencie in Monad record for escape implicit type conflict
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 14:08:46 +0900
parents 29c54b0197fb
children ebd0d6e2772c
comparison
equal deleted inserted replaced
102:9c62373bd474 103:a271f3ff1922
11 -- DeltaM definitions 11 -- DeltaM definitions
12 12
13 data DeltaM {l : Level} 13 data DeltaM {l : Level}
14 (M : {l' : Level} -> Set l' -> Set l') 14 (M : {l' : Level} -> Set l' -> Set l')
15 {functorM : {l' : Level} -> Functor {l'} M} 15 {functorM : {l' : Level} -> Functor {l'} M}
16 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 16 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM}
17 (A : Set l) 17 (A : Set l)
18 : Set l where 18 : Set l where
19 deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A 19 deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A
20 20
21 21
22 -- DeltaM utils 22 -- DeltaM utils
23 23
24 headDeltaM : {l : Level} {A : Set l} 24 headDeltaM : {l : Level} {A : Set l}
25 {M : {l' : Level} -> Set l' -> Set l'} 25 {M : {l' : Level} -> Set l' -> Set l'}
26 {functorM : {l' : Level} -> Functor {l'} M} 26 {functorM : {l' : Level} -> Functor {l'} M}
27 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 27 {monadM : {l' : Level} -> Monad {l'} M functorM}
28 -> DeltaM M {functorM} {monadM} A -> M A 28 -> DeltaM M {functorM} {monadM} A -> M A
29 headDeltaM (deltaM d) = headDelta d 29 headDeltaM (deltaM d) = headDelta d
30 30
31 31
32 tailDeltaM : {l : Level} {A : Set l} 32 tailDeltaM : {l : Level} {A : Set l}
33 {M : {l' : Level} -> Set l' -> Set l'} 33 {M : {l' : Level} -> Set l' -> Set l'}
34 {functorM : {l' : Level} -> Functor {l'} M} 34 {functorM : {l' : Level} -> Functor {l'} M}
35 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 35 {monadM : {l' : Level} -> Monad {l'} M functorM}
36 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A 36 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
37 tailDeltaM (deltaM d) = deltaM (tailDelta d) 37 tailDeltaM (deltaM d) = deltaM (tailDelta d)
38 38
39 39
40 appendDeltaM : {l : Level} {A : Set l} 40 appendDeltaM : {l : Level} {A : Set l}
41 {M : {l' : Level} -> Set l' -> Set l'} 41 {M : {l' : Level} -> Set l' -> Set l'}
42 {functorM : {l' : Level} -> Functor {l'} M} 42 {functorM : {l' : Level} -> Functor {l'} M}
43 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 43 {monadM : {l' : Level} -> Monad {l'} M functorM}
44 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A 44 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
45 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) 45 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd)
46 46
47 47
48 checkOut : {l : Level} {A : Set l} 48 checkOut : {l : Level} {A : Set l}
49 {M : {l' : Level} -> Set l' -> Set l'} 49 {M : {l' : Level} -> Set l' -> Set l'}
50 {functorM : {l' : Level} -> Functor {l'} M} 50 {functorM : {l' : Level} -> Functor {l'} M}
51 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 51 {monadM : {l' : Level} -> Monad {l'} M functorM}
52 -> Nat -> DeltaM M {functorM} {monadM} A -> M A 52 -> Nat -> DeltaM M {functorM} {monadM} A -> M A
53 checkOut O (deltaM (mono x)) = x 53 checkOut O (deltaM (mono x)) = x
54 checkOut O (deltaM (delta x _)) = x 54 checkOut O (deltaM (delta x _)) = x
55 checkOut (S n) (deltaM (mono x)) = x 55 checkOut (S n) (deltaM (mono x)) = x
56 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d) 56 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d)
60 -- functor definitions 60 -- functor definitions
61 open Functor 61 open Functor
62 deltaM-fmap : {l : Level} {A B : Set l} 62 deltaM-fmap : {l : Level} {A B : Set l}
63 {M : {l' : Level} -> Set l' -> Set l'} 63 {M : {l' : Level} -> Set l' -> Set l'}
64 {functorM : {l' : Level} -> Functor {l'} M} 64 {functorM : {l' : Level} -> Functor {l'} M}
65 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 65 {monadM : {l' : Level} -> Monad {l'} M functorM}
66 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B 66 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B
67 deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) 67 deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d)
68 68
69 -- monad definitions 69 -- monad definitions
70 open Monad 70 open Monad
71 deltaM-eta : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} 71 deltaM-eta : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'}
72 {functorM : {l' : Level} -> Functor {l'} M} 72 {functorM : {l' : Level} -> Functor {l'} M}
73 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 73 {monadM : {l' : Level} -> Monad {l'} M functorM}
74 -> A -> (DeltaM M {functorM} {monadM} A) 74 -> A -> (DeltaM M {functorM} {monadM} A)
75 deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x)) 75 deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta monadM x))
76 76
77 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} 77 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'}
78 {functorM : {l' : Level} -> Functor {l'} M} 78 {functorM : {l' : Level} -> Functor {l'} M}
79 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 79 {monadM : {l' : Level} -> Monad {l'} M functorM}
80 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A 80 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
81 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (mu {l} {A} monadM (fmap functorM headDeltaM x))) 81 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (mu monadM (fmap functorM headDeltaM x)))
82 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM))) 82 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM)))
83 (deltaM-mu (deltaM (mono xx))) 83 (deltaM-mu (deltaM (mono xx)))
84 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM))) 84 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} monadM x headDeltaM)))
85 (deltaM-mu (deltaM d)) 85 (deltaM-mu (deltaM d))
86 -- original deltaM-mu definitions. but it's cannot termination checking. 86 -- original deltaM-mu definitions. but it's cannot termination checking.
87 -- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu. 87 -- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu.
88 {- 88 {-
89 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM))) 89 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM)))
90 (deltaM-mu (deltaM (tailDelta d))) 90 (deltaM-mu (deltaM (tailDelta d)))
91 -} 91 -}
92 92
93 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} 93 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'}
94 {functorM : {l' : Level} -> Functor {l'} M} 94 {functorM : {l' : Level} -> Functor {l'} M}
95 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 95 {monadM : {l' : Level} -> Monad {l'} M functorM}
96 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B 96 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B
97 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d) 97 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d)