Copyright | (C) 2014-2015 Edward Kmett |
---|---|

License | BSD-style (see the file LICENSE) |

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

Stability | experimental |

Portability | GADTs, TFs, MPTCs, RankN |

Safe Haskell | Safe |

Language | Haskell2010 |

## Synopsis

- data Procompose p q d c where
- Procompose :: p x c -> q d x -> Procompose p q d c

- procomposed :: Category p => Procompose p p a b -> p a b
- idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
- idr :: Profunctor q => Iso (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
- assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b) (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b)
- eta :: (Profunctor p, Category p) => (->) :-> p
- mu :: Category p => Procompose p p :-> p
- stars :: Functor g => Iso (Procompose (Star f) (Star g) d c) (Procompose (Star f') (Star g') d' c') (Star (Compose g f) d c) (Star (Compose g' f') d' c')
- kleislis :: Monad g => Iso (Procompose (Kleisli f) (Kleisli g) d c) (Procompose (Kleisli f') (Kleisli g') d' c') (Kleisli (Compose g f) d c) (Kleisli (Compose g' f') d' c')
- costars :: Functor f => Iso (Procompose (Costar f) (Costar g) d c) (Procompose (Costar f') (Costar g') d' c') (Costar (Compose f g) d c) (Costar (Compose f' g') d' c')
- cokleislis :: Functor f => Iso (Procompose (Cokleisli f) (Cokleisli g) d c) (Procompose (Cokleisli f') (Cokleisli g') d' c') (Cokleisli (Compose f g) d c) (Cokleisli (Compose f' g') d' c')
- newtype Rift p q a b = Rift {
- runRift :: forall x. p b x -> q a x

- decomposeRift :: Procompose p (Rift p q) :-> q

# Profunctor Composition

data Procompose p q d c where Source #

is the `Procompose`

p q`Profunctor`

composition of the
`Profunctor`

s `p`

and `q`

.

For a good explanation of `Profunctor`

composition in Haskell
see Dan Piponi's article:

Procompose :: p x c -> q d x -> Procompose p q d c |

## Instances

procomposed :: Category p => Procompose p p a b -> p a b Source #

# Unitors and Associator

idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c') Source #

`(->)`

functions as a lax identity for `Profunctor`

composition.

This provides an `Iso`

for the `lens`

package that witnesses the
isomorphism between

and `Procompose`

(->) q d c`q d c`

, which
is the left identity law.

`idl`

::`Profunctor`

q => Iso' (`Procompose`

(->) q d c) (q d c)

idr :: Profunctor q => Iso (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c') Source #

`(->)`

functions as a lax identity for `Profunctor`

composition.

This provides an `Iso`

for the `lens`

package that witnesses the
isomorphism between

and `Procompose`

q (->) d c`q d c`

, which
is the right identity law.

`idr`

::`Profunctor`

q => Iso' (`Procompose`

q (->) d c) (q d c)

assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b) (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b) Source #

The associator for `Profunctor`

composition.

This provides an `Iso`

for the `lens`

package that witnesses the
isomorphism between

and
`Procompose`

p (`Procompose`

q r) a b

, which arises because
`Procompose`

(`Procompose`

p q) r a b`Prof`

is only a bicategory, rather than a strict 2-category.

# Categories as monoid objects

eta :: (Profunctor p, Category p) => (->) :-> p Source #

a `Category`

that is also a `Profunctor`

is a `Monoid`

in `Prof`

# Generalized Composition

stars :: Functor g => Iso (Procompose (Star f) (Star g) d c) (Procompose (Star f') (Star g') d' c') (Star (Compose g f) d c) (Star (Compose g' f') d' c') Source #

`Profunctor`

composition generalizes `Functor`

composition in two ways.

This is the first, which shows that `exists b. (a -> f b, b -> g c)`

is
isomorphic to `a -> f (g c)`

.

`stars`

::`Functor`

f => Iso' (`Procompose`

(`Star`

f) (`Star`

g) d c) (`Star`

(`Compose`

f g) d c)

kleislis :: Monad g => Iso (Procompose (Kleisli f) (Kleisli g) d c) (Procompose (Kleisli f') (Kleisli g') d' c') (Kleisli (Compose g f) d c) (Kleisli (Compose g' f') d' c') Source #

costars :: Functor f => Iso (Procompose (Costar f) (Costar g) d c) (Procompose (Costar f') (Costar g') d' c') (Costar (Compose f g) d c) (Costar (Compose f' g') d' c') Source #

`Profunctor`

composition generalizes `Functor`

composition in two ways.

This is the second, which shows that `exists b. (f a -> b, g b -> c)`

is
isomorphic to `g (f a) -> c`

.

`costars`

::`Functor`

f => Iso' (`Procompose`

(`Costar`

f) (`Costar`

g) d c) (`Costar`

(`Compose`

g f) d c)

cokleislis :: Functor f => Iso (Procompose (Cokleisli f) (Cokleisli g) d c) (Procompose (Cokleisli f') (Cokleisli g') d' c') (Cokleisli (Compose f g) d c) (Cokleisli (Compose f' g') d' c') Source #

This is a variant on `costars`

that uses `Cokleisli`

instead
of `Costar`

.

`cokleislis`

::`Functor`

f => Iso' (`Procompose`

(`Cokleisli`

f) (`Cokleisli`

g) d c) (`Cokleisli`

(`Compose`

g f) d c)

# Right Kan Lift

This represents the right Kan lift of a `Profunctor`

`q`

along a `Profunctor`

`p`

in a limited version of the 2-category of Profunctors where the only object is the category Hask, 1-morphisms are profunctors composed and compose with Profunctor composition, and 2-morphisms are just natural transformations.

## Instances

decomposeRift :: Procompose p (Rift p q) :-> q Source #

The 2-morphism that defines a left Kan lift.

Note: When `p`

is right adjoint to

then `Rift`

p (->)`decomposeRift`

is the `counit`

of the adjunction.