| Copyright | 2008-2013 Edward Kmett |
|---|---|
| License | BSD |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | experimental |
| Portability | rank 2 types, MPTCs, fundeps |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Data.Functor.Adjunction
Description
- 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
- adjuncted :: (Adjunction f u, Profunctor p, Functor g) => p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
- tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
- indexAdjunction :: Adjunction f u => u b -> f a -> b
- zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c
- zipR :: Adjunction f u => (u a, u b) -> u (a, b)
- unzipR :: Functor u => u (a, b) -> (u a, u b)
- unabsurdL :: Adjunction f u => f Void -> Void
- absurdL :: Void -> f Void
- cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
- uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
- extractL :: Adjunction f u => f a -> a
- duplicateL :: Adjunction f u => f a -> f (f a)
- splitL :: Adjunction f u => f a -> (a, f ())
- unsplitL :: Functor f => a -> f () -> f a
Documentation
class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where
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
Minimal complete definition
Nothing
Methods
unit :: a -> u (f a)
counit :: f (u a) -> a
leftAdjunct :: (f a -> b) -> a -> u b
rightAdjunct :: (a -> u b) -> f a -> b
Instances
| Adjunction Identity Identity | |
| Adjunction ((,) e) ((->) e) | |
| Adjunction f g => Adjunction (IdentityT f) (IdentityT g) | |
| Adjunction f u => Adjunction (Free f) (Cofree u) | |
| 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') | |
| (Adjunction f g, Adjunction f' g') => Adjunction (Sum f f') (Product g g') |
adjuncted :: (Adjunction f u, Profunctor p, Functor g) => p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
leftAdjunct and rightAdjunct form two halves of an isomorphism.
This can be used with the combinators from the lens package.
adjuncted::Adjunctionf u =>Iso'(f a -> b) (a -> u b)
tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
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 -> b
This definition admits a default definition for the
index method of 'Index", one of the superclasses of
Representable.
zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c
zipR :: Adjunction f u => (u a, u b) -> u (a, b)
A right adjoint functor admits an intrinsic notion of zipping
unabsurdL :: Adjunction f u => f Void -> Void
A left adjoint must be inhabited, or we can derive bottom.
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
And a left adjoint must be inhabited by exactly one element
uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
Every functor in Haskell permits uncozipping
extractL :: Adjunction f u => f a -> a
duplicateL :: Adjunction f u => f a -> f (f a)
splitL :: Adjunction f u => f a -> (a, f ())