Equational reasoning examples

Equational reasoning

One of the advantages often claimed for pure functional languages is the ease of equational reasoning, enabled by referential transparency and being able to replace equals by equals in all contexts. That is all great, and this page is not about repeating or elaborating on these things. But what, if anything, does it mean in programming practice?

This page is about collecting (links to) examples of equational reasoning in use. Please add any examples you encounter, provided you found them useful or enlightening, and comment on what you find most helpful about the examples. The examples don't have to be completely formal, but they should address some real issue, and be mostly readable by pragmatic Haskell programmers (we assume that the equational reasoning formalists have their own forums/pages;-). It is not necessary to copy the examples here, but your explanatory text should provide sufficient keywords to make this page findable by related searches.

Coding style

Haskellers of all levels are sometimes frustrated by not being able to understand the clever code produced by more advanced Haskellers. They see that the suggested solutions work, but either they can't see how, or they wouldn't have been able to come up with that kind of solution themselves. Well, Haskelling is a never-ending learning process, and one way to understand a piece of Haskell magic is to look behind the curtain: look up the definitions of the functions used, and unfold them in place, then simplify, and repeat until something emerges that you could have come up with yourself. That's an example application of equational reasoning!-)

Coding style: clever vs readable

In this long and interesting thead, the question was whether to prefer writing Haskell code that is more easily understood by beginners, or code that makes full use of the author's experience with possibly advanced Haskell abstractions. Note that there is no simple answer to this, it depends on context, audience, perception, commenting, types, presentation, etc, and even led to questions about a possible need to modernize Haskell teaching.

From the perspective of this wiki page, the interesting part is that various solutions for an example problem were proposed, involving direct recursive definitions, state transformers, scanl, and other approaches. Ideas about which form of definition were most readable, or even obvious, differed widely, and there seemed to be no way to reconcile the differences. And then it appeared that the suggested solutions weren't actually equivalent semantically..

This message takes the abstract state transformer solution and rewrites it step by step into a directly recursive definition that turns out to be slightly different from the originally specified direct recursion, confirming the problems indicated by manual and quickcheck testing.

This message revisits the problem, using the initial derivation to suggest a fix to the state transformer solution (no updated derivation is provided, though) as well as a modified scanl solution (for this, an abbreviated derivation into a directly recursive form matching the original spec is given). It turns out that both explicitly and implicitly recursive solution suggestions, in spite of being considered obvious by some, exhibited differences from the original spec.

Equational reasoning is useful here for demonstrating correctness or exposing incorrectness (while suggesting avenues for making corrections) more comprehensively than tests could. More importantly, though, program transformations provide the means for view transformations (mainly from abstract to concrete, but modulo the necessary insights also backwards), so code written in abstract fashion can still be understood and form the starting point for advancements in Haskell program understanding (though authors should be aware that the amount of work needed to read their code increases with the number of abstractions that readers may be unfamiliar with, just as the level of conciseness increases the same way).

Coding style: indentation creep with nested Maybe

Here the issue was direct use of Maybe, which led to levels of nesting which the original poster was rightly concerned about. Haskellers answered with various small improvement suggestions until someone brought it all together and dropped an alternative version of the code, hiding the explicit Maybe-matching in higher-levels of abstraction. The original poster was both impressed, and a little intimidated by an advanced solution that seemed to have no direct connection to the original code.

This message tried to explain the magic by transforming the original code in many small steps into the suggested final version. It wasn't entirely correct (follow the thread from there for questions, answers, and fix), but it did the job in terms of explanation and turning frustration into fun.