Portability  GADTs, TFs, MPTCs, RankN 

Stability  experimental 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Safe Haskell  Trustworthy 
 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 whereSource
is the Procompose
p qProfunctor
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 
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) 
procomposed :: Category p => Procompose p p a b > p a bSource
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
::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 cq 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 bProf
is only a bicategory, rather than a strict 2category.
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
::Functor
f => Iso' (Procompose
(UpStar
f) (UpStar
g) d c) (UpStar
(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
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
::Functor
f => Iso' (Procompose
(DownStar
f) (DownStar
g) d c) (DownStar
(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 downstars
that uses Cokleisli
instead
of DownStar
.
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 2category of Profunctors where the only object is the category Hask, 1morphisms are profunctors composed and compose with Profunctor composition, and 2morphisms are just natural transformations.
Category p => ProfunctorComonad (Rift p)  
ProfunctorFunctor (Rift p)  
ProfunctorAdjunction (Procompose p) (Rift p)  
~ (* > * > *) p q => Category (Rift p q) 

(Profunctor p, Profunctor q) => Profunctor (Rift p q)  
Profunctor p => Functor (Rift p q a) 
decomposeRift :: Procompose p (Rift p q) :> qSource
The 2morphism that defines a left Kan lift.
Note: When p
is right adjoint to
then Rift
p (>)decomposeRift
is the counit
of the adjunction.