|Home > Blog||e-mail: email@example.com github: ltratt twitter: @laurencetratt|
October 25 2012
static vs. dynamicdebates 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
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
type T1: ... type T2: ... sumtype S rangesover T1, T2 func f(x : S): typecase x: whenoftype T1: ... whenoftype T2: ...As this suggests,
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:
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
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.
UsabilitySum 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 multitypesBob 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
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
Expressivenessis 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 .
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 # 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 stringsSound static type systems will reject such programs as type-unsafe, because a) the
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.
ConclusionIn 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
more expressiveis 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
Footnotes 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.
 One can equally imagine
|Home > Blog||e-mail: firstname.lastname@example.org github: ltratt twitter: @laurencetratt|
|Copyright © 1995-2015 Laurence Tratt|