Summary
My thoughts on the battle between dynamic languages and those with Turing complete type systems after attending StrangeLoop.

I had the pleasure of attending StrageLoop 2011 this week. One theme that seemed to keep coming up was that of type systems. I had a fascinating hallway conversation with Daniel Spiewak about the Turing-completeness of Scala's type system; he argued that while this had not been intentional, it is actually inevitable that any sufficiently developed type system will be Turing-complete. Andrey Breslav's talk on The Kotlin Programming Language (slides in pdf) was interesting; Kotlin seems to be heading in the same direction as Scala, but is willing to sacrifice some of the more esoteric type system features in the interest of keeping things manageable. Andrey mentioned that one goal for Kotlin is to keep the type system from becoming Turing Complete. As much as I love Scala, I have to concede that this may be a wise choice.

Gerald Sussman gave a great talk with many themes; one of them was that we should stop trying to think in terms of provable correctness; it's just too hard. Finally, Rich Hickey finished off with a wonderful presentation that discussed the nature of complexity in Software Development. One point that Rich stressed in his talk was that static type checking and unit tests are often viewed as "guard rails", and he observed that relying on these to ensure correctness is akin to driving randomly along, careening off the sides of the road in hopes of reaching one's destination. Moreover, he pointed out that guide rails do nothing to help you plan your trip; actual planning is required.

All of this has had me pondering the cost and value of static typing. I've long been a proponent of it, and not strictly for theoretical reasons. I once had the misfortune of maintaining a website with its front end written in Perl. The lack of static typing made it much more difficult to understand what was going on; it also lead to what one StrangeLoop speaker referred to as "Typo Oriented Programming" - it was far too easy for a misspelled method or class name to make it into production on a rarely accessed code branch. Nowadays, I program mostly in Java. I cannot honestly say that I rely much on static typing to prevent errors per se, but I do rely on it to help me understand the structure of my code. Being able to find all references to a given type or method in a code base has many uses, ranging from aiding in discovery of how a system is structured to understanding the impact of a change under consideration.

At the same time, static typing can have definite drawbacks. I've at times had to jump through some hoops to maintain type safety, and I have many hours of discussions with colleagues about how one could possibly avoid having to make a single cast in a particular situation. Using functional programming techniques, the issue can become more challenging, especially when writing library code. While in theory, the "average" developer will not need to worry about these issues, it seems that in practice, static typing tends to be a leaky abstraction.

I think the right approach might be to avoid the extremes. At a minimum, I think a language should require explicit declaration of user-defined symbols (class names, method names, etc), and helpfully fail when a user attempts to use an undeclared symbol; this can help to keep Typo Oriented Programming in check. More complex type systems allow for additional expressiveness, which in turn can be used to provide additional insights into the code. At the same time, an excessive focus on static typing can start to yield diminishing returns with ever increasing complexity costs. While using a type system as guard rails might be misguided, using it as a set of street signs can be quite helpful.

This approach, to use static typing, but only to a point, has an unsatisfying element of impurity to it. It lacks both the simplicity of systems which avoid typing, as well as the mathematical elegance that complex type systems can provide. It requires that we make trade-offs, in some cases accepting a bit of extra effort to satisfy the type system, and in other cases choosing to let the type system complain, under the presumption that the work to "fix" the problem would be greater than any additional benefit that fix would likely yield. But while part of our craft involves seeking the most elegant solutions available, another part is steeped in the art of compromise.

Talk Back!

Have an opinion? Readers have already posted 13 comments about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Ian Robertson adds a new entry to his weblog, subscribe to his RSS feed.

Digg | del.icio.us | Reddit

About the Blogger

Ian Robertson is an application architect at Verisk Health. He is interested in finding concise means of expression in Java without sacrificing type safety. He contributes to various open source projects, including jamon and pojomatic.