Defense of Static Typing

This article is a defense of static type checking.

In this platform a few days ago an article appeared about the alleged pain of static type checking by Sarah Groff. She hates static typing and she is not alone. I estimate that about half of current programming work is done without static type checking : python, javascript, ruby, php, groovy, bash, ... are everywhere. Even the biggest software companies, who could afford to replace these technologies build on them. I think this is a big mistake by them, programming work is much less efficient [as in money] and much less fun and more frustration without static typing.

In this article i walk through Sarah's reasons of not liking static typing and refute them.

"All static, dependently-typed systems will rule out or be incapable of expressing some perfectly good, error-free programs."

True. But one can opt out from the constraint of static typing. All practical languages allow that. For example with unsafe type cast. Very cheap to do. One does not have to safe-guard all properties of the program by static typing. One can use static typing for properties that it can conveniently check and opt out from it when it gets into way. Most of a program is conveniently typeable. Thus one gets the benefits of static typing for most of the programming work and still is able to implement anything.

"In particular, adding in something like Typescript has interfered with some dynamic solutions we’ve come up with at work — code that was idiomatic JavaScript, but would have required a dynamic type generation. While this was solvable with effort, the necessity of the effort itself"

One should not need dynamic type generation to fit static typing on a program. Static typing requires static types only.

Static typing allows the representation and usage of the same dynamic object model as dynamically checked languages use : objects as dictionaries with symbol keys. One can pack such functionality into a library. All additional effort compared to a genuinely dynamically typed language is the necessity to type "" around those symbols.

"Not only is there the extra time spent understanding and implementing system-compliant types"

Matching of types is a requirement that is not created by static type checking. One has to ensure that in a dynamically checked program too.

"inference remains Not Great"

Inference is more than great, it is incredible. A type system named Hindley-Milner [a restriction of System Fw] provides full inference ability. Full. The algorithm is not even difficult to implement. It can infer everything. Everything. Not one type annotation is necessary. Noone does that though because the convenience of static types is so strong that it is appearant to everyone among the users of this type inference system. Almost everyone type-annotates at least the top level definitions.

In the same time Hindley-Milner is significantly more strong than for example Java's type system.

Such type system was used by Standard-ML and Haskell-98 if i know correctly.

Some more advanced types [much of the new typing capability of Haskell beyond the 98 standard] cause difficulty for inference. But one can decide to not use those types and when used, they will not prevent inference for those parts of the program that do not use them. The Haskell users are very excited about the new typing techniques with less inference capability. They do not care much about the poorness of the inference and look forward for dependent types :-).

"you still need good tests to check for logic and integration issues among other things"

Static typing does not intend to make all the tests unnecessary. But it manages to make much of them unnecessary. Static typing is a method to check a property of a program. It is not the best method for all the properties. For some properties tests may still be better. But for much of the properties : static typing is perfect and costless. The wiseness in it is to apply the simplicity, convenience of static typing for the properties that it is good for and leave the application of the much more expensive testing only for the properties for which static typing is awkward.

"List a -> Int -> List a -- is not a actually documentation"

Rather : it is not total documentation. It is some documentation. Even this type tells some information.

In some cases the type alone tells everything about the function. For example :

(x, y) -> (y, x) Can you guess what a function with this type does? Yes. Why? Because only one possibility exists. It swaps the components of the pair.

(x -> y) -> (y -> z) -> (x -> z) Can you guess what a function with this type does? Yes. Why? Because only one possibility exists. It composes the 2 input functions.

The constrain is caused by parametricity. In these example cases parametricity contrains the functions totally. Not only promise in comment is replaced by guarantee, but the implementation can not contain any bug either [for example it can not compose the input functions in opposite order than what the type suggests].

But in many cases parametricity constrains only partially. However partial is still valuable.

Bare types and parametricity guarantee some properties of the program, while comments only promise properties, and can contain mistake or not exist.

For the properties they can not check : comment documentation is available the same way as in languages without static typing. Again : static typing does not intend to replace all the comments, but it manages to replace much of them, which is a big advantage.

"However, because of the nature of compilers and code parsing, compilers often locate an error some distance from the code we have to change to fix it. An interpreter or a just-in-time compiler, by contrast, usually breaks closer to the issue."

The opposite is true. For example : sort :: Ordered x => List x -> List x If one invokes this function on a value of type (List (y -> y)) then will get error pointing to the location of the call, exactly where the error is. In dynamic type checking the problem is signaled from inside the sorting algorithm, where it tries to compare to member of the list [functions in this example] for the first time.

"Because I’m used to dynamic runtimes, I tend to code by writing small bit then running it to be sure it’ll work — often in a REPL (which in JavaScript is just your browser console). This is not consonant with the type-driven approach of top-down design and implementation, typing big blocks of code until they compile."

Many good statically typed languages provide REPL. In fact i can not think about one that does not.

In some statically typed languages a culture exists to write huge functions, which i also think is unhealthy. This problem is caused not by static typing, but by side effects. In functional statically typed programming functions tend to be small. This is also true for types : a good static type-system makes it possible to glue together a complex typing solution from simple pieces.

"developing with tiny iterations is actually better"

Static typing not only allows iterating in tiny steps, but it makes it much easier, because it makes refactoring much easier.

"side effects and imperfection are not enemies to be avoided: they are the whole thing"

This is a somewhat different topic. Functional and static typing are orthogonal aspects of programming. In theory. But in practice they correlate. The reason is that they are both instances of a more general paradigm : correct by construction as opposed to correct by testing.

The purpose of any program is some side effect. But that does not make side effects necessary in the semantics of the program. It is enough if the programmer can express effects. In functional programming effects are computed by functions, not performed. With other words : functional programming permits effects, they just happen not to the side. The "to the side" nature of effects that functional programming saves us from, and that makes programming a different, much better world. This topic is too big for this article, so i rather ask you to read my older writing about it from my website.

"I would argue that working in this small, iterative, accretionist way is how you write programs that are flexible, understood, and easy to change as your requirements change."

Side effects introduce dependencies. Thus they make functions big and, interdependent. They are exactly the opposite of "small", "iterative", "flexible", "understood", "easy to change".

"The problems that flow from such an approach are less likely to be type errors than to be logic errors — and a type system can’t help you with that."

The type system of Haskell prevents side effects and thus all possible errors that those could cause. By the way : practically : typing and logic are the same thing.

"For not only is the pursuit of a systematic perfection unrealistic in terms of what we want to accomplish in the world but it is a goal that is bad for people. While I think that only zombie Freud can truly explain the programmer fetish for correctness, it is pretty easy to argue that putting the idea of perfection at the core of computing underlies some of our less-humane effects."

Again : static typing is not a fetish of correctness, it is economical and fun. It does not try to prevent all bugs [which is impossible even theoretically]. Just much of them.

"Shouldn’t we make sites that are more reliable for our users even if it is at the expense of your personal dev experience? After all, that’s what the money’s for."

Again : static typing and functional programming are several times more economical. Bugs cost a lot of money. Allegedly : ones Bill Gates said that half of Microsoft's engineers are testing. And that cost is part only of production. Bugs cause economical cost on the user side too. Later corrections of software is much more expensive then before release. Lack of modifiability, ability to refactor, self-documentation, the abundance of unnecessary dependencies, the necessity to write unit tests to test even the most trivial properties of the program - are very expensive.

Additionally : static typing gives much increase in runtime efficiency and ease of program code editing.