What's the relationship between profunctors and arrows?

28
votes

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?

2
haskellfunctorcategory-theoryarrowsprofunctor
Kmett says Arrow is precisely Strong Category. – András Kovács
hackage.haskell.org/package/profunctors-5.2/docs/… ? – n. 1.8e9-where's-my-share m.
Linked in the Profunctors in Haskell: Categorifying Computations into Components via Arrows as Profunctors. – Petr

2 Answers

38
votes

What profunctors lack compared to arrows is the ability to compose them. If we add composition, will we get an arrow?

MONOIDS

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.

6
votes

@haoformayor's answer (and the referenced paper) is a great insight into the underlying category theory - monoidal categories are rather beautiful! - but I thought some code showing you how to turn an Arrow into a Strong Category and vice versa as they appear in their respective libraries might make a helpful addendum.

import Control.Arrow
import Control.Category
import Data.Profunctor
import Data.Profunctor.Strong
import Prelude hiding (id, (.))

One way...

newtype WrapP p a b = WrapP { unwrapP :: p a b }

instance Category p => Category (WrapP p) where
    id = WrapP id
    WrapP p . WrapP q = WrapP (p . q)

instance (Category p, Strong p) => Arrow (WrapP p) where
    first = WrapP . first' . unwrapP
    second = WrapP . second' . unwrapP

    -- NB. the first usage of id comes from (->)'s Category instance (id :: a -> a)
    -- but the second uses p's instance (id :: p a a)
    arr f = WrapP $ dimap f id id

... and t'other...

newtype WrapA p a b = WrapA { unwrapA :: p a b }

instance Arrow p => Profunctor (WrapA p) where
    dimap f g p = WrapA $ arr f >>> unwrapA p >>> arr g

instance Arrow p => Strong (WrapA p) where
    first' = WrapA . first . unwrapA
    second' = WrapA . second . unwrapA