|
Pure functions are beautiful, useful and desirable, yet I believe, like the post's author, that a language that tries to enforce referential transparency everywhere is misguided, in that it places too big a burden on programming while doing little to prevent bugs that really matter. Not all bugs are created equal -- some are easier to introduce and/or harder to find than others. A language that chooses to reduce bugs by placing non-trivial constraints on the developer -- i.e. by increasing the mental burden -- would do well to concentrate efforts on those bugs that cost more. IMO, Haskell does the exact opposite, nearly eliminating data-transformation bugs -- that are very easily found -- and doing little (though not nothing) to reduce effect-related bugs. Pure functional programming carries other burdens, too, some stemming from its conceptual roots in lambda calculus, like the lack of a clear complexity model. I also reject the conclusion that if most costly bugs are related to effects, our best course of action is getting rid of them altogether (or relegating them to an opaque runtime). This solution seems strange, as side-effects -- in spite of their name -- are the most central component of useful programs. Effects are the things we program (unless we're writing a compiler). This solution seems to me like suggesting to a programmer that since typing is the cause of wrist pain, she should type with her tongue. There are better solutions already. Clojure's approach to memory effects is at least as effective as Haskell's in preventing certain types of bugs, yet the language places a much lower mental burden on the programmer. Lastly, I think PFP has (unintentionally) caused many to believe it is the only approach to a more "mathematical" mode of programming, and the best course for formal software verification. Neither could be farther from the truth. Haskell could not have prevented the bug discovered in Java's (originally Python's) efficient sorting algorithms -- probably the most used sorting code in the world today -- a few months ago, and it would have been very hard to detect it even in Idris (if the algorithm is expressible at all in that language). Instead, it was discovered with a software verifier for imperative languages. It is true that PFP languages may depend in clever ways on the Curry-Howard correspondence to help (force?) the programmer to prove some properties of her algorithm, but spelling out a partial proof in the code itself is not the only -- or even the best -- way to verify a program. All this is not to say that we haven't learned a great deal from PFP and its approach to software verification. But it is just one approach of many, and one that is particularly intrusive. |