[tel]

Computation in mathematics is well represented in the constructive and intuitionistic camps. It was thoroughly examined in the 1930s via the invention of things like lambda calculus and turing machines. It was also subsequently rejected by most mathematicians not because it fails to be equational but just because they decided that they don't really care.

Including notions of computation makes equational theories hairier. That might be very much what you want, and there are plenty of ways in which mathematics talks about (2 + 2) being unequal to (4). Typically you instead replace equality with weaker notions going all the way down to the weakest (most intricate) examples of actual algorithmic computation.

So why avoid this kind of stuff? Because you want to pick a "cognitive abstraction", in your terms, which is most useful. It turns out that for a lot of purposes inclusion of computation is too hairy and obscures what people care about. It also turns out that in many cases what they care about is somewhat unaffected by the computational substrate involved.

I really can't say I agree that your beef with equational reasoning makes much sense to me, but I think it's just because you're shooting too broadly. You can easily have problems with the particular choice of granularity of equating taken by the Haskell community and language... but that's just a much smaller thing.

[pron]

> It was thoroughly examined in the 1930s

That's what I said. Only in the 20th century for something that might seem to an outsider to be fundamental to mathematics (after all, mathematicians sometimes compute, right?)

> So why avoid this kind of stuff? Because you want to pick a "cognitive abstraction", in your terms, which is most useful.

Oh, absolutely, but there are many ways and many forms of reconciling "equational" mathematics and computational mathematics, and PFP is just one of them. As I've shown in another comment, Prolog takes this much further than Haskell because it's truly equational (or, rather, relational), while Haskell gladly allows a direct (one-way) computation if it defines it as pure, i.e. in Haskell 2+2=>4 is still as different from 4=>2+2 as it is in Java. Other ways are the plain procedural style (which simply lets you name and parameterize a computation), and my favorite (although I don't know how practical), temporal logic used in, e.g. Esterel (and TLA+).

My beef is not with equational reasoning as a concept, and not even with Haskell's flavor of it. Certainly "equationality" in programming languages is a spectrum (as computation is inherently non-equational), and finding useful points on it is a matter for lots of empirical study. My "beef" (if that's what you want to call it) is with the claim that Haskell's particular design is somehow more fundamental or mathematical than other designs, and, to bring us back to the topic of the discussion, that (cognitive) monads are somehow essential. The reality is that there are many (good) justifications for Haskell's design, but they've been made by people to match certain human aesthetics and certain human goals[1] and they don't have any transcendent mathematical justification. They are just a point in the design space. Similarly, monads are only (pretty much) essential in Haskell given its design. Some people try to present Haskell (and monads) as the language (and abstraction) God, nay, better -- Math -- has given us, and that's just wrong. It's just a language like many others, with its own design choices. Besides, everybody knows God uses Lisp. My other "beef" is with the unjustified belief that a certain way of expressing an algorithm is automatically cognitively optimal just by virtue of it being equational (be it either in the Haskell or the Prolog sense).

[1]: One of them is a particular balance between correctness and specification effort, which, again, is also arbitrary and defined by the limitations of HM type inference.

P.S.

To clarify something I wrote in another comment, Haskell's definition of purity, while fundamentally arbitrary (from a computational theory point-of-view), makes a lot of sense if you've chosen that particular design.

[tel]

Ahhh, well if you're taking aim at Haskell somehow being "right" then I'm not going to say a thing. :)

I think as far as monads go I quite like your distinction drawn elsewhere between abstractions for mathematical sake and abstractions for human cognitive sake. I think ultimately it has a lot to do with someone's goals as a programmer and person as to which abstractions they should hold and realize.

I think, personally, monads have a very high power-to-weight ratio here, even outside of Haskell, but I've never been one to argue that one cannot live without them. Or even shouldn't.