Portability | GADTs |
---|---|

Stability | provisional |

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

Safe Haskell | Trustworthy |

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

- idl :: (Profunctor p, Profunctor q, Functor f) => p (q d c) (f (r d' c')) -> p (Procompose (->) q d c) (f (Procompose (->) r d' c'))
- idr :: (Profunctor p, Profunctor q, Functor f) => p (q d c) (f (r d' c')) -> p (Procompose q (->) d c) (f (Procompose r (->) d' c'))
- upstars :: (Profunctor p, Functor f, Functor h) => p (UpStar (Compose f g) d c) (h (UpStar (Compose f' g') d' c')) -> p (Procompose (UpStar f) (UpStar g) d c) (h (Procompose (UpStar f') (UpStar g') d' c'))
- kleislis :: (Profunctor p, Monad f, Functor h) => p (Kleisli (Compose f g) d c) (h (Kleisli (Compose f' g') d' c')) -> p (Procompose (Kleisli f) (Kleisli g) d c) (h (Procompose (Kleisli f') (Kleisli g') d' c'))
- downstars :: (Profunctor p, Functor g, Functor h) => p (DownStar (Compose g f) d c) (h (DownStar (Compose g' f') d' c')) -> p (Procompose (DownStar f) (DownStar g) d c) (h (Procompose (DownStar f') (DownStar g') d' c'))
- cokleislis :: (Profunctor p, Functor g, Functor h) => p (Cokleisli (Compose g f) d c) (h (Cokleisli (Compose g' f') d' c')) -> p (Procompose (Cokleisli f) (Cokleisli g) d c) (h (Procompose (Cokleisli f') (Cokleisli g') d' c'))

# Profunctor Composition

data Procompose p q d c whereSource

is the `Procompose`

p q`Profunctor`

composition of the profunctors `p`

and `q`

.

For a good explanation of profunctor composition in Haskell see Dan Piponi's article:

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

(Profunctor p, Profunctor q) => Profunctor (Procompose p q) | |

(Functor (Compose g f), Profunctor (Procompose p q), Corep f p, Corep g q) => Corep (Compose g f) (Procompose p q) | |

(Functor (Compose f g), Profunctor (Procompose p q), Rep f p, Rep g q) => Rep (Compose f g) (Procompose p q) | The composition of two representable profunctors is representable by the composition of their representations. |

Profunctor q => Functor (Procompose p q a) |

# Lax identity

idl :: (Profunctor p, Profunctor q, Functor f) => p (q d c) (f (r d' c')) -> p (Procompose (->) q d c) (f (Procompose (->) 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 p, Profunctor q, Functor f) => p (q d c) (f (r d' c')) -> p (Procompose q (->) d c) (f (Procompose 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)

# Generalized Composition

upstars :: (Profunctor p, Functor f, Functor h) => p (UpStar (Compose f g) d c) (h (UpStar (Compose f' g') d' c')) -> p (Procompose (UpStar f) (UpStar g) d c) (h (Procompose (UpStar f') (UpStar g') d' c'))Source

kleislis :: (Profunctor p, Monad f, Functor h) => p (Kleisli (Compose f g) d c) (h (Kleisli (Compose f' g') d' c')) -> p (Procompose (Kleisli f) (Kleisli g) d c) (h (Procompose (Kleisli f') (Kleisli g') d' c'))Source

downstars :: (Profunctor p, Functor g, Functor h) => p (DownStar (Compose g f) d c) (h (DownStar (Compose g' f') d' c')) -> p (Procompose (DownStar f) (DownStar g) d c) (h (Procompose (DownStar f') (DownStar g') d' c'))Source

cokleislis :: (Profunctor p, Functor g, Functor h) => p (Cokleisli (Compose g f) d c) (h (Cokleisli (Compose g' f') d' c')) -> p (Procompose (Cokleisli f) (Cokleisli g) d c) (h (Procompose (Cokleisli f') (Cokleisli g') d' c'))Source

This is a variant on `downstars`

that uses `Cokleisli`

instead of `DownStar`

.

`cokleislis`

::`Functor`

f => Iso' (`Procompose`

(`Cokleisli`

f) (`Cokleisli`

g) d c) (`Cokleisli`

(`Compose`

g f) d c)