| Portability | rank 2 types, MPTCs, fundeps |
|---|---|
| Stability | experimental |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
Data.Functor.Adjunction
Description
- 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
Instances
| 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
Constructors
| Representation | |
repAdjunction :: Adjunction f g => Representation g (f ())Source