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

Stability | experimental |

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

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

- distributeAdjunct :: (Adjunction f g, Functor w) => w (g a) -> g (w a)
- data Representation f x = Representation {}
- repAdjunction :: Adjunction f g => Representation g (f ())

# Documentation

class (Functor f, Distributive g) => Adjunction f g | f -> g, g -> f whereSource

An adjunction between Hask and Hask.

rightAdjunct unit = id leftAdjunct counit = id

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

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

Adjunction Identity Identity | |

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

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

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

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

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

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

distributeAdjunct :: (Adjunction f g, Functor w) => w (g a) -> g (w a)Source

Every right adjoint is representable by its left adjoint applied to unit Consequently, we use the isomorphism from ((->) f ()) ~ g to distribute the right adjoint over any other functor.

data Representation f x Source

repAdjunction :: Adjunction f g => Representation g (f ())Source