Safe Haskell	None
Language	GHC2021

Control.Comonad.Travel

Contents

Travel: Comonad from a Category

Description

Implementation of "Directed Containers as Categories," D. Ahman and T. Uustalu, EPTCS 207, 2016, pp. 89-98

https://arxiv.org/abs/1604.01187

Synopsis

data Travel (cat :: k -> k -> Type) r where
- MkTravel :: forall k (cat :: k -> k -> Type) r (a :: k). Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
data TravelTag (cat :: k -> k -> Type) x where
- TravelFrom :: forall k (cat :: k -> k -> Type) (a :: k). Sing a -> TravelTag cat (Sigma k (TyCon (cat a)))
truncateTravel :: forall k (cat :: k -> k -> Type) r. SingKind k => Store (Demote k) r -> Travel cat r

Travel: Comonad from a Category

data Travel (cat :: k -> k -> Type) r where Source #

Make Polynomial Comonad from Category.

Travel cat is a polynomial functor for any type constructor cat.

Travel cat r ~ ∑a. ((∑b. cat a b) -> r)

Travel cat is a Comonad if cat is a Category.

Constructors

MkTravel :: forall k (cat :: k -> k -> Type) r (a :: k). Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r

Instances

Instances details

Functor (Travel cat) Source #

Instance details

Defined in Control.Comonad.Travel

Methods

fmap :: (a -> b) -> Travel cat a -> Travel cat b #

(<$) :: a -> Travel cat b -> Travel cat a #

Category cat => Comonad (Travel cat) Source #

Instance details

Defined in Control.Comonad.Travel

Methods

extract :: Travel cat a -> a #

duplicate :: Travel cat a -> Travel cat (Travel cat a) #

extend :: (Travel cat a -> b) -> Travel cat a -> Travel cat b #

Polynomial (Travel cat) Source #

Instance details

Defined in Control.Comonad.Travel

Associated Types

type Tag (Travel cat)
Instance details Defined in Control.Comonad.Travel type Tag (Travel cat) = TravelTag cat

Methods

toPoly :: Travel cat x -> Poly (Tag (Travel cat)) x

fromPoly :: Poly (Tag (Travel cat)) x -> Travel cat x

type Tag (Travel cat) Source #

Instance details

Defined in Control.Comonad.Travel

type Tag (Travel cat) = TravelTag cat

data TravelTag (cat :: k -> k -> Type) x where Source #

Constructors

TravelFrom :: forall k (cat :: k -> k -> Type) (a :: k). Sing a -> TravelTag cat (Sigma k (TyCon (cat a)))

Instances

Instances details

SDecide k => TestEquality (TravelTag cat :: Type -> Type) Source #
Instance details Defined in Control.Comonad.Travel Methods testEquality :: TravelTag cat a -> TravelTag cat b -> Maybe (a :~: b) #
SDecide k => GEq (TravelTag cat :: Type -> Type) Source #
Instance details Defined in Control.Comonad.Travel Methods geq :: TravelTag cat a -> TravelTag cat b -> Maybe (a :~: b) #

truncateTravel :: forall k (cat :: k -> k -> Type) r. SingKind k => Store (Demote k) r -> Travel cat r Source #

Constructs Travel cat from Store (Demote k), which can be thought of as a Travel cat but its arrows are forgotten.