The limits of type theory: computation vs. interaction

[0; 'a'; fun x -> x + 1];;

The common type is object, or perhaps more specifically, non-nil object (object!), if 0 is not treated as nil (value type).

If you try to interact with an object (add it to a number, call a method, etc.), your language has to decide what to do: fail because that method is not part of the type object, or force people to cast to the proper sub-type, or allow a kind of dependent typing/casting (if type(it)=int: it+1 else if type=char: it.uppercase), or (like boo, python, ruby, etc.) allow "duck typing": allow any calls/methods on the object, and check it at run-time instead of compile-time

I guess he would downvote me? I don't get HN any more...

The question of computation vs. interaction is an fascinating one, but I think there's another question (perhaps related) to the applicability of "rich" types to practical programming, and that is regarding the role of types, and how far they should be stretched. I think there is little question that "simple" type systems (like in C/C++/Java/C#) aid in developing large systems. But much of the fascination with type theory (as the article states) has to do with the Curry-Howard isomorphism, and the ability of programs to carry proofs to some of their properties. This is believed to be a powerful tool in software verification. The question then becomes to what extent should this tool be used? What properties can be proven? What properties programmers are willing to try and prove? How much harder is it to prove a property than write a possibly-incorrect algorithm without proof?

The benefit of proofs in code would only be worthwhile if it was relatively easy for common programmers to prove the absence of bugs that would have been more costly to find and fix using other methods, and that that ease would not come at the cost of other properties (such as performance). So far I have a feeling that this is not being delivered. Your run-of-the-mill clever use of types usually prevents very "cheap" bugs, and hard bugs are even harder to prevent with types.

I'll give a concrete and recent real-world example. A few months ago, a bug was discovered in Python's and Java's sequential sorting algorithm[1], Timsort. It was introduced to Python in 2002, and its adoption by Java in 2011 has probably made it the most used sorting algorithm in the world. Yet, it contained a fatal bug that could cause it to crash by overflowing an array. There are a few interesting observations one could make about the bug and its discovery with relation to type systems.

1. The bug was discovered by a verification program that does not rely on type-based proofs in the code. The output from the verification system quickly showed where the bug actually was. AFAIK, the verification program required no assistance with proving the correctness of the algorithm, only that the variants the algorithm seeks to maintain be stated.

2. Proving the invariants required by the (rather complicated) algorithm with types would have required dependent types, and would have probably been a lot harder than using the verification program used. It is also unclear (to me) whether the problem and the fix would have been so immediately apparent.

3. The interaction of "type-proofs" with program semantics (namely, the requirement of referential transparency) would have made the type-proven algorithm much slower, and this particular algorithm was chosen just for its speed.

4. The corrected version ended up not being used because it could have adversely affected performance, and it was noticed that the "incorrect" algorithm with a slightly larger internal array would still always produce correct results for the input sizes currently supported in Java.

This example of a purely computational real-world bug shows some more limitations of the type-system approach to verification, I think.

Going back to effects and interactions, pure-FP approaches have a hard time dealing with timing properties. I already gave the same example on another discussion today, but the Esterel language (and languages influenced by it) has been used successfully to write 100% verifiable programs for safety-critical domains in the industry for a long time now. It is an imperative language (though it's not Turing complete) with side effects and a lot of interactions, yet it has a verifier that uses Pnueli's temporal logic to guarantee behavior, without requiring the programmer to supply proofs.

To summarize, type systems have shown their usefulness in reducing the cost of software development, but they need to be considered as a component in a larger verification space, and they need to strike a balance between usefulness and ease of use.

[1]: http://www.envisage-project.eu/proving-android-java-and-pyth...

[2]: http://www.envisage-project.eu/key-deductive-verification-of...

I didn't downvote you, but here oneliners are discouraged and often downvoted. They are usually very difficult to understand without too much context. For example, I don't know who is Conor McBride ( http://en.wikipedia.org/wiki/Conor_McBride )!

Try to expand the comment. Something like: "Conor McBride has a article that agree/disagree with this [link] because [two or three line explanation]."