Several people have claimed (1,2,3) that Haskell’s `Arrow`

class is exactly the intersection of `Category`

and `Strong`

(from `profunctors`

). This is often justified by a reference to “Notions of Computation as Monoids” by Rivas and Jaskelioff, which shows the correspondence between Arrows and monoids in a category of strong profunctors, but that is actually a different point. To be an `Arrow`

, it is not enough for a type constructor to be an instance of `Strong`

(i.e., a strong profunctor) and be an instance of `Category`

(i.e., having some monoidal structure): the monoid and the strength must also be compatible.

Some quick definitions, for background.

First, the `Profunctor`

and `Strong`

classes and their respective laws:

```
class Profunctor p where
dimap :: (a' -> a) -> (b -> b') -> p a b -> p a' b'
-- Laws:
-- P1: dimap id id p = p
-- P2: dimap f g (dimap h k p) = dimap (h . f) (g . k) p
class Profunctor p => Strong p where
first' :: p a b -> p (a,c) (b,c)
-- Laws:
-- SP1: first' (first' p) = dimap assocr assocl (first' p)
-- SP2: dimap id fst (first' p) = dimap fst id p
-- SP3: dimap (id *** f) id (first' p) =
-- dimap id (id *** f) (first' p)
-- SP4: dimap (f *** id) (g *** id) (first' a) =
-- first' (dimap f g p)
assocl (x,(y,z)) = ((x,y),z)
assocr ((x,y),z) = (x,(y,z))
f *** g = \(x,y) -> (f x, g y)
-- equivalently, the one from Arrow
```

P1 and P2 are simply the usual functor laws, applied to profunctors. The laws for `Strong`

are not explicitly stated in `profunctors`

, but come from the idea that `first`

is a “strength”. SP3 and SP4 are guaranteed by the parametricity of `first'`

.

Next, the Haskell's `Category`

and `Arrow`

classes and their respective laws:

```
class Category p where
id :: p a a
(.) :: p b c -> p a b -> p a c
-- Laws:
-- C1: p . (q . r) = (p . q) . r
-- C2: id . p = p
-- C3: p . id = p
class Category p => Arrow p where
arr :: (a -> b) -> p a b
first :: p a b -> p (a,c) (b,c)
-- Laws:
-- A1: arr id = id
-- A2: arr (g . f) = arr g . arr f
-- A3: first (arr f) = arr (f *** id)
-- A4: first (p . q) = first p . first q
-- A5: arr (id *** f) . first p = first p . arr (id *** f)
-- A6: arr fst . first p = p
-- A7: arr assocr . first (first p) = first p . arr assocr
```

The claim is that any instance of `Strong`

and `Category`

is also an instance of `Arrow`

. That is,

```
newtype SPCA p a b = SPCA { unSPCA :: p a b }
deriving (Profunctor, Strong, Category)
instance (Strong p, Category p) => Arrow (SPCA p) where
arr f = SPCA (dimap f id id)
first = first'
```

This assumes that the `Arrow`

laws can be proven using only the laws for `Profunctor`

, `Strong`

, and `Category`

, but none of these laws describe the interaction of `dimap`

and `first'`

with `(.)`

and `id`

. Indeed, these laws could not describe these interactions, because `Arrow`

is the first class to include all four of these operations.

Thus, it is possible to define a type with lawful instances of `Category`

, `Profunctor`

, and `Strong`

for which `SPCA`

will give an unlawful `Arrow`

. For example:

```
newtype Twist a b = Twist { getTwist :: (a,a) -> (b,b) }
instance Category Twist where
id = Twist id
Twist f . Twist g = Twist (f . g)
instance Profunctor Twist where
dimap pre post (Twist f) =
Twist ((post *** post) . f . (pre *** pre))
instance Strong Twist where
first' (Twist f) = Twist (\((a1,c1),(a2,c2)) ->
let (b1,b2) = f (a1,a2) in ((b1,c2),(b2,c1)))
```

That’s all pretty standard, aside from the twist in the last line. The proofs for the `Category`

and `Profunctor`

laws are obvious. Proofs that `Twist`

satisfies the `Strong`

laws are similarly simple, but perhaps less obvious, so I've included them in the appendix.

**Although Twist is a lawful instance of Strong and Category, it is not an Arrow.** In particular, an instance following the

`SPCA`

pattern violates several `Arrow`

laws:```
instance Arrow Twist where
arr f = dimap f id id
first = first'
```

We can easily observe a violation of A3:

```
> getTwist (arr (id *** id)) ((1,2),(3,4))
((1,2),(3,4))
> getTwist (first (arr id)) ((1,2),(3,4))
((1,4),(3,2))
```

