[pron]

> Well, the problem in Haskell is that it's a language of evaluating expressions at heart: executing effects makes no sense any more than it would in arithmetic.

You know what else doesn't make sense in arithmetic? Computation. I think it is important to wonder how come mathematical definitions of computation didn't come about until the 20th century[1] even though math has had most of its big breakthroughs (to date) by then (or, at least, there was no revolution in mathematics in the 20th century on the same scale as there was in physics). And yet, as advanced as math was, computation was only defined very late in the game. The reason is that, perhaps ironically, the concept of computation is absent from most of math, which is "equational".

But computation is the very core of computer science. So, for example, in arithmetic, 4 and 2+2 are the same thing because 4 = 2 + 2. So in arithmetic, equality means "sameness". But in computer science they are most certainly not the same, because the process of moving from one of the representation to the other is precisely what a computation does. Not only that, the process isn't even necessarily symmetrical, as moving in one direction may entail a much higher computational complexity than going in the other direction.

Any distinction between calculations and effect (other than actual IO) is, therefore, arbitrary. Whether or not the particular distinctions Haskell makes (where waiting for one second may or may not be an effect depending on how it is implemented) in the form Haskell makes it -- using pure functions and equational reasoning and describing effects with monads -- is actually useful and beneficial is a question for psychologists. Given Haskell's design, monads are certainly useful in Haskell, but that utility can't be generalized to languages with other designs.

[1]: https://en.wikipedia.org/wiki/Computability_theory

[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.

[pron]

I will add that in general, there is an inherent mismatch between "equational" math and computation, and there have been various approaches to bring the two closer, e.g. Hoare Logic, various process calculi and temporal logic (my personal favorite). Haskell's approach is basically using lambda calculus[1] to unify some computations such as 2+2=4 with 2+2 -computes-> 4 [2](Prolog goes one step further and unifies 2+2=4 with both 2+2 -computes-> 4 and 4 -computes-> 2+2, as equality is a kind of relation and Prolog is relational) and other computations as monads wrapping various "unsafe" operations[3]. It works, and it's quite elegant if LC as the one true expression of computation is your cup of tea. I think it's clear why this approach can be a fine design choice, but it's also clear why it can be not so fine. Personally I think that design doesn't sit too well with most programmers as a cognitive abstraction.

So the answer to "why are monads useful?" is that if for whatever reason (e.g. it makes programming easier for you) you decide to model computation as Haskell does, as LC and "equational reasoning", monads are invaluable as an elegant description of various computations that wouldn't otherwise be convenient to express. Once you use other approaches, monads (as a cognitive abstraction) quickly lose their usefulness and appeal.

[1]: Which is one common definition of computation and one of the "original three" definitions, but not a very good or powerful description of computation as it lacks good measures of complexity (it also lacks introspection which makes it less powerful than the Universal Turing Machine, but that is no a very common capability in programming languages other than Lisp).

[2]: In fact, "computational math" doesn't care in the least that 2+2 equals 4. All it cares about is the computation 2+2 -computes-> 4 (or 4 -computes-> 2+2, the latter is completely separate from and unrelated to the former). It is those various approaches of verifying computation that care about the relationship between 2+2=4 and 2+2 -computes-> 4, but those can (and should?) be completely separate from the programming language.

[3]: That split between some computations and others is exactly why a `sleep` operation in Haskell can be implemented to either be "effectful" (using monads) or "pure" (using only "pure" computation). That artificial distinction doesn't really have a rigorous definition in computation theory; rather, the definition of "pure" is a language-level design choice. For example, in Koka a divergent computation (i.e. infinite sleep) is an effect, but not a finite sleep; in Haskell, neither is an effect. In both Haskell and Koka, a stack overflow is not an effect and neither is memory allocation. OTOH, in Haskell spawning a new thread is considered an effect (which seems really weird to me). I hope that at this point it is clear that the distinction between "pure" and effect is arbitrary and not a fundamental concept of computation (aside, perhaps, from IO).