Mercurial > hg > Members > atton > delta_monad
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 |