Distributivity laws can be simplified

[viercc]

The documentation of Zip says an instance of Zip must satisfy the following Distributivity laws.

-- The distributivity laws of Zip f
                   align (zip xs ys) zs ≡ undistrThesePair <$> zip (align xs zs) (align ys zs)
distrPairThese <$> zip (align xs ys) zs ≡                      align (zip xs zs) (zip ys zs)
                   zip (align xs ys) zs ≡ undistrPairThese <$> align (zip xs zs) (zip ys zs)

Each of the three equations must hold. Let me name each equation as Distr(1) - Distr(3).

-- Distr(1)
align (zip xs ys) zs ≡ undistrThesePair <$> zip (align xs zs) (align ys zs)

-- Distr(2)
distrPairThese <$> zip (align xs ys) zs ≡ align (zip xs zs) (zip ys zs)

-- Distr(3)
zip (align xs ys) zs ≡ undistrPairThese <$> align (zip xs zs) (zip ys zs)

But only Distr(2) is necessary among three, if I'm not mistaken. The rest follows from Distr(2).

Gist: https://gist.github.com/viercc/5b79efc5c3593a1b487a51f04c2bffca#file-distributive-simplify-md

I propose changes to the documentation stating this.

• Remove Distr(1) from the law and add a note that it follows from Distr(2).
• Just remove Distr(3). It is a direct consequence of undistrPairThese . distrPairThese = id.
  • Probably there should be a comment on undistrPairThese that it is a left inverse (but not the inverse) of distrPairThese.