Portability | rank 2 types, MPTCs, fundeps |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Safe Haskell | None |

- 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

- tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
- indexAdjunction :: Adjunction f u => u b -> f a -> b
- 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 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

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

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

Adjunction Identity Identity | |

(Functor ((,) e), Representable ((->) e)) => Adjunction ((,) e) ((->) e) | |

(Functor (IdentityT f), Representable (IdentityT g), Adjunction f g) => Adjunction (IdentityT f) (IdentityT g) | |

(Functor (EnvT e w), Representable (ReaderT e m), Adjunction w m) => Adjunction (EnvT e w) (ReaderT e m) | |

(Functor (WriterT s m), Representable (TracedT s w), Adjunction m w) => Adjunction (WriterT s m) (TracedT s w) | |

(Functor (Compose f' f), Representable (Compose g g'), Adjunction f g, Adjunction f' g') => Adjunction (Compose f' f) (Compose g g') |

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

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