Search code examples
haskellfunctional-programmingproof

Haskell: Is it true that function application distributes over list concatenation?


After reading this question: Functional proofs (Haskell)

And after looking at the inductive proof of forall xs ys. length (xs ++ ys) = length xs + length ys from the Haskell School of Music (page 164).

It seemed to me that function application distributes over list concatenation.

Hence the more general law might be that forall f xs ys. f (xs ++ ys) = f xs ++ f ys.

But how would one prove/disprove such a predicate?

-- EDIT --

I made a typo it was meant to be: forall f xs ys. f (xs ++ ys) = f xs + f ys, which matches what the previous question and the Haskell SoM uses. That being said, because of this typo, it's no longer "distributivity" property. However, @leftaroundabout made the correct answer for my original typoed question. And as for my intended question, the law is still not correct, because functions don't need the preserve the structural value. The f might give a completely different answer depending on the length of the list it is applied to.


Solution

  • No, this is clearly not true in general:

    f [_] = []
    f l = l
    

    then

    f ([1] ++ [2]) = f [1,2] = [1,2]
    

    but

    f [1] ++ f [2] = [] ++ [] = []
    

    I'm sure the functions which do have this problem form an interesting class, but general functions can do pretty much anything to a list's structure which thwarts such invariants.