Friday, March 9, 2012

More on static typing

As I've said earlier, I find static typing aesthetically appealing but am skeptical about its practical value.

Type systems are the chemo of programming. They are designed to make things harder. You hope that most of what it does is make mistakes harder, but you know from experience that static typing introduces a grain of trickiness into everything.

What do people find so appealing about dynamic languages?:

You know, maybe the dynamic crowd just wants freedom to not have to think as carefully about what they're doing. The software might not be correct or robust, but maybe it doesn't have to be.

-- Apocalisp

The whole answer is very good, but the author has a fundamental misconception: that the only cases where a dynamic language admits a program that a static language rejects is when the program is incorrect. Consider that the following python code is perfectly correct:

a = [ ]
for i in range(0, 8, 2):
    for j in range(i): a.append('x')


total = 0
i = 0
while i**2 < len(a):
    total += a[i**2]
    i += 1

but that it would not pass a static type checker. You could of course struggle a long time to prove via the type system that the while loop accesses only those elements of a that happen to be numbers (you could probably do it, but it would be a long and painful journey). But more importantly, even if you don't do it, the code is still correct.

The difficulty of static type systems is not that they require your code to be more correct, but that they require you demonstrate its correctness in a certain way. That certain way is a pretty elegant one, but it is also a terribly specific one, and so there will always be correct code to which a static type system is poorly suited.

Unit testing statically typed functional code

Unit tests do introduce redundancy, which means that when requirements change, the code implementing them and the tests covering this code must both be changed. [...] given how statically typed functional programming covers a lot of the ground unit tests are intended for, it feels like it's a constant overhead one can simply reduce without penalty.

-- back2dos

Some of the bug-finding power of static typing comes from redundancy; in fact, if you want to catch inadvertant changes in behavior introduced by refactoring, you will need to specify explicit type signatures, which are redundant.

I wonder, are there any statically typed programming languages which provide tools to check whether the inferred type of a function changes across different versions of the code?

If you have specs which can be mapped directly to function declarations - fine. But typically those are two completely different levels of abstractions.

-- Doc Brown

Of course, in theory all levels of abstraction can be checked statically; but how many people are leet enough to actually do that? (Consider -- what would you need to do to write a statically verified sorting function). If unit tests can take you to 97% sure that your code is correct (and still correct after a refactoring), how much time are you willing to spend on that extra 3%?

No comments:

Post a Comment