in defense of types

[Matthias Felleisen <address@hidden>]

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