Modulekan-extensions-5.2.7Haskell2010

Data.Functor.Day

Eitan Chatav first introduced me to this construction

The Day convolution of two covariant functors is a covariant functor.

Day convolution is usually defined in terms of contravariant functors, however, it just needs a monoidal category, and Hask^op is also monoidal.

Day convolution can be used to nicely describe monoidal functors as monoid objects w.r.t this product.

datadata Day (f :: Type -> Type) (g :: Type -> Type) a

The Day convolution of two covariant functors.

Instances9ComonadTrans, Functor, Applicative, Distributive, Comonad, ComonadApply, …

Comonad f => ComonadTrans (Day f)Defined in kan-extensions-5.2.7 · Data.Functor.Day
Functor (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(Applicative f, Applicative g) => Applicative (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(Representable f, Representable g) => Distributive (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(Comonad f, Comonad g) => Comonad (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(ComonadApply f, ComonadApply g) => ComonadApply (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(Representable f, Representable g) => Representable (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Day
(Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u')Defined in kan-extensions-5.2.7 · Data.Functor.Day
type Rep (Day f g) = (Rep f, Rep g)Defined in kan-extensions-5.2.7 · Data.Functor.Day

valueday :: f (a -> b) -> g a -> Day f g b

Construct the Day convolution

valuedap :: Applicative f => Day f f a -> f a

Collapse via a monoidal functor.

dap (day f g) = f <*> g

valueassoc :: Day f (Day g h) a -> Day (Day f g) h a

Day convolution provides a monoidal product. The associativity of this monoid is witnessed by assoc and disassoc.

assoc . disassoc = id
disassoc . assoc = id
fmap f . assoc = assoc . fmap f

valuedisassoc :: Day (Day f g) h a -> Day f (Day g h) a

Day convolution provides a monoidal product. The associativity of this monoid is witnessed by assoc and disassoc.

assoc . disassoc = id
disassoc . assoc = id
fmap f . disassoc = disassoc . fmap f

valueswapped :: Day f g a -> Day g f a

The monoid for Day convolution on the cartesian monoidal structure is symmetric.

fmap f . swapped = swapped . fmap f

valueintro1 :: f a -> Day Identity f a

Identity is the unit of Day convolution

intro1 . elim1 = id
elim1 . intro1 = id

valueintro2 :: f a -> Day f Identity a

Identity is the unit of Day convolution

intro2 . elim2 = id
elim2 . intro2 = id

valueelim1 :: Functor f => Day Identity f a -> f a

Identity is the unit of Day convolution

intro1 . elim1 = id
elim1 . intro1 = id

valueelim2 :: Functor f => Day f Identity a -> f a

Identity is the unit of Day convolution

intro2 . elim2 = id
elim2 . intro2 = id

valuetrans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a

Apply a natural transformation to the left-hand side of a Day convolution.

This respects the naturality of the natural transformation you supplied:

fmap f . trans1 fg = trans1 fg . fmap f

valuetrans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a

Apply a natural transformation to the right-hand side of a Day convolution.

This respects the naturality of the natural transformation you supplied:

fmap f . trans2 fg = trans2 fg . fmap f

valuecayley

valuedayley

Proposition 4.1 from Pastro and Street