| I find this entire discussion to be indicative of a deeper disconnect within "programming culture" [insofar as such a thing exists]. Broadly, it seems to me there are are (a) folks who value mathematics and the ability to reason about programs using mathematics, and (b) folks who do not see the value of being able to reason about programs. I personally fall into the (a) camp, since I work on compilers and formal verification. Monads are mathematically useful when trying to define the semantics of a programming language. This mathematical usefulness translates into useful API design [which I personally see as the hallmark of all functional programming techniques]. On the other hand, if one does not care about or want to abstract over a very generic notion of a side-effect, yes, monads are useless. You can go your entire life without needing to know what one is. And that's okay. Why does side (a) side feel the need to pressure side (b) into learning all of their mathematical tools? Why does side (b) see side (a) as "being difficult" or "being obtuse on purpose"? As far as I can tell, the two groups do not even share the same axioms about how we should build and reason about programs. Monads are a red herring. - Real world example of where monads are used to reason about programs: Inside the VE-LLVM codebase, which provides a formal model of LLVM in Coq to prove certain properties of certain algorithms used with LLVM corred, a monad is used: https://github.com/vellvm/vellvm-legacy/blob/e4c22d795974ba7.... Much of the reasoning around sequential side-effecting semantics is phrased in this language. |
From our side of the fence, FP concepts appear dense and obtuse the way they're currently explained. Until that changes, we'll remain divided.