splitInterchange.hs

import Control.Arrow

type IsEq a = (a, a)

splitInterchange :: (Arrow f) => f a1 a2 -> f a2 a3 -> f b1 b2 -> f b2 b3
                              -> IsEq (f (a1, b1) (a3, b3)) 
splitInterchange f1 f2 g1 g2 = (lhs, rhs)
  where
    lhs = (f1 >>> f2) *** (g1 >>> g2)
    rhs = (f1 *** g1) >>> (f2 *** g2)


{-
Can this law be derived from existing laws?

using: 1) f *** g = first f >>> second g              | default implementation of (***)
       2) first (f >>> g) = first f >>> first g       | arrow functor law
       3) second (f >>> g) = second f >>> second g    | the same as 2) but for 'second'
       4) second g >>> first f = first f >>> second g | arrow exchange law

lhs: (f1 >>> f2) *** (g1 >>> g2)
     first (f1 >>> f2) >>> second (g1 >>> g2)                | 1)
     first f1 >>> first f2 >>> second g1 >>> second g2       | 2) and 3)

rhs: (f1 *** g1) >>> (f2 *** g2)
     (first f1 >>> second g1) >>> (first f2 >>> second g2)   | 1)
     first f1 >>> second g1 >>> first f2 >>> second g2       | arrow associativity law
     first f1 >>> first f2 >>> second g1 >>> second g2       | 4)
     
     QED.
     
References:
 - http://haskell.cs.yale.edu/wp-content/uploads/2012/06/FromJFP.pdf
-}

I made a mistake by using 4) for the proof. This is not the arrow exchange law but the arrow commutativity law as defined in http://haskell.cs.yale.edu/wp-content/uploads/2012/06/FromJFP.pdf. That means this law only holds for commutative arrows and not conventional arrows.