Another Non-Argument in Type Systems

[RSS feed]
 

October 25 2012

I find most static vs. dynamic debates to be painful (as I've said before) and, in general, I try to ignore them. However, every so often a new argument is raised which needs consideration. About 18 months ago, Bob Harper asserted that a dynamic language is a straightjacketed static language that affords less rather than more expressiveness. Part of the underlying argument is correct, but it avoids an important part of the story. I've recently seen several restatements of this assertion, so, unfortunately, I feel compelled to write a brief rebuttal explaining why I believe it's yet another non-argument in the ongoing debate about which class of languages is better.

My firm belief is that statically and dynamically typed languages overlap in some ways, but differ in others. Each has tasks they are better suited to, and neither is inherently better than the other. Bob shows in his article one area in which statically typed languages allow things that dynamically typed languages can't; in this article, I'm simply going to point out that this leads to a mirror-image where dynamically typed languages allow things that statically typed languages can't. In that sense, the argument I make here is a restatement of ideas in my dynamically typed languages paper.

Before we can go any further, we need a shared understanding of a concept from statically typed languages such as ML and Haskell (i.e. not Java or its ilk): sum types. Since this concept is unfamiliar to many programmers, I'm going to present a simple definition of the core features; sum types have a lot of extra features (tagging, pattern matching, etc.) that aren't germane to this article's argument. The basic idea is that sum types are a super type that ranges over other types. Whereas in OO languages a sub-class explicitly chooses its super-class(es), sum types (the super class equivalent) choose the types they range over (the subclass equivalent) — the latter have no idea which sum types they are ranged over by. I can therefore take the types T1 and T2 and make a sum type over them S. Whenever my program wants to do anything with a value of static type S, I must then use what I'll call a typecase statement to differentiate whether the dynamic type of the value is actually a T1 or a T2 (readers familiar with the concept will realise that this is intended to be a very simple form of pattern matching). Writing this out in pseudocode can help visualize the important relationships between these concepts:

type T1:
  ...

type T2:
  ...

sumtype S rangesover T1, T2

func f(x : S):
  typecase x:
    whenoftype T1:
      ...
    whenoftype T2:
      ...
As this suggests, typecase acts as a dynamic type check, with the only difference from its cousins in dynamically typed languages being that we are forced to write out all of the possible types the sum type ranges over. We could not, for example, leave off the whenoftype T2 clause in the above example.

With that under our belt, we can now look at Bob's argument. He makes two points which can seem to be separate but which I suggest are really just different ways of looking at a single underlying idea:

  1. Dynamic typing is but a special case of static typing, one that limits, rather than liberates, one that shuts down opportunities, rather than opening up new vistas.
  2. this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice!

Bob points out that, conceptually, a dynamically typed program has a single static sum type ranging over all the other types in the program. We could therefore take a dynamically typed program and perform a conversion to a statically typed equivalent. Although Bob doesn't make it explicit how to do this, we can work out a simple manual method (though it's not clear to me that this would be fully automatable for most real programs). We would first need to see all the points where the program performs operations that use types (perhaps by a sort of type inference; but we'd also need to include dynamic type checks using e.g. isinstance in Python or instanceof in Java). All the types referenced would then be ranged over a single sum type. Whenever a sum type is encountered statically, we would then need to use a typecase to check the dynamic type of the value, and then perform an appropriate action. In this way we can guarantee that our once-dynamically typed program is statically type-safe.

This conceptual argument is quite correct. However, it is then used as the basis for two jumps of logic, both of which I believe to be incorrect. First that this means that dynamic typing is a special case of static typing; and that, because of this, dynamically typed languages only have a single type. I also think that the thought experiment misses the very important factor of whether, if we were to do this for real, the results would be in any way usable. I'll now tackle these points in reverse order.

Usability

Sum types are a powerful theoretical tool; when used judiciously, they can also improve code. Used indiscriminately – particularly where a sum type ranges over an unduly large number of other types – they create an unwieldy mess because of the requirement to check all the types that have been ranged over.

The encoding of dynamically typed languages we used above would lead to a huge increase in the size of programs, since a static type system forces us to explicitly express all the checks that a dynamically typed run-time implicitly performs for us. It would also remove the possibility of making use of a dynamically typed system's ability to execute and run programs which are deliberately not statically type safe (a useful property when comprehending and modifying large systems). I therefore assert that while it's a valid thought experiment, it would be deeply impractical for many real systems which make use of the easy dynamicity offered by dynamically typed languages.

Unitypes and multitypes

Bob rests much of his argument on the notion that his encoding shows that dynamically typed languages only have a single type — that they are, therefore, unityped (as opposed, one presumes, to multityped). As his suggested encoding indirectly shows, dynamically typed languages can indeed be thought of as having a single static type (or, as I often tend to think of things, a static type checker which always returns true). However, they can have an arbitrary number of dynamic types. The fundamental difference between statically and dynamically typed languages isn't over how many types they have: it's about when those types are utilised.

Consider a program which tries to add an int to a string (e.g. "abc" + 123). A statically typed language, depending on its type system, is likely to either reject such a statement as untypeable, or coerce the int to a string at compile-time. A dynamically typed language has exactly the same choices as the statically typed language: it is likely to reject such a statement as untypeable, or coerce the int to a string. The only difference is that the choice of rejection or coercion happens upon every execution at run-time, not once at compile-time.

It therefore makes no sense to say that a language is unityped without qualifying whether that relates to its static or dynamic type system. Python, for example, is statically unityped and dynamically multityped; C is statically multityped and dynamically unityped; and Haskell is statically and dynamically multityped. Although it's a somewhat minor point, one can argue (with a little hand waving) that many assembly languages are both statically and dynamically unityped.

The relative expressiveness of dynamically and statically typed languages

Expressiveness is a word that we in programming languages should be wary of, because, like Humpty Dumpty, we often use it to mean whatever we want it to mean. Bob implicitly equates expressiveness with the ability to state more, stronger, static properties of a program. That's one reasonable interpretation of expressiveness, but it's not the only one — let's call it static expressiveness. If we consider dynamic expressiveness, we can see that expressiveness is a multi-dimensional quality, with no clear winners.

Every static type system designer faces a fundamental choice: should the static type system be sound or complete? If the type system is complete then it will be unsound, letting through some programs that will cause run-time type errors. Conversely, if the type system is sound then (because of the expressivity of programming languages) it will be incomplete, rejecting some programs that will run without type errors at run-time. Nearly all statically typed languages therefore aim to be sound rather than complete [1].

The following program (in pseudo-Python) shows a program which will fail to type check in any sound static type system which I know of:

l = [...]  # A list of non-empty strings
if len(l) > 0:
  l = l[0] # Extract the first string from the list
  print(l) # Print the string
if len(l) <= 0:
  l.sort() # The sort operation is valid on lists but not strings
Sound static type systems will reject such programs as type-unsafe, because a) the l variable changes type (from List(String) on line 1, to string on line 3) b) a later use of the type requires it to be of a specific type (List(*)) on line 6). While this program may not be an example of good design, we can trivially see that this program will never lead to a type error at run-time because of the non-overlapping predicates on the if clauses. We could design a sound type system that will deal with this specific case but, because a sound type-system won't be complete, we can always find another similar run-time correct example which the type system will reject [2].

