Arrow law: first depends only on the first component of the pair. Why do we need this one?

Question

John Hughes in his "Generalising Monads to Arrows" writes (chapter 8):

We formalise the property that first f depends only on first components of pairs as follows: first f >>> arr fst = arr fst >>> f

I understand that the law filters out implementations of such sort:

newtype KleisliMaybe a b = KMb { runKMb :: a -> Maybe b }

instance Category KleisliMaybe where 
 ...

instance Arrow KleisliMaybe where
 first f = KMb $ const Nothing
 ...

But the wording seems a bit odd for this case (I would have chosen "first has no side-effects" or something like that for such an instance).

So, what are other reasons to keep it around?

Moreover, there is another law: first f >>> second (arr g) = second (arr g) >>> first f. I did not find any implementations it filters out (I did - see the edit). How does this law help us?

---

Edit: more thoughts on the latter law.

Take a look at the following snippet:

newtype KleisliWriter = KW { runKW :: a -> (String, b) }

instance Category KleisliWriter where
 ...

instance Arrow KleisliWriter where
 arr f = KW $ \ x -> ("", f x)
 first  (KW f) = KW $ \ ~(a, d) -> f a >>= (\ x -> ("A", (x, d)))
 second (KW f) = KW $ \ ~(d, b) -> f b >>= (\ x -> ("B", (d, x)))

Such an instance behaves this way:

GHCi> c = KW $ \ x -> ("C", x)
GHCi> fst . runKW (first c >>> second (arr id)) $ (1, 2)
"CAB"
GHCi> fst . runKW (second (arr id) >>> first c) $ (1, 2)
"BCA"

As far as I get it, we have got no law for second f = swap >>> first f >>> swap. Therefore, we can forbid both second and first to have any side-effects with this law. Yet, the original wording still does not seem to hint at that again:

...we formalise the intuition that the second component of the pair is unaffected by first f as a law...

Are those laws just pure formalisations for solid proofs?

Answer 1

Short answer: There's a different pair of laws that cover "first and second have no side-effects":

first (arr f) = arr (first f)
second (arr f) = arr (second f)

After thinking about it, I THINK that both laws you've identified:

first f >>> arr fst          =   arr fst >>> f                -- LAW-A
first f >>> second (arr g)   =   second (arr g) >>> first f   -- LAW-B

are, in fact, redundant because they follow from those no-side-effects laws, the other laws, and a couple of "free theorems".

Your counterexamples violate the no-side-effects laws, so that's why they also violate LAW-A and/or LAW-B. If someone has a true counterexample that obeys the no-side-effects laws but violates LAW-A or LAW-B, I'd be very interested in seeing it.

Long answer:

The property "first has no side effects (of its own, at least)" is better formalized by the law stated earlier in Section 8 of that article:

first (arr f) = arr (first f)

Recall that Hughes says an arrow is "pure" (equivalently, "has no side-effects") if it can be written arr expr. So, this law states that, given any computation that is already pure and so can be written arr f, applying first to that computation also results in a pure computation (because it is of the form arr expr with expr = first f). Therefore, first introduces no impurities / no effects of its own.

The other two laws:

first f >>> arr fst          =   arr fst >>> f                -- LAW-A
first f >>> second (arr g)   =   second (arr g) >>> first f   -- LAW-B

are intended to capture the idea that for a particular instance Arrow Foo and a particular arrow action f :: Foo B C, the action:

first f :: forall d. Foo (B,d) (C,d)

acts on the first components of its input/output pairs as if the second components weren't there. The laws correspond to the properties:

1. LAW-A: the output component C and any side effects depend only on input B, not input d (i.e., no dependence on d)
2. LAW-B: the component d passes through unchanged, unaffected by the input B or any side effects (i.e., no effect on d)

With respect to LAW-A, if we consider the action first f :: Foo (B,d) (C,d) and focus on the C component of its output using a pure function to extract it:

first f >>> arr fst :: Foo (B,d) C

then the result is the same as if we first forcibly remove the second component using a pure action:

arr fst :: Foo (B,d) B

and allow the original action f to act only on B:

arr fst >>> f :: Foo (B,d) C

