Equational programming
Posted on December 25, 2010
by Tommy McGuire
It is Christmas and Dr. McGuire is too busy watching snow fall to come up with a real post, so he is just rehashing a reply to a question on the haskell-beginners mailing list as if it were new. Typical.Jun HU wrote:
My first language is C, and I've strong intention in learning a pure functional programming language. My very first question is how to think in the functional programming way, anyone has some ideas.
I cannot claim C as my first language, but I do say it is my "natural" language; I have written more code in C than I have in any other, and I've been using it for nigh on 20 years. I also cannot claim to think in the functional programming way, but using O'Caml and Haskell has definitely changed how I program in any language. In fact, I suspect functional programming has had a bigger effect than I had previously considered. But I am definitely not a Haskell guru.
I believe the biggest difference between functional and procedural programming is thinking equationally rather than operationally. With procedural programming as in C (and most object oriented languages, which in my experience are more procedural than not), the tendency is to think operationally: "First the program does this, then that happens, then that,...." Now, back at UT Austin (I grew up in the land of Dijkstra), at the time anyway, they were fond of teaching axiomatic thinking: "At this point in the program text, the state is this; at that point in the text, the state is that...." That is definitely a significant improvement, and I attribute what decent code I have written to that approach, but it definitely is not as natural as either operational or equational thinking.
Thinking operationally (or "pretending to be the computer") is problematic because there are typically an exponential number of paths through a program. As a result, it is impossible to completely understand even middling small program. Further, operational approaches provide no particularly good strategies for developing programs.
If you can get past the initial visceral revulsion at the thought of proving programs correct (Horrors!), thinking axiomatically has significant benefits. On one hand, it reduces the exponential number of paths through the program to a linear number of positions in the program text. For example, if you have a block of program text s which, in a program state p is guaranteed to arrive at another state q, and likewise program text t going from q to r, then you have s;t going from p to r; it doesn't matter what happens in the middle. Further, axiomatic thinking does provide some guidance to writing code: if you think you need a conditional statement, then you want to go from p to some narrow, definite state q; if you need a loop, then you can look for an invariant and a termination condition. Not easy, but there is something
On the other hand, in functional languages (and also when taking functional approaches in a non-functional language), it is very important to think equationally: "This means that; this other thing is that...." This is especially true in Haskell, which is not strict; if you try to think operationally or even axiomatically, you run into difficulties when the state of a non-strict program does not resemble the state of a strict program.
Equational thinking completely does away with the "number of paths" argument. A functional definition is, or should be, small enough to understand directly, based on any underlying definitions. Further, because the state does not change (in operational terms, or equivalently in axiomatic terms, there is only one state), it becomes less important to manipulate the program as a whole. Instead each definition can be dealt with separately.
Now, equational thinking is easy for stuff like
\[\textbf{add_one}\ n = n + 1\]
But it is not immediately apparent how that extends to something that needs recursion, say. The big "Ah-ha!" moment for me was the realization that recursion and mathematical induction are the same thing (ok, it's not a surprise for anyone; the big deal was when I internalized it enough to use the idea to naturally write code). With that, you can deal with anything programmatically equational and recursive as mathematically equational and inductive. The change in thinking is as big as the difference between operational and axiomatic.
Equational thinking extends beyond basic function definitions; I think it is the key to the type system, classes, and most of the other neat language features. At this point, I am still struggling with category theory, although I have been able to make use of monads reasonably elegantly (in my (humble) opinion, of course). I think there is another step there, although I haven't made it.
This is all rather fuzzy and exceptionally difficult to put into words. However, I am willing to change my traditional definition, Programming is applied formal logic, to include at least abstract algebra and category theory at this point, though.
