My point is that you need to understand Monads to use Haskell/Lean/Idris/Coq for anything practical. Because those languages are pure. You don’t have to understand monads to use non-functional languages. In the same way that you don’t have to understand Category Theory to use Haskell. So when I say you don’t use monads in non-functional languages that is exactly what I mean. In the same way that you don’t use Turing Machines in any programming language even though it “is” a Turing Machine underneath.
It's a fallacy that one has to understand monads to be able to use them. I don't have to understand a car to be able to drive it. I have to know what the pedals do, what the steering wheel does, and practise to develop my intuition. Same with monads. I need to know what do notation does, what some basic operations do, and then I need practice to develop my intuition.
I disagree. If you don’t understand Monads then you loose a lot of opportunities to write clean elegant code in pure functional languages. I wrote my own Monads all the time in Haskell. However if you are not using a pure language then I agree.
I think a lot of it depends on what you mean by "understanding Monads". If "understanding Monads" means knowing where they fit in category theory (not simply where they fit in the Haskell typeclass hierarchy) that is absolutely not necessary to be productive in Haskell - I've worked with effective, professional Haskell programmers who have no idea what adjunction is.
Understanding how things fit together behind the interface well enough to implement it isn't a high bar and (as you say) has a pretty high payoff as you work on slightly larger projects.
