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 |
- 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 #
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 |
procomposed :: Category p => Procompose p p a b -> p a b #
Unitors and Associator
idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c') #
(->)
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') #
(->)
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) #
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.
Categories as monoid objects
eta :: (Profunctor p, Category p) => (->) :-> p #
a Category
that is also a Profunctor
is a Monoid
in Prof
mu :: Category p => Procompose p p :-> p #
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') #
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') #
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') #
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') #
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.
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) :-> q #
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.