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

- class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where
- 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 #

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

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

Adjunction Identity Identity # | |

Adjunction ((,) e) ((->) e) # | |

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

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

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

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

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

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

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

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

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

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