A4 is similarly violated.

## What went wrong?

Now, this is not a disproof that a monoid in the category of strong profunctors is an arrow. That result is sound. The problem is that having instances of `Category`

and `Strong`

is insufficient does not guarantee being a strong profunctor monoid.

Part of this confusion most likely stems from the loose way Haskell programmers tend to use ideas from category theory. This looseness is often convenient, but it can hide distinctions between related categories with different properties.

For example, `Twist`

can be represented as an object in **Pro**, a monoidal category of profunctors described by Rivas and Jaskelioff. That object forms a monoid. It can also be represented as an object in **SPro**, a monoidal category of strong profunctors, but *that* object is *not* a monoid. Haskell gains flexibility by blurring the distinction between objects in **Pro** and objects in **SPro**, but even though the types for their respective monoid operations are the same, the correctness conditions are different.

## Defining monoids of profunctors

I mentioned **Pro** and **SPro** and monoids in those categories, so I thought it might be useful to describe them a bit more. This is mostly a recap of the paper, so feel free to skim.

First, **Pro** is a category whose objects are profunctors and whose morphisms are natural transformations between profunctors. To conveniently represent the latter, we define:

`type p :-> q = forall a b. p a b -> q a b`

Conveniently, any function `f :: p :-> q`

is guaranteed to be a natural transformation by parametricity.

To talk about monoids in **Pro**, we first need to define a monoidal structure, and we’re going to work with profunctor composition. Re-using the terminology from `Data.Profunctor.Composition`

, we have:

```
data Procompose p q a b =
forall x. Procompose (p x b) (q a x)
instance (Profunctor p, Profunctor q)
=> Profunctor (Procompose p q) where
dimap pre post (Procompose p q) =
Procompose (dimap id post p) (dimap pre id q)
```

This is a bifunctor over **Pro**, and has three natural transformations which make it monoidal.

```
pmap :: (p :-> p') -> (q :-> q')
-> (Procompose p q :-> Procompose p' q')
pmap f g (Procompose p q) = Procompose (f p) (g q)
passoc :: Procompose (Procompose p q) r :->
Procompose p (Procompose q r)
passoc (Procompose (Procompose p q) r =
Procompose p (Procompose q r)
idr :: Profunctor p => Procompose p (->) :-> p
idr (Procompose p f) = dimap f id p
idl :: Profunctor p => Procompose (->) p :-> p
idl (Procompose f p) = dimap id f p
```

(The last three all have inverses, but we won’t need them here.)

With these definitions, we can talk about monoids in **Pro** and describe their laws.

```
class Profunctor p => ProfunctorMonoid p where
mult :: Procompose p p :-> p
unit :: (->) :-> p
-- Laws:
-- PM1: mult . pmap id mult = mult . pmap mult id . passoc
-- PM2: mult . pmap unit id = idl
-- PM3: mult . pmap id unit = idr
```

Given an instance of `ProfunctorMonoid`

, we can define an instance of `Category`

in an obvious way.

Next, **SPro** is a category whose objects are strong profunctors^{1} and whose morphisms are strong natural transformations, meaning they are compatible with the strengths.

```
type SPNT p q = forall a b. p a b -> q a b
-- Law: f . first' = first' . f
```

Unfortunately, parametricity is not enough to guarantee this. As an example,

```
twist :: (a -> b) -> Twist a b
twist f = Twist (f *** f)
```

This has the right type to be a strong natural transformation, but it does not respect the strengths.

```
> getTwist (twist (first' id)) ((1,2),(3,4))
((1,2),(3,4))
> getTwist (first' (twist id)) ((1,2),(3,4))
((1,4),(3,2))
```

Fortunately, `pmap`

, `passoc`

, `idl`

, and `idr`

do respect the strengths, so we can reuse them when defining a class for strong profunctor monoids:

```
class (Strong p, ProfunctorMonoid p)
=> StrongProfunctorMonoid p where
smult :: SPNT (Procompose p p) p
sunit :: SPNT (->) p
-- Laws:
-- SPM1: smult . pmap id smult = mult . pmap smult id . passoc
-- SPM2: smult . pmap sunit id = idl
-- SPM3: smult . pmap id sunit = idr
instance (Strong p, Strong q) => Strong (Procompose p q) where
first' (Procompose p q) = Procompose (first' p) (first' q)
```

Note that the only difference between `StrongProfunctorMonoid`

and `ProfunctorMonoid`

is the requirement that `smult`

and `sunit`

respect the strengths. The other laws are effectively the same.

Given an instance of `StrongProfunctorMonoid`

, it is easy to define lawful instances of `Category`

