Portability | rank 2 types, MPTCs, fundeps |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

- class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where
- unit :: a -> u (f a)
- counit :: f (u a) -> a
- leftAdjunct :: (f a -> b) -> a -> u b
- rightAdjunct :: (a -> u b) -> f a -> b

- tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
- indexAdjunction :: Adjunction f u => u b -> f a -> b
- zipR :: Adjunction f u => (u a, u b) -> u (a, b)
- unzipF :: Functor u => u (a, b) -> (u a, u b)
- inhabitedL :: Adjunction f u => f Void -> Void
- cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
- uncozipF :: Functor f => Either (f a) (f b) -> f (Either a b)

# Documentation

class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f whereSource

An adjunction between Hask and Hask.

Minimal definition: both `unit`

and `counit`

or both `leftAdjunct`

and `rightAdjunct`

,
subject to the constraints imposed by the default definitions that the following laws
should hold.

unit = leftAdjunct id counit = rightAdjunct id leftAdjunct f = fmap f . unit rightAdjunct f = counit . fmap f

Any implementation is required to ensure that `leftAdjunct`

and `rightAdjunct`

witness
an isomorphism from `Nat (f a, b)`

to `Nat (a, g b)`

rightAdjunct unit = id leftAdjunct counit = id

leftAdjunct :: (f a -> b) -> a -> u bSource

rightAdjunct :: (a -> u b) -> f a -> bSource

Adjunction Identity Identity | |

Adjunction ((,) e) ((->) e) | |

Adjunction f g => Adjunction (IdentityT f) (IdentityT g) | |

Adjunction w m => Adjunction (EnvT e w) (ReaderT e m) | |

Adjunction m w => Adjunction (WriterT s m) (TracedT s w) | |

(Adjunction f g, Adjunction f' g') => Adjunction (Compose f' f) (Compose g g') |

tabulateAdjunction :: Adjunction f u => (f () -> b) -> u bSource

Every right adjoint is representable by its left adjoint applied to a unit element

Use this definition and the primitives in Data.Functor.Representable to meet the requirements of the superclasses of Representable.

indexAdjunction :: Adjunction f u => u b -> f a -> bSource

zipR :: Adjunction f u => (u a, u b) -> u (a, b)Source

A right adjoint functor admits an intrinsic notion of zipping

inhabitedL :: Adjunction f u => f Void -> VoidSource

A left adjoint must be inhabited, or we can derive bottom

cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)Source

And a left adjoint must be inhabited by exactly one element