A few years ago, I didn't care about functional programming. A year ago, it would have been unthinkable for me to work with a bunch of type system fanatics. I've been a Lisper for a long time, very much disliking anything breaking the Lisp mold, and it was just a little over a year ago that I learned, and came to appreciate, Haskell and the advantages it provides.
This is how I perceive the modern world of typeful programming, as a programmer who most naturally thinks in Lisp, with some experience in that area and a relatively newfound appreciation for it.
I won't discuss the benefits of immutable, persistent data structures, except where it naturally comes up in discussion of types. Clojure demonstrates that you don't need fancy type systems to get many of the advantages of immutable data. Were I to take on a large project in Common Lisp now, I would certainly try to use Funds or some implementation of Okasaki's data structures wherever beneficial, but I don't care to discuss that.
I will be similarly mute on the benefits of Haskell-flavored normal-order evaluation, for similar reasons. They will come up more often in relation to type systems, though.
I've broken up the discussion into simple assertions and discussion of them. You won't find rigorous logical backing of my statements, merely the empirical and anecdotal, because the former has already been done quite well elsewhere, and won't be as fun for me.
Here I keep links to articles already posted. The unlinked articles have been written, but not posted yet, for the sake of cadence.
- Type systems prove things about your programs.
- Optimization is just a side benefit.
- Type systems help with “a class of errors”: factual, but not true.
- C and Java do not have good type systems.
- With a type system, whether you can write a program depends on whether you can prove its correctness.
- “Inference” is “proof assistance”.
- Some type systems are much better than others.
- More type system features can make proofs harder to write.