I find it interesting that he's now advocating monads considering his earlier stance on static type systems[0].
Of course it may just be that he's changed his mind -- it happens.
(Yes, I consider monads as fundamentally requiring a static type system, at least if you're using monad transformers or similar advanced techniques. In practice you're not going to be able to get things right without compiler assistance when you have a stack of N monad transformers.)
I also find the bit on having a "pure" annotation vs. having explicit monads particularly insightful. The difference between a type system that only handles "pure/impure" vs. a type system that handles "pure/state-effect/writer-effect/network-effect/etc." is huge.
If "in practice, you're not going to be able to get things right..." than what the hell? That just strikes me as crazy.
Note that I am not necessarily against monads. However, this idea that they are both a good answer and require fairly extensive programmatic help seem counter.
I realize we can never reduce programs to things which are trivial and easy to comprehend. However, any new paradigm/trick that will always require compiler assistance doesn't sound like a step forward.
(Of course, in my mind a step forward are tools that don't necessarily need you to change your current languages and programs. Which is one of the things that annoys me with many new languages. Seems we always get a new wave of effectively solved areas of programming with incomplete solutions that are "cool" because they are in the new language.)
I'm not sure how that even follows from what I wrote.
Note, I am all for extensive static analysis. To the point that I am excited about such tools as Coverity and friends.
I am beginning to take exception to requiring ever more from the programmer. To the point that a programmer can't "in practice" specify a program correctly without a type checker. (Which... is what the parent post says. Right?)
I would much rather have it such that "in practice" we can specify programs without help. Since that implies that we can "in practice" read and reason about programs without extensive help, as well.
Sorry, didn't mean "compiler assistance", I meant "programmatic assistance" (as in your original reply). I hope my post makes more sense with that change!
So, it sounds like my post is still the more nonsensical. I'm not against any programmatic assistance. I am growing weary of the ones that require rather large stretches from the programmer to show dividends.
So, I would rather have a static analysis tool let me know that I am using data straight from the user, than I would generate a rather large type system that includes this. See GWT and the "SafeHtml" joy for an example of what sucks in programming.
Now, it can easily be argued that the problem there was Java not being quite strong enough, but even in languages like Scala, things can be difficult.
Of course, I have grown to love the Lisp world where people have pretty much agreed to write in the S expressions. Not because they are the most readable form, but because they really are ascii art of the structure of what you are trying to say.
So, yeah, I'm a jumble of conflicting feelings on this. :)
I find it interesting that he's now advocating monads considering his earlier stance on static type systems[0]. Of course it may just be that he's changed his mind -- it happens.
(Yes, I consider monads as fundamentally requiring a static type system, at least if you're using monad transformers or similar advanced techniques. In practice you're not going to be able to get things right without compiler assistance when you have a stack of N monad transformers.)
I also find the bit on having a "pure" annotation vs. having explicit monads particularly insightful. The difference between a type system that only handles "pure/impure" vs. a type system that handles "pure/state-effect/writer-effect/network-effect/etc." is huge.
[0] http://lambda-the-ultimate.org/node/1311