As this example shows, dynamically typed languages will execute to completion every program which contains no dynamic type errors. Statically typed languages will prevent some such programs from executing in the first place (at best, forcing the user to rewrite his already correct program using sum types). On this basis, one can therefore argue that dynamically typed languages are more dynamically expressive. It also provides a mirror-image encoding from above: one can always translate statically typed programs to a dynamically typed equivalent.

All that I've done in the above is to restate a simple principle: statically and dynamically typed languages enforce their types at different points in a program's life-cycle. Depending on whether you view things through a static or dynamic type prism, either class of language can be considered more expressive. Dynamically typed languages will try and execute type-unsafe programs; statically typed languages will reject some type-safe programs. Neither choice is ideal, but all our current theories suggest this choice is fundamental. Therefore, stating that one class of language is more expressive than the other is pointless unless you clearly state which prism you're viewing life through.

Conclusion

In summary, if Bob's article had explicitly stated that he was solely considering static expressivity (as e.g. James Iry's chart of language's different static expressivity does), I would have agreed with it. In this article, I've tried to show that statically and dynamically typed languages overlap in many ways, but differ in others. Neither is exactly a subset of the other nor, as the underlying theory shows, could they be. Arguing whether static or dynamic typing is universally better or more expressive is therefore pointless. One must consider the pros and cons for the tasks one has at hand, and choose accordingly. Personally, I use both styles, and I have no wish to unduly restrict my language toolbox.

Acknowledgements: My thanks to Martin Berger and Christian Urban for insightful comments on early drafts of this article. All opinions, errors, omissions, or infelicities, are my own.

Updated (October 25 2012)

Joseph Cottam pointed out that the code example was incorrect if l contained an empty string at position 0. I've updated the comment in the code accordingly.

Footnotes

[1] Since formally proving this turns out to be rather hard, some seemingly sound type systems have turned out not to be so (e.g. Eiffel). Fixing this after the fact is then problematic because restricting the type system further to make it sound is likely to end up with perfectly correct real-world programs suddenly being identified as type-unsafe.

[2] One can equally imagine static analysis techniques which would let the program snippet through. Static analysis techniques tend to be both unsound and incomplete in order to make wider-ranging analysis possible. They therefore can not replace static type systems, but can augment them.

Follow me on Twitter @laurencetratt

Link to this entry

 

All posts

 

Last 10 posts

An editor for composed programs
The Bootstrapped Compiler and the Damage Done
Relative and Absolute Levels
General Purpose Programming Languages' Speed of Light
Another Non-Argument in Type Systems
Server Failover For the Cheap and Forgetful
Fast Enough VMs in Fast Enough Time
Problems with Software 3: Creating Crises Where There Aren't Any
Problems with Software 2: Failing to Use the Computing Lever
Problems with Software 1: Confusing Problems Whose Solutions Are Easy to State With Problems Whose Solutions Are Easy to Realise
 
 

DSLs

Tony Clark
Zef Hemel
 

Modelling

Mark Delgano
Steven Kelly
Jim Steel
 

OS

Marc Balmer
Ross Burton
Peter Hansteen
OpenBSD Journal
Ted Unangst
 

Programming

Peter Bell
Gilad Bracha
Tony Clark
Cliff Click
William Cook
Jonathan Edwards
Daniel Ehrenberg
Fabien Fleutot
Martin Fowler
John Goerzen
Grace
James Hague
James Iry
JOT
Ralf Laemmel
Lambda the Ultimate
Daniel Lemire
Michael Lucas
Bertrand Meyer
Keith Packard
Havoc Pennington
Brown PLT
John Regehr
Software Engineering Radio
Diomidis Spinellis
Shin Tai
Markus Voelter
Phil Wadler
Russel Winder
Steve Yegge