{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}

-- | Monoid <-> One-object category <-> 'Traced' comonad
module Control.Comonad.Travel.Traced where

import Control.Category.OneObject
import Control.Comonad.Traced
import Control.Comonad.Travel
import Data.Singletons.Sigma (Sigma (..))
import Data.Unit.Singletons

-- | @Travel (OneObject m) r ~ (m -> r) ~ Traced m r@
fromTraced :: Traced m r -> Travel (OneObject m) r
fromTraced :: forall m r. Traced m r -> Travel (OneObject m) r
fromTraced Traced m r
w = Sing '()
-> (Sigma () (TyCon (OneObject m '())) -> r)
-> Travel (OneObject m) r
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel Sing '()
SUnit '()
SU \(Sing fst
SUnit fst
SU :&: OneObject m
m) -> Traced m r -> m -> r
forall m a. Traced m a -> m -> a
runTraced Traced m r
w m
m

toTraced :: Travel (OneObject m) r -> Traced m r
toTraced :: forall m r. Travel (OneObject m) r -> Traced m r
toTraced (MkTravel Sing a
_ Sigma () (TyCon (OneObject m a)) -> r
f) = (m -> r) -> Traced m r
forall m a. (m -> a) -> Traced m a
traced (\m
m -> Sigma () (TyCon (OneObject m a)) -> r
f (Sing '()
SUnit '()
SU Sing '()
-> (TyCon (OneObject m a) @@ '())
-> Sigma () (TyCon (OneObject m a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: m -> OneObject m a '()
forall m (a :: ()) (b :: ()). m -> OneObject m a b
OneObject m
m))