Data.Functor.Adjunction

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

unit, counit | leftAdjunct, rightAdjunct

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 Par1 Par1

Methods

unit :: a -> Par1 (Par1 a)

counit :: Par1 (Par1 a) -> a

leftAdjunct :: (Par1 a -> b) -> a -> Par1 b

rightAdjunct :: (a -> Par1 b) -> Par1 a -> b

Adjunction Identity Identity

Methods

unit :: a -> Identity (Identity a)

counit :: Identity (Identity a) -> a

leftAdjunct :: (Identity a -> b) -> a -> Identity b

rightAdjunct :: (a -> Identity b) -> Identity a -> b

Adjunction (V1 *) (U1 *)

Methods

unit :: a -> U1 * (V1 * a)

counit :: V1 * (U1 * a) -> a

leftAdjunct :: (V1 * a -> b) -> a -> U1 * b

rightAdjunct :: (a -> U1 * b) -> V1 * a -> b

Adjunction f u => Adjunction (Free f) (Cofree u)

Methods

unit :: a -> Cofree u (Free f a)

counit :: Free f (Cofree u a) -> a

leftAdjunct :: (Free f a -> b) -> a -> Cofree u b

rightAdjunct :: (a -> Cofree u b) -> Free f a -> b

Adjunction ((,) e) ((->) LiftedRep LiftedRep e)

Methods

unit :: a -> (LiftedRep -> LiftedRep) e (e, a)

counit :: (e, (LiftedRep -> LiftedRep) e a) -> a

leftAdjunct :: ((e, a) -> b) -> a -> (LiftedRep -> LiftedRep) e b

rightAdjunct :: (a -> (LiftedRep -> LiftedRep) e b) -> (e, a) -> b

Adjunction f g => Adjunction (Rec1 * f) (Rec1 * g)

Methods

unit :: a -> Rec1 * g (Rec1 * f a)

counit :: Rec1 * f (Rec1 * g a) -> a

leftAdjunct :: (Rec1 * f a -> b) -> a -> Rec1 * g b

rightAdjunct :: (a -> Rec1 * g b) -> Rec1 * f a -> b

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

Methods

unit :: a -> IdentityT * g (IdentityT * f a)

counit :: IdentityT * f (IdentityT * g a) -> a

leftAdjunct :: (IdentityT * f a -> b) -> a -> IdentityT * g b

rightAdjunct :: (a -> IdentityT * g b) -> IdentityT * f a -> b

Adjunction m w => Adjunction (WriterT s m) (TracedT s w)

Methods

unit :: a -> TracedT s w (WriterT s m a)

counit :: WriterT s m (TracedT s w a) -> a

leftAdjunct :: (WriterT s m a -> b) -> a -> TracedT s w b

rightAdjunct :: (a -> TracedT s w b) -> WriterT s m a -> b

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

Methods

unit :: a -> ReaderT * e m (EnvT e w a)

counit :: EnvT e w (ReaderT * e m a) -> a

leftAdjunct :: (EnvT e w a -> b) -> a -> ReaderT * e m b

rightAdjunct :: (a -> ReaderT * e m b) -> EnvT e w a -> b

(Adjunction f g, Adjunction f' g') => Adjunction ((:+:) * f f') ((:*:) * g g')

Methods

unit :: a -> (* :*: g) g' ((* :+: f) f' a)

counit :: (* :+: f) f' ((* :*: g) g' a) -> a

leftAdjunct :: ((* :+: f) f' a -> b) -> a -> (* :*: g) g' b

rightAdjunct :: (a -> (* :*: g) g' b) -> (* :+: f) f' a -> b

(Adjunction f g, Adjunction f' g') => Adjunction (Sum * f f') (Product * g g')

Methods

unit :: a -> Product * g g' (Sum * f f' a)

counit :: Sum * f f' (Product * g g' a) -> a

leftAdjunct :: (Sum * f f' a -> b) -> a -> Product * g g' b

rightAdjunct :: (a -> Product * g g' b) -> Sum * f f' a -> b

(Adjunction f g, Adjunction f' g') => Adjunction ((:.:) * * f' f) ((:.:) * * g g')

Methods

unit :: a -> (* :.: *) g g' ((* :.: *) f' f a)

counit :: (* :.: *) f' f ((* :.: *) g g' a) -> a

leftAdjunct :: ((* :.: *) f' f a -> b) -> a -> (* :.: *) g g' b

rightAdjunct :: (a -> (* :.: *) g g' b) -> (* :.: *) f' f a -> b

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

Methods

unit :: a -> Compose * * g g' (Compose * * f' f a)

counit :: Compose * * f' f (Compose * * g g' a) -> a

leftAdjunct :: (Compose * * f' f a -> b) -> a -> Compose * * g g' b

rightAdjunct :: (a -> Compose * * g g' b) -> Compose * * f' 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))

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

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

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

Every functor in Haskell permits unzipping

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

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

absurdL :: Void -> f Void

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 ())

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