Re: Erlang type system and static vs. dynamic types

[Jan-Willem Maessen <address@hidden>]

Russ Ross <ll@russross.com> writes:
> I was reading Joe Armstrong's paper "The development of Erlang" from
> ICFP '97 and noticed this interesting point when talking about the
> new type system being applied to the standard libraries:
> 
>   "The type system has uncovered no errors.  The kernel libraries
>    were written by Erlang "experts"--it seems that good programmers
>    don't make type errors.  It will be interesting to see if this
>    remains true when we start type checking code written by less
>    experienced programmers."

To me, this says very little about type systems at all.  Instead what
it says is "Well-written, well-tested code doesn't contain many
errors".  

> I've read similar comments by Python and Lisp advocates who assert
> that latent typing doesn't lead to errors that pop up late in the
> game as one might expect because those just aren't the kinds of
> errors that programmers tend to make in practice.  This Erlang
> example seemed like a good concrete data point supporting such
> claims.
> 
> One of the points static type systems promise is reduction of these
> kinds of errors.  [...]

Advocates of static typing do sometimes make the argument that
non-statically-typed code may contain latent type errors which may one
day break the program.  I think this line of argument is a bit of a
red herring [1].  Both sides of the static/dynamic typing debate have
latched on to it rather ferociously, I fear, with no benefit to
anyone.

Instead, the hope of static typing is to quickly and accurately catch
a large number of fairly basic errors---type errors---allowing the
programmer to focus energy on deeper bugs.  Yes, many of those errors
would also be caught simply by running the code.  But then we must go
through the tedious process of localizing the error and re-building
the program, one type error at a time.

> [...]  Our
> application rarely suffered from invalid class cast exceptions, and
> when it did they appeared very early (usually at system startup time
> from dynamically loaded classes and configuration data) so they were
> easy bugs to find and fix.

But what if we didn't have to take the time to run our program and
find them at all?

With a sufficiently polymorphic type system, the class of errors we
spot is pretty large, and there isn't nearly as much work to do once
the program compiles.  [The Haskell programmer's hubris is "once it
passes the type checker, it just works".  I won't go quite this
far---I've written too much Haskell code for that---but it works right
the first time almost all the time.]

And of course static types *are* a nice method for enforcing very
simple contracts in code written by multiple programmers.  No
substitute for good design and modularity, but a help.

-Jan-Willem Maessen
jmaessen@alum.mit.edu

[1] A red herring unless one is writing security or safety-critical
code of some sort and is seeking to provide particular guarantees to
the programmer.  A glance at any PoPL proceedings after 1995 or so
will show that this has become a major focus of academic type theory.