kan-extensions-5.0.1: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

Data.Functor.Day

Description

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.

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

Synopsis

# Documentation

data Day f g a Source

The Day convolution of two covariant functors.

`Day f g a -> h a` is isomorphic to `f a -> Rift g h a`

Constructors

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

Instances

 Functor (Day f g) Source (Applicative f, Applicative g) => Applicative (Day f g) Source (Representable f, Representable g) => Distributive (Day f g) Source (Representable f, Representable g) => Representable (Day f g) Source type Rep (Day f g) = (Rep f, Rep g) Source

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

Construct the Day convolution

dap :: Applicative f => Day f f a -> f a Source

Collapse via a monoidal functor.

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

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

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
```

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

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
```

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

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

````fmap` f `.` `swapped` = `swapped` `.` `fmap` f
```

intro1 :: f a -> Day Identity f a Source

`Identity` is the unit of `Day` convolution

````intro1` `.` `elim1` = `id`
`elim1` `.` `intro1` = `id`
```

intro2 :: f a -> Day f Identity a Source

`Identity` is the unit of `Day` convolution

````intro2` `.` `elim2` = `id`
`elim2` `.` `intro2` = `id`
```

elim1 :: Functor f => Day Identity f a -> f a Source

`Identity` is the unit of `Day` convolution

````intro1` `.` `elim1` = `id`
`elim1` `.` `intro1` = `id`
```

elim2 :: Functor f => Day f Identity a -> f a Source

`Identity` is the unit of `Day` convolution

````intro2` `.` `elim2` = `id`
`elim2` `.` `intro2` = `id`
```

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

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
```

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

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
```