[shrimpx]

One guy Eugenio Moggi saw that the category theoretical "monad" could formalize "imperative programming" in pure functional languages by carrying a "world" parameter that represents the state being modified. Since then people have been trying hard to jam the rest of category theory into programming hoping to uncover similarly striking results, to no avail.

[curryhoward]

> by carrying a "world" parameter that represents the state being modified

From this, it's clear you've never read and understood Moggi's seminal paper. Monads are functors with some extra monoidal structure. The concept, and even Moggi's use of it in categorical semantics, has nothing to do with "worlds".

The important realization is that there are many more monads than just the one hardcoded into one's programming language of choice. State, error handling, parsing, reading from an environment, backtracking, nondeterminism, mutable state, logging, probability, continuations, async/await, I/O, ...these are all just specific instantiations of the general interface of monads. Recognizing that allows you to build abstractions that work for any monad, rather than re-discovering and re-implementing the same idea for each one separately. It's been a remarkably fruitful area of research.

[shrimpx]

Sorry for saying "world" and for underrepresenting Moggi's paper, but all those things you're mentioning are side effects and are captured by the same concept, of representing effects by carrying a parameter through a chain of function calls.

I'm not backing down from the core claim that Moggi realised that CT monads are a nice formalization of side effects in pure functional programming, and that this caused a flurry of interest in "what else" of high impact/interest CT can explain of programming, and that there isn't much else.

[curryhoward]

> all those things you're mentioning are side effects and are captured by the same concept, of representing effects by carrying a parameter through a chain of function calls

No. The state and environment monads fall under that rubric, but many of the others are far removed from what you're describing. You can't implement backtracking in a purely functional way simply by passing around an extra parameter, because backtracking affects the control flow. Continuations are even stranger—they're not even algebraic!

> I'm not backing down from the core claim that Moggi realised that CT monads are a nice formalization of side effects in pure functional programming

No, Moggi's paper was about formalizing the semantics of impure programming languages. It wasn't until Wadler that we started using monads to model side effects in pure functional programming. Please read the actual research before citing it.

[Dontrememberit]

What about optics?

[LessDmesg]

Monads are still programmable semi-colons, though. Yes, there are a lot of things you can program into a line-end symbol. Yes, some of those things are general and work for any already modded semi-colon. But it's still just programmable semi-colons: implicit, uncomposable, and frankly better left alone.

[jolux]

>implicit

You'll have to elucidate, I don't follow.

>uncomposable

Demonstrably false, see monad transformers.

>better left alone.

"Yeah, well, that's just, like, your opinion."

[patrec]

Monad transformers are really not the great counterexample you seem to think they are.

[jolux]

Monads were described as uncomposable. Monad transformers are one way they’re composed. I don’t understand your objection.

[patrec]

A lot of people consider Monad transformers as an ugly hack to partially paper of the lack of compositionality of Monads (hence alternative attempts like extensible effects). Something that composes nicely has low overhead, does not introduce additional boilerplate or require making arbitrary additional choices (such as ordering). But Monad transformers do often involve non-trivial overhead, additional boilerplate (not sure how much things have progressed since mtl) and extraneous complexity.

[louthy]

> Monads are still programmable semi-colons, though

No, they’re not. That’s just an analogy that’s sometimes useful when describing them to imperative programmers to aid intuition.