Modulekan-extensions-5.2.7Haskell2010

Data.Functor.Contravariant.Day

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

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

The Day convolution of two contravariant functors.

Instances5Contravariant, Divisible, Representable, Adjunction, Rep

Contravariant (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Day
(Divisible f, Divisible g) => Divisible (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Day
(Representable f, Representable g) => Representable (Day f g)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Day
(Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u')Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Day
type Rep (Day f g) = (Rep f, Rep g)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Day

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

Construct the Day convolution

day1 (day f g) = f
day2 (day f g) = g

valuerunDay :: (Contravariant f, Contravariant g) => Day f g a -> (f a, g a)

Break apart the Day convolution of two contravariant functors.

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
contramap f . assoc = assoc . contramap 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
contramap f . disassoc = disassoc . contramap f

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

The monoid for Day convolution in Haskell is symmetric.

contramap f . swapped = swapped . contramap f

valueintro1 :: f a -> Day Proxy f a

Proxy serves as the unit of Day convolution.

day1 . intro1 = id
contramap f . intro1 = intro1 . contramap f

valueintro2 :: f a -> Day f Proxy a

Proxy serves as the unit of Day convolution.

day2 . intro2 = id
contramap f . intro2 = intro2 . contramap f

valueday1 :: Contravariant f => Day f g a -> f a

In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit.

day1 . intro1 = id
day1 = fst . runDay
contramap f . day1 = day1 . contramap f

valueday2 :: Contravariant g => Day f g a -> g a

In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit. day2 . intro2 = id day2 = snd . runDay contramap f . day2 = day2 . contramap f

valuediag :: f a -> Day f f a

Diagonalize the Day convolution:

day1 . diag = id
day2 . diag = id
runDay . diag = a -> (a,a)
contramap f . diag = diag . contramap f

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:

contramap f . trans1 fg = trans1 fg . contramap 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:

contramap f . trans2 fg = trans2 fg . contramap f