and `Arrow`

, and vice versa.

## What are the instances of `ProfunctorMonoid`

?

Earlier I mentioned that any instance of `ProfunctorMonoid`

can define an instance of `Category`

, but are instances of `Profunctor`

and `Category`

enough to define a lawful instance of `ProfunctorMonoid`

? I’m not certain.

Certainly, we can define functions with the appropriate types, as the `profunctor`

package does:

```
mult' :: Category p => Procompose p p :-> p
mult' (Procompose p q) = p . q
unit' :: (Category p, Profunctor p) => (->) :-> p
unit' f = dimap f id id
```

Of these, `mult'`

seems pretty obviously correct. PM1 reduces easily to C1. In contrast, `unit'`

involves an interaction between `dimap`

and `id`

, which is not addressed by any of the available laws. If we knew, for example,

`X: dimap id f p . q = p . dimap f id q`

that would be sufficient to prove PM2 and PM3 (and also to show that `dimap f id id = dimap id f id`

). Unfortunately, I don’t see any way to derive X algebraically, given the laws we have. Conversely, I don’t see any way to define lawful instances of `Category`

and `Profunctor`

which violate X, so there may be a way to derive it by appealing to aspects of Haskell’s type system. (I would not expect this property to hold in a general categorical setting.)

In particular, P1 and the inability for Haskell functions to distinguish `id`

from an arbitrary function seemingly prevent `dimap`

from marking its results in a way that `(.)`

could use to distinguish the two sides in X. (Note that X is easily proven in the case where `f = id`

.) I imagine something more rigorous could be made of this, but I will have to leave it for better practitioners.

## Appendix: Proofs

Proof that `Twist`

is a lawful instance of `Strong`

:

```
SP1:
first' (first' p)
=
first' (Twist (\((a1,c1),(a2,c2)) ->
let (b1,b2) = getTwist p (a1,a2) in ((b1,c2),(b2,c1))))
=
Twist (\(((a1,c1),d1),((a2,c2),d2)) ->
let (bc1,bc2) =
let (b1,b2) = getTwist p (a1,a2) in ((b1,c2),(b2,c1))
in ((bc1,d2),(bc2,d1)))
=
Twist (\(((a1,c1),d1),((a2,c2),d2)) ->
let (b1,b2) = getTwist p (a1,a2) in (((b1,c2),d2),(b2,c1),d1))
=
Twist (\(((a1,c1),d1),((a2,c2),d2)) ->
let (b1,b2) = getTwist p (a1,a2)
in (assocl (a1,(c2,d2)), assocl (a2,(c1,d1))))
=
Twist (\(((a1,c1),d1),((a2,c2),d2)) ->
let (bcd1,bcd2) =
let (b1,b2) = getTwist p (a1,a2) in ((a1,(c2,d2)),(a2,(c1,d1)))
in (assocl bcd1, assocl bcd2))
=
Twist (\(((a1,c1),d1),((a2,c2),d2)) ->
let (bcd1,bcd2) = getTwist (first' p) ((a1,(c1,d1)),(a2,(c2,d2)))
in (assocl bcd1, assocl bcd2))
=
Twist (\(acd1,acd2) ->
let (bcd1,bcd2) = getTwist (first' p) (assocr acd1, assocr acd2)
in (assocl bcd1, assocl bcd2)
=
Twist ((assocl *** assocl) . getTwist (first' p) . (assocr *** assocr))
=
dimap assocr assocl (first' p)
SP2:
dimap id fst (first' p)
=
Twist ((fst *** fst) . getTwist (first' p) . (id *** id))
=
Twist ((fst *** fst) . getTwist (first' p))
=
Twist (\((a1,c1),(a2,c2)) -> (fst *** fst) (getTwist (first' p) ((a1,c1),(a2,c2))))
=
Twist (\((a1,c1),(a2,c2)) -> let (b1,b2) = getTwist p (a1,a2) in (fst *** fst) ((b1,c2),(b2,c1)))
=
Twist (\((a1,c1),(a2,c2)) -> let (b1,b2) = getTwist p (a1,a2) in (b1,b2))
=
Twist (\((a1,c1),(a2,c2)) -> getTwist p (a1,a2))
=
Twist (getTwist p . (fst *** fst))
=
Twist ((id *** id) . getTwist p . (fst *** fst))
=
dimap fst id p
```

SP3 and SP4 are guaranteed by parametricity.

These objects should be pairs containing a profunctor and a strength. In Haskell, instances of

`Strong`

uniquely determine the strength, but this is not true in general. (For example, there is an obvious alternative strength for`Twist`

which*is*compatible with its`Category`

instance.)↩