Control.Comonad.Transformerless.Traced

newtype Traced m a

Constructors

• Traced (m -> a)

Instances

• Newtype (Traced w a) _
• Functor (Traced m)
• (Semigroup m) => Extend (Traced m)
  1. Law: extend f <<< extend g = extend (f <<< extend g)
  2. Proof:
  3. Rewrite pointfully:
  4. (extend f <<< extend g) x = extend (f <<< extend g) x
  5. LHS := extend f (extend g x) =
  6. extend f (\ t -> g \ t' -> x (t <> t')) =
  7. \ s -> f (\ s' -> (\ t -> g \ t' -> x (t <> t')) (s <> s')) =
  8. \ s -> f (\ s' -> g \ t' -> x (s <> s' <> t'))
  9. RHS := \ s -> (f <<< extend g) (\ s' -> x (s <> s')) =
  10. \ s -> (\ y -> f (extend g y)) (\ s' -> x (s <> s')) =
  11. \ s -> (\ y -> f (\ t -> g (\ t' -> y (t <> t')))) (\ s' -> x (s <> s')) =
  12. \ s -> f (\ t -> g (\ t' -> (\ s' -> x (s <> s')) (t <> t'))) =
  13. \ s -> f (\ t -> g (\ t' -> x (s <> t <> t'))) = (via renaming)
  14. \ s -> f (\ s' -> g \ t' -> x (s <> s' <> t'))
• (Monoid m) => Comonad (Traced m)
  1. Law: extract <<= xs = xs
  2. Proof:
  3. RHS := \ x -> s
  4. LHS := extend extract (\ x -> s) =
  5. \ t -> extract (\ t' -> (\ x -> s) (t <> t')) =
  6. \ t -> (\ x -> s) (t <> mempty) =
  7. \ t -> (\ x -> s) t =
  8. \ x -> s

runTraced :: forall a m. Traced m a -> m -> a

traced :: forall a m. (m -> a) -> Traced m a

track :: forall m a. Monoid m => m -> Traced m a -> a

1. Law: track mempty = extract
2. Proof:
3. First, rewrite as: track mempty f = extract f
4. RHS := f mempty
5. LHS := f mempty
6. Law: (track s =<= track t) x = track (s <> t) x
7. Proof:
8. RHS := track (s <> t) x = x (s <> t)
9. LHS := composeCoKliesliFlipped (track s) (track t) x =
10. track s (track t <<= x) =
11. track s (extend (track t) x) =
12. track s (\ t' -> (track t) \ t'' -> x (t' <> t'')) =
13. track s (\ t' -> x (t' <> t)) =
14. x (s <> t)

tracks :: forall m a. Monoid m => (a -> m) -> Traced m a -> a

listen :: forall m a. Traced m a -> Traced m (Tuple a m)

listens :: forall m b a. (m -> b) -> Traced m a -> Traced m (Tuple a b)

censor :: forall m a. (m -> m) -> Traced m a -> Traced m a