adjunctions- Adjunctions

Portabilityrank 2 types, MPTCs, fundeps
MaintainerEdward Kmett <>
Safe HaskellNone






class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f whereSource

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 


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

counit :: f (u a) -> aSource

leftAdjunct :: (f a -> b) -> a -> u bSource

rightAdjunct :: (a -> u b) -> f a -> bSource


tabulateAdjunction :: Adjunction f u => (f () -> b) -> u bSource

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

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

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

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

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 aSource