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 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))
((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 forTwist
which is compatible with itsCategory
instance.)↩