0 | module Control.Comonad.Traced.Interface
 1 |
 2 | import Data.Morphisms
 3 |
 4 | import Control.Comonad
 5 | import Control.Comonad.Env.Env
 6 | import Control.Comonad.Store.Store
 7 | import Control.Comonad.Traced.Traced
 8 | import Control.Comonad.Trans
 9 |
10 | %default total
11 |
12 | public export
13 | interface Comonad w => ComonadTraced m w | w where
14 |   trace : m -> w a -> a
15 |
16 | --------------------------------------------------------------------------------
17 | --          Utilities
18 | --------------------------------------------------------------------------------
19 |
20 | public export %inline
21 | traces : ComonadTraced m w => (a -> m) -> w a -> a
22 | traces f wa = trace (f $ extract wa) wa
23 |
24 | public export %inline
25 | lowerTrace : (ComonadTrans t, ComonadTraced m w) => m -> t w a -> a
26 | lowerTrace m = trace m . lower
27 |
28 | --------------------------------------------------------------------------------
29 | --          Implementations
30 | --------------------------------------------------------------------------------
31 |
32 | public export %inline
33 | Monoid m => ComonadTraced m (Morphism m) where
34 |   trace m (Mor f) = f m
35 |
36 | public export %inline
37 | ComonadTraced m w => ComonadTraced m (EnvT e w) where
38 |   trace = lowerTrace
39 |
40 | public export %inline
41 | ComonadTraced m w => ComonadTraced m (StoreT s w) where
42 |   trace = lowerTrace
43 |
44 | public export %inline
45 | (Comonad w, Monoid m) => ComonadTraced m (TracedT m w) where
46 |   trace m (MkTracedT wf) = extract wf m
47 |