Data.Functor.Adjunction

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

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)

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.

This definition admits a default definition for the index method of 'Index", one of the superclasses of Representable.

A right adjoint functor admits an intrinsic notion of zipping

Every functor in Haskell permits unzipping

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

And a left adjoint must be inhabited by exactly one element

Every functor in Haskell permits uncozipping