comparison agda/deltaM.agda @ 94:bcd4fe52a504

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 cf372fbcebd8
comparison
equal deleted inserted replaced
93:8d92ed54a94f 94:bcd4fe52a504
1 open import Level 1 open import Level
2 2
3 open import basic
3 open import delta 4 open import delta
4 open import delta.functor 5 open import delta.functor
5 open import nat 6 open import nat
6 open import laws 7 open import laws
7 8
53 checkOut O (deltaM (delta x _)) = x 54 checkOut O (deltaM (delta x _)) = x
54 checkOut (S n) (deltaM (mono x)) = x 55 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 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d)
56 57
57 58
59
60 -- functor definitions
58 open Functor 61 open Functor
59 deltaM-fmap : {l : Level} {A B : Set l} 62 deltaM-fmap : {l : Level} {A B : Set l}
60 {M : {l' : Level} -> Set l' -> Set l'} 63 {M : {l' : Level} -> Set l' -> Set l'}
61 {functorM : {l' : Level} -> Functor {l'} M} 64 {functorM : {l' : Level} -> Functor {l'} M}
62 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 65 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
63 -> (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
64 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
69 -- monad definitions
70 open Monad
71 deltaM-eta : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'}
72 {functorM : {l' : Level} -> Functor {l'} M}
73 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
74 -> A -> (DeltaM M {functorM} {monadM} A)
75 deltaM-eta {_} {A} {_} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x))
76
77 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'}
78 {functorM : {l' : Level} -> Functor {l'} M}
79 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
80 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B
81 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (mono x)) f = deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))
82 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f))))
83 (deltaM-bind (deltaM d) (tailDeltaM ∙ f))
84
85 deltaM-mu : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'}
86 {functorM : {l' : Level} -> Functor {l'} M}
87 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
88 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
89 deltaM-mu d = deltaM-bind d id