Apparently, every Arrow is a Strong profunctor. Indeed ^>> and >>^ correspond to lmap and rmap. And first' and second' are just the same as first and second. Similarly every ArrowChoice is also Choice.
What profunctors lack compared to arrows is the ability to compose them. If we add composition, will we get an arrow? In other words, if a (strong) profunctor is also a category, is it already an arrow? If not, what's missing?
What profunctors lack compared to arrows is the ability to compose them. If we add composition, will we get an arrow?
This is exactly the question tackled in section 6 of "Notions of Computation as Monoids," which unpacks a result from the (rather dense) "Categorical semantics for arrows". "Notions" is a great paper because while it dives deep into category theory it (1) doesn't assume the reader has more than a cursory knowledge of abstract algebra and (2) illustrates most of the migraine-inducing mathematics with Haskell code. We can briefly summarize section 6 of the paper here:
Say we have
class Profunctor p where
dimap :: (contra' -> contra) -> (co -> co') -> p contra co -> p contra' co'
Your bog-standard, negative-and-positive dividin' encoding of profunctors in Haskell. Now this data type,
data (⊗) f g contra co = forall x. (f contra x) ⊗ (g x co)
as implemented in Data.Profunctor.Composition, acts like composition for profunctor. We can, for example, demonstrate a lawful instance Profunctor:
instance (Profunctor f, Profunctor g) => Profunctor (f ⊗ g) where
dimap contra co (f ⊗ g) = (dimap contra id f) ⊗ (dimap id co g)
We will hand-wave the proof that it is lawful for reasons of time and space.
OK. Now the fun part. Say we this typeclass:
class Profunctor p => ProfunctorMonoid p where
e :: (a -> b) -> p a b
m :: (p ⊗ p) a b -> p a b
This is, with a lot more hand-waving, a way of encoding the notion of profunctor monoids in Haskell. Specifically this is a monoid in the monoidal category Pro, which is a monoidal structure for the functor category [C^op x C, Set] with ⊗ as the tensor and Hom as its unit. So there's a lot of ultraspecific mathematical diction to unpack here but for that you should just read the paper.
We then see that ProfunctorMonoid is isomorphic to Arrow ... almost.
instance ProfunctorMonoid p => Category p where
id = dimap id id
(.) pbc pab = m (pab ⊗ pbc)
instance ProfunctorMonoid p => Arrow p where
arr = e
first = undefined
instance Arrow p => Profunctor p where
lmap = (^>>)
rmap = (>>^)
instance Arrow p => ProfunctorMonoid p where
e = arr
m (pax ⊗ pxb) = pax >> pxb
Of course we are ignoring the typeclass laws here but, as the paper shows, they do work out fantastically.
Now I said almost because crucially we were unable to implement first. What we have really done is demonstrated an isomorphism between ProfunctorMonoid and pre-arrows .The paper calls Arrow without first a pre-arrow. It then goes on to show that
class Profunctor p => StrongProfunctor p where
first :: p x y -> p (x, z) (y, z)
class StrongProfunctor p => StrongProfunctorMonoid p where
e :: (a -> b) -> p a b
m :: (p ⊗ p) a b -> p a b
is necessary and sufficient for the desired isomorphism to Arrow. The word "strong" comes from a specific notion in category theory and is described by the paper in better writing and richer detail than I could ever muster.
So to summarize:
A monoid in the category of profunctors is a pre-arrow, and vice versa. (A previous version of the paper used the term "weak arrows" instead of pre-arrows, and that's OK too I guess.)
A monoid in the category of strong profunctors is an arrow, and vice versa.
Since monad is a monoid in the category of endofunctors we can think of the SAT analogy Functor : Profunctor :: Monad : Arrow. This is the real thrust of the notions-of-computation-as-monoids paper.
Monoids and monoidal categories are gentle sea creatures that appear everywhere, and it's a shame that some students will go through computer science or software engineering education without being taught monoids.
Category theory is fun.
Haskell is fun.