RE: dynamic vs. static typing

["Anton van Straaten" <address@hidden>]

On 30 Nov 2003, at 4:36 PM, Pascal Costanza wrote:
> >> Anton van Straaten wrote:
> >>
> >>> Pierce has a nice description of the subjective effects of
> >>> static type checks, in TAPL:
> >>>
> >>>    "In practice, static typechecking exposes a surprisingly
> >>> broad range of errors.  Programmers working in richly typed
> >>> languages often remark that their programs tend to "just work"
> >>> once they pass the typechecker, much more often than they feel
> >>> they have a right to expect.  One possible explanation
> >>> for this is that not only trivial mental slips [...] but also
> >>> deeper conceptual errors [...] will often manifest as
> >>> inconsistencies at the level of types."
...
> > Calling it a subjective assessment is a little misleading: it's a
> > real effect, but it's difficult to describe in a brief summary,
> > and I doubt many people appreciate how complex it is.  So the
> > main way in which this effect is communicated is in the subjective
> > sense, "wow, my programs just work".
>
> I doubt it is possible to describe this in a long and detailed
> analysis. My impression is that you are describing what is essentially
> an esoteric experience. (My intention is not to use this as a
> pejorative term, but simply as the opposite of "exoteric".)

I don't agree with that.  Of course, all experience is subjective, but in
this case the phenomenon being experienced is something which I believe is
possible to define quite well.  However, it is a complex and
multi-dimensional thing: whether it is explicitly identified or not, there
is a separate program that is threaded intricately through every other
program, at every value reference and function/method application.  This
separate program operates on types.  In most languages and with most real
systems, it is at least theoretically possible to run that program before
runtime, and it will tell you when you've done something wrong with types in
your program.  Because this affects every value reference and
functional/method application, the consequences of this are far-reaching.

Just because no-one has sat down to illustrate this phenomenon and its
consequences in detail, doesn't mean it's not possible to do so.  In fact, I
suspect no-one has done it because it is blindingly obvious that the
phenomenon exists, to anyone who has sufficient experience with both
dynamically- and statically- typed languages.  (Note that I'm not saying
that it's blindingly obvious that anyone with such experience would prefer
one over the other, only that they would be aware of the effect I'm talking
about.  If there are any counterexamples out there, please speak up.)

> The pattern community uses the term "quality without a name" for
> similar experiences.

I don't consider this to be an example of that sort of quality.  In
particular, the pattern community is not talking about something with a
strong formalization.  The quality I'm referring to can be described by a
few names, including "provable program properties".  Types in a program are
mathematical proofs, with a direct correspondence to proofs in logic (the
Curry-Howard correspondence).  The subjective experience Pierce describes
may be little more than what one would expect from the fact that when a
compiler statically check types, it's essentially running a proof-checker on
a program and confirming theorems about ubiquitous aspects of that program's
validity.

> There are ways to find out whether such
> experiences have objective content. See
> http://www.patternlanguage.com/archive/ieee/ieeetext.htm

I last read any of that stuff in the '90s.  Rather than re-reading it to
find out what you mean, perhaps you could be more specific about what sort
of tests are proposed?  However, in this case, I'm not sure it's necessary.
I can propose a concrete test that anyone can duplicate, given access to a
programmer familiar with static typing, and one familiar with dynamic
typing.  (They can be the same programmer, if he/she is honest and unbiased,
like me ;)

The test is this: write a non-trivial program in a DT language, and every
time a bug is encountered during testing or in production, examine whether
and how that bug would have been caught by a static type system.  Make a
list of all such instances.  It is guaranteed that there will be a long list
of such bugs.  The experience I'm talking about is the experience of quickly
and provably finding all such bugs, prior to ever running the program.

A point that's perhaps harder to define is the degree to which this all
helps ensure that the program's semantics are correct.  But, even though I
believe there is such a connection, i.e. that early typechecking helps
expose semantic errors, I don't think this is necessarily the main point.
I'll venture out on a limb and say something difficult to prove, but which
perhaps might be intuitively recognized: I suspect many good programmers
more often write semantically correct programs but run into many essentially
trivial bugs, than vice versa (write programs free of trivial bugs but
semantically flawed.)  Early typechecking quickly finds the simple but often
time-consuming stuff, and this alone can provide the experience Pierce
described.  If it helps point out some semantic errors, that's a bonus.

Anton