Safe Haskell | Safe-Inferred |
---|

# Contravariant Applicative

class Contravariant f => Divisible f whereSource

A `Divisible`

contravariant functor is the contravariant analogue of `Applicative`

.

In denser jargon, a `Divisible`

contravariant functor is a monoid object in the category
of presheaves from Hask to Hask, equipped with Day convolution mapping the Cartesian
product of the source to the Cartesian product of the target.

By way of contrast, an `Applicative`

functor can be viewed as a monoid object in the
category of copresheaves from Hask to Hask, equipped with Day convolution mapping the
Cartesian product of the source to the Cartesian product of the target.

Given the canonical diagonal morphism:

delta a = (a,a)

should be associative with `divide`

`delta`

`conquer`

as a unit

`divide`

`delta`

m`conquer`

= m`divide`

`delta`

`conquer`

m = m`divide`

`delta`

(`divide`

`delta`

m n) o =`divide`

`delta`

m (`divide`

`delta`

n o)

With more general arguments you'll need to reassociate and project using the monoidal structure of the source category. (Here fst and snd are used in lieu of the more restricted lambda and rho, but this construction works with just a monoidal category.)

`divide`

f m`conquer`

=`contramap`

(`fst`

. f) m`divide`

f`conquer`

m =`contramap`

(`snd`

. f) m`divide`

f (`divide`

g m n) o =`divide`

f' m (`divide`

`id`

n o) where f' a = case f a of (bc,d) -> case g bc of (b,c) -> (a,(b,c))

Divisible Equivalence | |

Divisible Comparison | |

Divisible Predicate | |

Monoid r => Divisible (Op r) | |

(Divisible f, Applicative g) => Divisible (ComposeCF f g) | |

(Applicative f, Divisible g) => Divisible (ComposeFC f g) |

# Contravariant Alternative

class Divisible f => Decidable f whereSource

A `Divisible`

contravariant functor is a monoid object in the category of presheaves
from Hask to Hask, equipped with Day convolution mapping the cartesian product of the
source to the Cartesian product of the target.

`choose`

Left m (`lose`

f) = m`choose`

Right (`lose`

f) m = m`choose`

f (`choose`

g m n) o =`divide`

f' m (`divide`

`id`

n o) where f' bcd =`either`

(`either`

`id`

(`Right`

.`Left`

) . g) (`Right`

.`Right`

) . f

In addition, we expect the same kind of distributive law as is satisfied by the usual
covariant `Alternative`

, w.r.t `Applicative`

, which should be fully formulated and
added here at some point!