Here, the structure of the first f >>> arr fst action leaves open the possibility that first f can depend on the d component of the input in formulating its side effects and constructing the C component of its output; but, the structure of the arr fst >>> f action eliminates this possibility by removing the d component via a pure action before allowing any non-trivial computation by f. The fact that these two actions are equal (the law) makes it clear that first f produces a C output (and side effects, through f, since first has no additional effects of its own) from the B input in a manner that can't also depend on the d input.

LAW-B is is harder. The most obvious way of formalizing this property would be the pseudolaw:

first f >>> arr snd = arr snd

which directly states that first f doesn't change the extracted (arr snd) second component. However, Hughes points out that this is too restrictive, because it doesn't allow first f to have side effects (or at least any that can survive the pure action arr snd). Instead, he provides the more complicated law:

first f >>> second (arr g)   =   second (arr g) >>> first f

The idea here is that, if first f ever modified the d value, then there would be some case where the following two actions would be different:

-- `first f` changes `inval` to something else
second (arr (const inval)) >>> first f
-- if we change it back, we change the action
second (arr (const inval)) >>> first f >>> second (arr (const inval))

But, because of LAW-B, we have:

second (arr (const inval)) >>> first f >>> second (arr (const inval))
-- associativity
= second (arr (const inval)) >>> (first f >>> second (arr (const inval)))
-- LAW-B
= second (arr (const inval)) >>> (second (arr (const inval)) >>> first f)
-- associativity
= (second (arr (const inval)) >>> (second (arr (const inval))) >>> first f
-- second and arr preserve composition
= second (arr (const inval >>> const inval)) >>> first f
-- properties of const function
= second (arr (const inval)) >>> first f

and so the actions are the same, contrary to our assumption.

HOWEVER, I conjecture that LAW-A and LAW-B are both redundant, because I believe (see my hesitation below) they follow from the other laws plus a "free theorem" for the signature:

first f :: forall d. Foo (B,d) (C,d)

Assuming first and second satisfy the no-side-effects laws:

first (arr f) = arr (first f)
second (arr f) = arr (second f)

then LAW-B can be rewritten as:

first f >>> second (arr g)              = second (arr g) >>> first f
-- no side effects for "second"
first f >>> arr (second g)              = arr (second g) >>> first f
-- definition of "second" for functions
first f >>> arr (\(x,y) -> (x, g y))  = arr (\(x,y) -> (x, g y)) >>> first f

and this last statement (call it LAW-B-prime) is just the free theorem for first f. (Intuitively, since first f is polymorphic in the type of d, any pure action on d is necessarily "invisible" to first f, so first f and any such action will commute.) Similarly, there's a free theorem for:

first f >>> arr fst :: forall d. Foo (B,d) C

that captures the idea that, since this signature is polymorphic in d, no pure pre-action on d can affect the action:

arr (\(x,y) -> (x, g y)) >>> (first f >>> arr fst) = first f >>> arr fst

But the left-hand side can be rewritten:

-- by associativity
(arr (\(x,y) -> (x, g y)) >>> first f) >>> arr fst
-- by LAW-B-prime
(first f >>> arr (\(x,y) -> (x, g y))) >>> arr fst
-- by associativity
first f >>> (arr (\(x,y) -> (x, g y)) >>> arr fst)
-- `arr` preserves composition
first f >>> arr ((\(x,y) -> (x, g y)) >>> fst)
-- properties of fst
first f >>> arr fst

giving the right-hand side.

I only hesitate here because I'm not used to thinking about "free theorems" for possibly effectful arrows instead of functions, and so I'm not 100% sure that it goes through.

I'd be very interested to see if someone can come up with true counterexamples for these laws that violate LAW-A or LAW-B but satisfy the no-side-effects laws. The reason your counterexamples violate LAW-A and LAW-B is that they violate the no-side-effects laws. For your first example:

> runKMb (first (arr (2*))) (2,3)
Nothing
> runKMb (arr (first (2*))) (2,3)
Just (4,3)

and for your second:

> runKW (first (arr (2*))) (1,2)
("A",(2,2))
> runKW (arr (first (2*))) (1,2)
("",(2,2))