[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
in defense of types
In a recent posting, which I promptly lost, Paul Graham, challenged the
usefulness of static typing in programming languages. I'd like to take
him up on this aspect of PLs.
[Note: For those of you who know me from academic venues,
you will note that I "play Paul" there, but for very different
reasons. We need to challenge each other on such statements
because only strong challenges to scientific claims will ensure
that these claims are 'hardened'. So, if you want to know what's wrong
with types and the influence of the type research community, go to academic
conferences.]
So here we go. Static types are necessary
(1) to establish basic properties of software
and
(2) to establish absolute yet cheap abstraction boundaries between modules.
LL languages suffer from the lack of types, for this very purpose.
(1) Suppose you write a program in your favorite LL. You probably write
some code, develop some tests (in the opposite order of course),
debug, add tests, write more code, etc. You also write some
integration test, and you use some test harness. Fine. What do you
have now? You have a program that works IN SOME scenarios S1 .. Sn
for some finite n.
With static types in your language, you can express infinite
varieties of such scenarios and ask some program to check that your
program FOR ALL such scnearios.
Trivial example: You write f(n) = ... n ... and test f(0), f(-1), f(1),
etc. With types, you can write f(n:Integer):Integer = ... and the
type checker confirms that f produces an Integer when given an
Integer for all Integers. Assuming your type checker is sound, this
is a big help. You will never have to doubt that f's output was an
Integer.
[There is more to say. For example, ML is a language with an explicitly
typed core and a (bad) "programming environment" that elaborates an
implicitly typed surface syntax into the core. Also, MrSpidey (and
friends) doesn't type check for Scheme w/o a language of assertions about
inputs. These assertions form a language of types.)]
(2) Suppose your LL program gets large. You want to do what people always do:
layer the program and introduce boundaries. Yes, in Scheme you can do this
with generative structures (sorry, I don't use "Scheme" in the sense of
"Guy's Scheme." As many here know, I have taken poetic license as far as
Scheme is concerned). BUT, that's expensive. You place the to-be-abstracted
values into a "box", send them outside, and get them back -- untouched.
With types, you can say something like this at a module boundary:
there is a type t, here are some instances of type t,
i even give you functions to create t's, and work with t's,
but i won't tell you what they are implemented in.
Now you or your partners have no way of corrupting these values. And you
know what, they are actually integers, and if you had known, you could have
used all kinds of numeric hacks to compute values. But fortunately you
didn't, because I, the module writer, can now change t to a hash table
and do all kinds of nice things with it.
What's the cost for that? Zero. Yeap, in a statically typed world, there is
no run-time cost.
Is there a conceptual cost? Yes, you can't run programs that don't satisfy
the rules.
-- Matthias