[theamk]

Maybe I am not a enough of a functional programmer, but I don't see what's impossible here? Any symbolic algebra system (like Wolfram Mathematica) can do such derivations, and much more.

Sure, this is interesting, but in the sense of "look at this emergent behavior -- such a simple system can do unusually complex result", rather than "wow! no one could do such things with computer before"

[lmm]

You can do symbolic algebra on symbolic function definitions. What's interesting about this stuff is that it works for "real" functions - plain Haskell functions that we can't inspect the definition of, just call in the normal way (there's no macros or monkeypatching or anything like that going on). It's like being able to use numerical methods but still somehow solve everything exactly.

[octachron]

Deciding that symbolic expressions are equal is in fact undecidable for even relatively simple sets of symbolic expressions: this is Richardson's theorem.

So this is an example of carefully constrained conditions where equality between all total functions on an infinite set is decidable.