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	Haskell2010

Data.Functor.Adjunction

Description

Synopsis

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 Source #

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

unit , counit | leftAdjunct , rightAdjunct

Methods

unit :: a -> u (f a) Source #

counit :: f (u a) -> a Source #

leftAdjunct :: (f a -> b) -> a -> u b Source #

rightAdjunct :: (a -> u b) -> f a -> b Source #

Instances

Instances details

Adjunction Par1 Par1 Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Par1 ( Par1 a) Source # counit :: Par1 ( Par1 a) -> a Source # leftAdjunct :: ( Par1 a -> b) -> a -> Par1 b Source # rightAdjunct :: (a -> Par1 b) -> Par1 a -> b Source #
Adjunction Identity Identity Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Identity ( Identity a) Source # counit :: Identity ( Identity a) -> a Source # leftAdjunct :: ( Identity a -> b) -> a -> Identity b Source # rightAdjunct :: (a -> Identity b) -> Identity a -> b Source #
Adjunction ( V1 :: Type -> Type ) ( U1 :: Type -> Type ) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> U1 ( V1 a) Source # counit :: V1 ( U1 a) -> a Source # leftAdjunct :: ( V1 a -> b) -> a -> U1 b Source # rightAdjunct :: (a -> U1 b) -> V1 a -> b Source #
Adjunction f u => Adjunction ( Free f) ( Cofree u) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Cofree u ( Free f a) Source # counit :: Free f ( Cofree u a) -> a Source # leftAdjunct :: ( Free f a -> b) -> a -> Cofree u b Source # rightAdjunct :: (a -> Cofree u b) -> Free f a -> b Source #
Adjunction ( (,) e) ((->) e :: Type -> Type ) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> e -> (e, a) Source # counit :: (e, e -> a) -> a Source # leftAdjunct :: ((e, a) -> b) -> a -> e -> b Source # rightAdjunct :: (a -> e -> b) -> (e, a) -> b Source #
Adjunction f g => Adjunction ( Rec1 f) ( Rec1 g) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Rec1 g ( Rec1 f a) Source # counit :: Rec1 f ( Rec1 g a) -> a Source # leftAdjunct :: ( Rec1 f a -> b) -> a -> Rec1 g b Source # rightAdjunct :: (a -> Rec1 g b) -> Rec1 f a -> b Source #
Adjunction w m => Adjunction ( EnvT e w) ( ReaderT e m) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> ReaderT e m ( EnvT e w a) Source # counit :: EnvT e w ( ReaderT e m a) -> a Source # leftAdjunct :: ( EnvT e w a -> b) -> a -> ReaderT e m b Source # rightAdjunct :: (a -> ReaderT e m b) -> EnvT e w a -> b Source #
Adjunction f g => Adjunction ( IdentityT f) ( IdentityT g) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> IdentityT g ( IdentityT f a) Source # counit :: IdentityT f ( IdentityT g a) -> a Source # leftAdjunct :: ( IdentityT f a -> b) -> a -> IdentityT g b Source # rightAdjunct :: (a -> IdentityT g b) -> IdentityT f a -> b Source #
Adjunction m w => Adjunction ( WriterT s m) ( TracedT s w) Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> TracedT s w ( WriterT s m a) Source # counit :: WriterT s m ( TracedT s w a) -> a Source # leftAdjunct :: ( WriterT s m a -> b) -> a -> TracedT s w b Source # rightAdjunct :: (a -> TracedT s w b) -> WriterT s m a -> b Source #
( Adjunction f g, Adjunction f' g') => Adjunction (f :+: f') (g :*: g') Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> (g :: g') ((f :+: f') a) Source # counit :: (f :+: f') ((g :: g') a) -> a Source # leftAdjunct :: ((f :+: f') a -> b) -> a -> (g :: g') b Source # rightAdjunct :: (a -> (g :: g') b) -> (f :+: f') a -> b Source #
( Adjunction f g, Adjunction f' g') => Adjunction ( Sum f f') ( Product g g') Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Product g g' ( Sum f f' a) Source # counit :: Sum f f' ( Product g g' a) -> a Source # leftAdjunct :: ( Sum f f' a -> b) -> a -> Product g g' b Source # rightAdjunct :: (a -> Product g g' b) -> Sum f f' a -> b Source #
( Adjunction f g, Adjunction f' g') => Adjunction (f' :.: f) (g :.: g') Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> (g :.: g') ((f' :.: f) a) Source # counit :: (f' :.: f) ((g :.: g') a) -> a Source # leftAdjunct :: ((f' :.: f) a -> b) -> a -> (g :.: g') b Source # rightAdjunct :: (a -> (g :.: g') b) -> (f' :.: f) a -> b Source #
( Adjunction f g, Adjunction f' g') => Adjunction ( Compose f' f) ( Compose g g') Source #
Instance details Defined in Data.Functor.Adjunction Methods unit :: a -> Compose g g' ( Compose f' f a) Source # counit :: Compose f' f ( Compose g g' a) -> a Source # leftAdjunct :: ( Compose f' f a -> b) -> a -> Compose g g' b Source # rightAdjunct :: (a -> Compose g g' b) -> Compose f' f a -> b Source #

adjuncted :: ( Adjunction f u, Profunctor p, Functor g) => p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d)) Source #

leftAdjunct and rightAdjunct form two halves of an isomorphism.

This can be used with the combinators from the lens package.

adjuncted :: Adjunction f u => Iso' (f a -> b) (a -> u b)

tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b Source #

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 Source #

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 Source #

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

A right adjoint functor admits an intrinsic notion of zipping

unzipR :: Functor u => u (a, b) -> (u a, u b) Source #

Every functor in Haskell permits unzipping

unabsurdL :: Adjunction f u => f Void -> Void Source #

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

absurdL :: Void -> f Void Source #

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

uncozipL :: Functor f => Either (f a) (f b) -> f ( Either a b) Source #

Every functor in Haskell permits uncozipping

extractL :: Adjunction f u => f a -> a Source #

duplicateL :: Adjunction f u => f a -> f (f a) Source #

splitL :: Adjunction f u => f a -> (a, f ()) Source #

unsplitL :: Functor f => a -> f () -> f a Source #