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

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

counit :: f (u a) -> a Source #

leftAdjunct :: (f a -> b) -> a -> u b Source #

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

Adjunction Par1 Par1 Source # | |

Adjunction Identity Identity Source # | |

Adjunction (V1 *) (U1 *) Source # | |

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

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

Adjunction f g => Adjunction (Rec1 * f) (Rec1 * g) Source # | |

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

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

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

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

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

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

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

adjuncted :: (Adjunction f u, Profunctor p, Functor g) => p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d)) Source #

`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 Source #

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

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

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 -> Void Source #

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 -> a Source #

duplicateL :: Adjunction f u => f a -> f (f a) Source #

splitL :: Adjunction f u => f a -> (a, f ()) Source #