{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}

-- | Discrete category <-> 'Env' comonad
module Control.Comonad.Travel.Env where

import Control.Comonad.Env
import Control.Comonad.Travel
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Sigma (Sigma (..))
import Data.Type.Equality
import Prelude hiding (id, (.))

-- | @(':~:')@ is a discrete category on kind @k@.
type Discrete :: forall k. k -> k -> Type
type Discrete = (:~:)

-- | @Travel (Discrete @k) r ~ (k, r) ~ Env k r@
fromEnv :: (SingKind k) => Env (Demote k) r -> Travel (Discrete @k) r
fromEnv :: forall k r. SingKind k => Env (Demote k) r -> Travel Discrete r
fromEnv (Env (Demote k) r -> (Demote k, r)
forall e a. Env e a -> (e, a)
runEnv -> (Demote k
x, r
r)) = case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
x of
  SomeSing Sing a
sx -> Sing a -> (Sigma k (TyCon (Discrete a)) -> r) -> Travel Discrete r
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel Sing a
sx \(Sing fst
_ :&: a :~: fst
TyCon (Discrete a) @@ fst
Refl) -> r
r

toEnv :: (SingKind k) => Travel (Discrete @k) r -> Env (Demote k) r
toEnv :: forall k r. SingKind k => Travel Discrete r -> Env (Demote k) r
toEnv (MkTravel Sing a
sx Sigma k (TyCon (Discrete a)) -> r
k) = Demote k -> r -> EnvT (Demote k) Identity r
forall e a. e -> a -> Env e a
env (Sing a -> Demote k
forall (a :: k). Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sx) (Sigma k (TyCon (Discrete a)) -> r
k (Sing a
sx Sing a -> (TyCon (Discrete a) @@ a) -> Sigma k (TyCon (Discrete a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: a :~: a
TyCon (Discrete a) @@ a
forall {k} (a :: k). a :~: a
Refl))