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