Re: in defense of types

[Michael Vanier <address@hidden>]

I agree with everything you say.  Now I'd like to hear what you say against
types in the academic world ;-)  

My view is that types are a very cheap invariant to maintain; in fact, they
usually have negative cost because their presence usually allows
optimizations that are impossible without them.  Add to that the increased
probability of program correctness and it's a solid win.  The downside is
that in languages with weak type systems (e.g. almost anything but ML)
there is a pretty hefty hit on expressiveness.  Another hit is the
increased verbosity in any language without type inference (again, almost
anything but ML).  Even in ML dialects it's tricky to incorporate some
features (e.g. object-orientation; I know ocaml does it but it's not the
most graceful fit).

Also, I don't recall PG challenging the usefulness of static typing.  Maybe
it was the verbosity of explicitly-declared types that he was arguing
against.  Paul?

Mike


> Date: Tue, 28 May 2002 19:55:03 -0400 (EDT)
> From: Matthias Felleisen <matthias@ccs.neu.edu>
> 
> 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
>