1

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.

Community
  • 1
  • 1
CMCDragonkai
  • 6,222
  • 12
  • 56
  • 98
  • "But how would one prove/disprove such a predicate?" By induction, I assume. If you are a real genius you could probably do it by inspection, but for the rest of us, induction has been the way to go for quite a few centuries. It isn't actually true - what you probabl want is the weaker statement - `foldr f x xs \`f\` foldr f x ys = foldr f x (xs ++ ys)`. – user2407038 Feb 16 '16 at 11:25
  • But is the proof the same as the proofs for `forall xs ys. length (xs ++ ys) = length xs + length ys`? How does one prove by induction for functions? What is `n` and `n + 1` in terms of functions? – CMCDragonkai Feb 16 '16 at 11:29
  • How did you even arrive at that more general law? It doesn't typecheck with the specific one (suddenly `f` needs to return a list), and even with concatenation is trivially disproven by substituting `tail` for `f`: `tail ([1] ++ [2]) == [2]` whereas `tail [1] ++ tail [2] == []`. – Sebastian Redl Feb 16 '16 at 11:29

2 Answers2

8

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.

leftaroundabout
  • 117,950
  • 5
  • 174
  • 319
  • 4
    For the record, such functions are called [homomorphisms](https://ncatlab.org/nlab/show/homomorphism) (magma homomorphisms in this case). – gallais Feb 16 '16 at 12:11
3

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.

Well, clearly that is not the case. For example:

reverse ([1..3] ++ [4..6]) /= reverse [1..3] ++ reverse [4..6]

The example that you're quoting is a special case that's called a monoid morphism: a function f :: m -> n such that:

  1. m and n are monoids with binary operation <> and identity mempty;
  2. f mempty = mempty
  3. f (m <> m') == f m <> f m'

So length :: [a] -> Int is a monoid morphism, sending [] to 0 and ++ to +:

length [] = 0
length (xs ++ ys) = length xs + length ys
Luis Casillas
  • 29,802
  • 7
  • 49
  • 102