The slings and arrows of outrageous fortune

Arrow is more than Strong and Category

By Dave Menendez
Tuesday, July 18, 2017, at 9:07 PM
Filed under: Haskell

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))
> getTwist (first (arr id)) ((1,2),(3,4))

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 profunctors1 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))
> getTwist (first' (twist id)) ((1,2),(3,4))

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:

    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)

    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.

  1. 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.)