I wholly agree with you. The compile-time checks that static typing enable are
tremendously convenient. If your language also provides an easy way to declare
subtypes, then this mechanism becomes even more useful.

However, the common assumption that the "bondage and discipline" of static
typing is somehow inherently incompatible with "language features that allow you
to mix things together with complete freedom" is not entirely true.

I'll confess I'm not precisely sure how you mean "mix things together", so I'll
just go through the options that occur to me:

1) If you mean how C programmers are likely to use an "int" for both coordinates
and passenger counts, and thus could add them together erroneously, then this is
actually a case of a *lack* of a language feature--specifically, straightforward
subtyping machinery.

2) If you mean how some languages employ implicit type coercion, then you of
course realize this is simply (sub)type unification.

3) If, as I hope, you are instead referring to beasties such as Lisp, which, in
the strong sense, really do "allow you to mix things together with complete
freedom", then we have something to talk about. Lisp happens to be
dynamically-typed, but this sort of expressivity is actually *not* incompatible
with static typing. The pattern calculus which I keep spamming the listserv
about is both statically typed *and* allows you to "mix things together with
[almost] complete freedom". The only limitation on this "freedom" is that you
can't compose expressions which don't make sense (are ill-typed), such as "ADD 5
CONS"--but who wants to be able to generate code which provably will cause a
run-time error?


P.S. To all: It's about time for a different subject heading (or even subject),
no? This is hardly "equivalence of maps to classes and types" material...

P.P.S. To Gary: That was pretty lame of me to say that "T" is "eval" for an
expression "T". I'll write you a proper metacircular evaluator for the pattern
calculus when I next have some free time.