On Giving Things Up, pt 2

Yesterday’s post was supposed to be about a general principle, rather than a particular example — I got a bit carried away. That principle is: there are a lot of decisions being made in modern programming language theory that feel like sacrifices, like giving things up. But they’re not, really. They’re gaining things — additional structure — and in almost every case, whatever you wanted to do would have fit into the structure already.

Example: static typing
I hope I don’t get carried away again, but let’s try one more example before we continue about the general principle. A lot of people really like dynamically typed languages as opposed to statically typed languages. I used to feel like this too. Type systems like Java’s and C’s felt incredibly restrictive to me — why couldn’t I just do it in Python, where I write a function once and it automatically works on any value?

Except, of course, it doesn’t automatically work on any value. When you write something like

  def double_and_subtract_one(x):
      return x*2 - 1

you are expecting x to be a number. Sure, you can pass it a dictionary if you define a subclass of dict with an __lmult__ method that returns a number, or whatever, but it’s not what you’re expecting. You, the programmer, have specific ideas about the types1 of most of your variables, even if Python doesn’t.

If I may be so bold: I don’t think you’ve ever wanted or will ever want to write code that couldn’t, in principle, pass a sufficiently smart type checker. You don’t want to write code where it’s impossible to say that you won’t ever subtract an object from a string, or call a method on an object that doesn’t have one. Maybe there are no modern typecheckers smart enough2 to have the same ideas as you do about how your code works, and in that case I would agree that no existing statically typed language is suitable for you. But nothing you want is inherently opposed to the idea of type analysis itself.

Okay, back to the general principle: you can “give up” these “freedoms”, and often it will turn out that you never would have used these freedoms anyway. But why would you want to do this? Isn’t it still better to have more freedom, just in case?

Well… it’s not that simple. You can look at it as losing freedom, but as I touched on in the opening paragraph, you can also think of it as gaining structure or knowledge. And this means that if you keep those freedoms (which, again, you were probably never ever going to use), you give up structure that you and the compiler could use to write better, safer code.

Type systems are a bit polarized for an example, so let’s return to the previous subject of termination checking. You can either allow general recursion and potentially shoot yourself in the foot, or you can have a termination checker and restrict yourself a tiny bit.

What do you lose if you go with a termination checker? The ability to write a very small class of bizarre3 programs — those that cannot be proven not to loop forever without doing useful work. Even if you’re writing an operating system you don’t want to do this — you don’t want to forever get stuck incrementing a single counter because you missed a loop boundary condition, you want to loop forever doing the bookkeeping required to run an operating system.

What do you gain? Well, it’s not the ability to write programs that do useful work — you can write those in a language with general recursion. What you gain is help from the compiler. Without a termination checker, you have to step through your code manually before you can understand whether it’s going to run the way you want it — keeping track along the way of every possible state transition, every combination of variable values at any point. The freedom to write malformed programs comes with an exacting obligation to ensure that you’re not writing malformed programs. Accept a termination checker, and this requirement is lifted — leaving you with more time to attend to the interesting, application-specific logic of your program.

Freedom and the Turing tarpit are two sides of the same coin. All human applications are built of structure.

  1. If you’re a fan of duck typing, maybe you have ideas about interfaces, rather than particular types. But a lot of statically-typed languages support interfaces too — tracking the interfaces supported by a particular variable is not really much different from tracking the types. 
  2. But if you haven’t looked at Haskell or OCaml or another language of that family, please don’t conclude this until you have. Haskell is an entirely different world than C or Java. 
  3. Actually, what termination checkers lock you out of is a bit more worrying than my previous post suggests. Since I wrote that post, I have learned the following theorem: a language whose programs always terminate is unable to express certain always-terminating programs (unsurprising), including (gasp) the interpreter for that language itself. I certainly didn’t expect this and I will admit it makes me uneasy. Nevertheless, it seems more like the same kind of thing as the famous “no system can represent itself” result from Goedel, rather than “this system is unexpectedly weak”, so I think my point still stands. 

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s