contravariant-0.5.1: Contravariant functors

Portabilityportable
Stabilityprovisional
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellTrustworthy

Data.Functor.Contravariant.Day

Description

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

http://ncatlab.org/nlab/show/Day+convolution

Synopsis

Documentation

data Day f g a Source

The Day convolution of two contravariant functors.

Constructors

forall b c . Day (f b) (g c) (a -> (b, c)) 

Instances

day :: f a -> g b -> Day f g (a, b)Source

Construct the Day convolution 

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

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

Break apart the Day convolution of two contravariant functors.

assoc :: Day f (Day g h) a -> Day (Day f g) h aSource

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

disassoc :: Day (Day f g) h a -> Day f (Day g h) aSource

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

swapped :: Day f g a -> Day g f aSource

The monoid for Day convolution in Haskell is symmetric. 

 contramap f . swapped = swapped . contramap f

intro1 :: f a -> Day Proxy f aSource

Proxy serves as the unit of Day convolution. 

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

intro2 :: f a -> Day f Proxy aSource

Proxy serves as the unit of Day convolution. 

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

day1 :: Contravariant f => Day f g a -> f aSource

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

day2 :: Contravariant g => Day f g a -> g aSource

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

diag :: f a -> Day f f aSource

Diagonalize the Day convolution: 

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

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

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

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

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