0 | module Control.Comonad.Traced.Traced
 1 |
 2 | import Control.Comonad
 3 | import Control.Comonad.Trans
 4 | import Control.Monad.Identity
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | record TracedT (m : Type) (w : Type -> Type) (a : Type) where
10 |   constructor MkTracedT
11 |   runTracedT : w (m -> a)
12 |
13 | public export
14 | Traced : (m : Type) -> (a : Type) -> Type
15 | Traced m = TracedT m Identity
16 |
17 | public export %inline
18 | traced : (m -> a) -> Traced m a
19 | traced f = MkTracedT (Id f)
20 |
21 | public export %inline
22 | runTraced : Traced m a -> m -> a
23 | runTraced (MkTracedT (Id f)) = f
24 |
25 | --------------------------------------------------------------------------------
26 | --          Utilities
27 | --------------------------------------------------------------------------------
28 |
29 | public export %inline
30 | listen : Functor w => TracedT m w a -> TracedT m w (a, m)
31 | listen = { runTracedT $= map (\f,m => (f m, m)) }
32 |
33 | public export %inline
34 | listens : Functor w => (m -> b) -> TracedT m w a -> TracedT m w (a, b)
35 | listens g = { runTracedT $= map (\f,m => (f m, g m)) }
36 |
37 | public export %inline
38 | censor : Functor w => (m -> m) -> TracedT m w a -> TracedT m w a
39 | censor g = { runTracedT $= map (. g) }
40 |
41 | --------------------------------------------------------------------------------
42 | --          Interface Implementations
43 | --------------------------------------------------------------------------------
44 |
45 | appEnv : (s -> a -> b) -> (s -> a) -> s -> b
46 | appEnv ff fa s = ff s (fa s)
47 |
48 | public export %inline
49 | Functor w => Functor (TracedT m w) where
50 |   map f = { runTracedT $= map (f .) }
51 |
52 | public export %inline
53 | Applicative w => Applicative (TracedT m w) where
54 |   pure = MkTracedT . pure . const
55 |   MkTracedT wf <*> MkTracedT wa = MkTracedT (map appEnv wf <*> wa)
56 |
57 | public export %inline
58 | (Comonad w, Monoid m) => Comonad (TracedT m w) where
59 |   extract (MkTracedT wf) = extract wf neutral
60 |   extend f =
61 |     { runTracedT $= extend (\w,m => f (MkTracedT $ map (. (<+> m)) w)) }
62 |
63 | public export %inline
64 | (ComonadApply w, Monoid m) => ComonadApply (TracedT m w) where
65 |   MkTracedT wf <@> MkTracedT wa = MkTracedT (map appEnv wf <@> wa)
66 |
67 | public export %inline
68 | Monoid m => ComonadTrans (TracedT m) where
69 |   lower = map ($ neutral) . runTracedT
70 |