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.
2 comments:
Have you seen typed racket? The idea of writing your programs with dynamic typing first then typing them is appealing for a Lisper, I think. Curious about your take on that.
Hey Luís: I've been using Racket recently for pedagogical reasons, and have used Typed Clojure (very closely based on Typed Racket, if much less mature) a bit.
My initial concerns, admittedly not well informed, are that its sense of parametric polymorphism is weakened to the point that many useful free theorems cannot be derived, and the (for me) essential feature of higher-kinded types seems to be absent.
Supposing you're working with Lisp, though, it seems to be greatly superior to writing many varieties of tests. I've had trouble writing Python recently for the lack of rigor in simply checking that my changes are sound, and Typed Racket looks like a great improvement in the situation. Of course, how many tests are satisfied depends on how many free theorems you can generate. I hope to have a better idea in the future.
Post a Comment