| Copyright | (C) 2014 Edward Kmett |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | experimental |
| Portability | GADTs, TFs, MPTCs, RankN |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Data.Profunctor.Composition
Description
- 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)
- upstars :: Functor g => Iso (Procompose (UpStar f) (UpStar g) d c) (Procompose (UpStar f') (UpStar g') d' c') (UpStar (Compose g f) d c) (UpStar (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')
- downstars :: Functor f => Iso (Procompose (DownStar f) (DownStar g) d c) (Procompose (DownStar f') (DownStar g') d' c') (DownStar (Compose f g) d c) (DownStar (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 qProfunctor composition of the
Profunctors p and q.
For a good explanation of Profunctor composition in Haskell
see Dan Piponi's article:
Constructors
| Procompose :: p x c -> q d x -> Procompose p q d c |
Instances
| Category * p => ProfunctorMonad (Procompose p) | |
| ProfunctorFunctor (Procompose p) | |
| ProfunctorAdjunction (Procompose p) (Rift p) | |
| (Profunctor p, Profunctor q) => Profunctor (Procompose p q) | |
| (Choice p, Choice q) => Choice (Procompose p q) | |
| (Strong p, Strong q) => Strong (Procompose p q) | |
| (Closed p, Closed q) => Closed (Procompose p q) | |
| (Corepresentable p, Corepresentable q) => Corepresentable (Procompose p q) | |
| (Representable p, Representable q) => Representable (Procompose p q) | The composition of two |
| Profunctor p => Functor (Procompose p q a) | |
| type Corep (Procompose p q) = Compose (Corep p) (Corep q) | |
| type Rep (Procompose p q) = Compose (Rep q) (Rep p) |
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 cq d c, which
is the left identity law.
idl::Profunctorq => 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 cq d c, which
is the right identity law.
idr::Profunctorq => Iso' (Procomposeq (->) 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 bProf is only a bicategory, rather than a strict 2-category.
Generalized Composition
upstars :: Functor g => Iso (Procompose (UpStar f) (UpStar g) d c) (Procompose (UpStar f') (UpStar g') d' c') (UpStar (Compose g f) d c) (UpStar (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).
upstars::Functorf => Iso' (Procompose(UpStarf) (UpStarg) d c) (UpStar(Composef 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
downstars :: Functor f => Iso (Procompose (DownStar f) (DownStar g) d c) (Procompose (DownStar f') (DownStar g') d' c') (DownStar (Compose f g) d c) (DownStar (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.
downstars::Functorf => Iso' (Procompose(DownStarf) (DownStarg) d c) (DownStar(Composeg 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 downstars that uses Cokleisli instead
of DownStar.
cokleislis::Functorf => Iso' (Procompose(Cokleislif) (Cokleislig) d c) (Cokleisli(Composeg 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
| (~) (* -> * -> *) p q => Category * (Rift p q) |
|
| Category * p => ProfunctorComonad (Rift p) | |
| ProfunctorFunctor (Rift p) | |
| ProfunctorAdjunction (Procompose p) (Rift p) | |
| (Profunctor p, Profunctor q) => Profunctor (Rift p q) | |
| Profunctor p => Functor (Rift p q a) |
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.