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