program surgery vs. type safety

[Alex Martelli]

Jeremy Fincher wrote:

> Alex Martelli <aleax at aleax.it> wrote in message
> news:<QAOsb.21403$hV.779611 at news2.tin.it>...
>> Sure,
>> "tests can only show the _presence_ of errors, not their
>> _absence_".  But so can static, compiler-enforced typing -- it
>> can show the presence of some errors, but never the absence of
>> others ("oops I meant a+b, not a-b"! and the like...).
> 
> But it *does* show the absence of type errors, and almost any
> invariant can be coded into the Hindley-Milner typesystem.  Writing to

How do most _typical_ invariants of application programs, such
as "x > y", get coded e.g. in Haskell's HM typesystem?  I don't
think "almost any invariant" makes any real sense here.  When I'm
doing geometry I need to ensure that any side of a triangle is
always less than the sum of the other two; when I'm computing a
payroll I need to ensure that the amount of tax to pay does not
exceed the gross on which it is to be paid; etc, etc.  Simple
inequalities of this sort _are_ "most invariants" in many programs.
Others include "there exists at least one x in xs and at least
one y in ys such that f(x,y) holds" and other such combinations
of simple propositional logic with quantifiers.

> a file opened for reading, multiplying matrices with improper
> dimensions, etc. are both (among others) valid for encoding in the
> typesystem.  Too many dynamic typing advocates look at a typesystem
> and see only a jail (or a padded room ;)) to restrict them.  A good

And (IMHO) too many static typing advocates have a hammer (a static
typesystem) and look at the world as a collection of nails (the very
restricted kinds of invariants they actually can have that system
check at compile-time), conveniently ignoring (most likely in good
faith) the vast collection of non-nails which happen to fill, by
far, most of the real world.

> static typesystem isn't a jail, but the raw material for building
> compiler-enforced invariants into your code.  Think DBC that the
> compiler won't compile unless it can *prove* the contract is never
> violated.

What I want is actually a DBC which will let me state invariants I
"know" should hold even when it's not able to check them *at run
time*, NOT one that is the very contrary -- so restrictive that it
won't let me even state things that would easily be checkable at
run time, just because it can't check them at _compile_ time.

If I state "function f when called with parameter x will terminate 
and return a result r such that pred(r,x) holds", it may well be
that even the first part can't be proven or checked without solving
the Halting Problem.  I don't care, I'd like to STATE it explicitly
anyway in certain cases, perhaps have some part of the compiler
insert a comment about what it's not been able to prove (maybe it
IS able to prove that _IF_ f terminates _THEN_ pred(r, x) holds,
that's fine, it might be helpful to a maintainer to read the (very
hypothetical) computer-generated comment about having proven that
but not having been able to prove the antecedent.

But I'm not going to be willing to pay very much for this kind of
neat features -- either in terms of money (or equivalents thereof,
such as time) or convenience and comfort.  I would no doubt feel
otherwise, if the kinds of applications I code and the environments
in which I work were vastly different.  But they aren't, haven't
been for the > 1/4 century I've been programming, and aren't at all
likely to change drastically any time soon.  So, I see static typing
as a theoretically-interesting field of no real applicability to my
work.  If I felt otherwise about it, I would most likely be coding
in Haskell or some kind of ML, of course -- nobody's come and FORCED
me to choose a dynamically-typed language, you know?

> The main point, however, you made yourself: tests can only show the
> *presence* of errors, whereas static typing can prove their absence.

Static typing *cannot* "prove the absence of errors": it can prove the
absence of "static typing errors", just like a compilation phase can
prove the absence of "syntax errors", and the tests can equally well
prove the absence of the EQUALLY SPECIFIC errors they're testing for.

NONE of these techniques can "prove the absence of errors".  CS
theoreticians have been touting theorem-proving techniques that IN
THEORY should be able to do so for the last, what, 40+ years?  So
far, the difference from theory and practice in practice has proven
larger than the difference between practice and theory in theory.

Incidentally, at least as much of this theoretical work has been
done with such dynamic-typing languages as Scheme as with such
static-typing languages as ML.  Static typing doesn't seem to be
particularly necessary for THAT purpose, either.


>>  In my
>> experience, the errors that static type-checking reliably catches
>> are a subset of those caught by systematic tests, particularly
>> with test-driven design.
> 
> But does the compiler write the tests for you?  At the very least, one
> could argue that static typing saves the programmer from having to
> write a significant number of tests.

One could, and one would be dead wrong.  That is not just my own
real-life experience -- check out Robert Martin's blog for much more
of the same, for example.  Good unit tests are not type tests: they
are _functionality_ tests, and types get exercised as a side effect.
(This might break down in a weakly-typed language, such as Forth or
BCPL: I don't have enough practical experience using TDD with such
weakly-typed -- as opposed to dynamically strongly-typed -- languages
to know, and as I'm not particularly interested in switching over to
any such language at the moment, that's pretty academic to me now).


>>  But systematic use of tests also
>> catches quite a few other kinds of errors, so, it gives me MORE
>> confidence than static type-checking would; and the "added
>> value" of static type-checking _given_ that I'll have good
>> batteries of tests anyway is too small for me to yearn to go
>> back to statically checked languages.
> 
> You make it seem like static typing and tests are mutually exclusive.

No: the fact that the added value is too small does not mean it's zero,
i.e., that it would necessarly be "irrational" to use both if the
costs were so tiny as to be even smaller than the added value.  Say
that I'm typing in some mathematical formulas from one handbook and
checking them on a second one; it's not necessarily _irrational_ to 
triple check on a third handbook just in case both of the first should
happen to have the same error never noticed before -- it's just such
a tiny added value that you have to be valuing your time pretty low,
compared to the tiny probability of errors slipping by otherwise, to
make this a rational strategy.  There may be cases of extremely costly
errors and/or extremely low-paid workforce in which it could be so (e.g.,
if the N-uple checking was fully automated and thus only cost dirt-cheap
computer-time, NO human time at all, then, why not).

In practice, I see test-driven design practiced much more widely by
users of dynamically typed languages (Smalltalk, Python, Ruby, &c),
maybe in part because of the psychological effect you mention...:

> Obviously, they're not, though admittedly when I programmed in O'Caml
> I felt far less *need* for tests because I saw far fewer bugs.

...but also, no doubt, because for most people using dynamically
typed languages is so much faster and more productive, that TDD is
a breeze.  The scarcity of TDD in (e.g.) O'Caml then in turn produces:

> Good thing, too -- the testing libraries available for O'Caml (like
> most everything else for that language) are pretty nasty :)

...this kind of effect further discouraging sound testing practices.

(There are exceptions -- for reasons that escape me, many Java shops
appear to have decent testing practices, compared to C++ shops -- I
don't know of any FP-based shop on which to compare, though).


Alex