| |
Another Non-Argument in Type Systems
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:
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.
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 .
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 .
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
|
|
|