[E-Lang] static typing

[Darius Bacon]

[The `you' here is MarkM, who asked me to copy this to the list.]

I've been going through the e-lang archives and finding much of it
very illuminating -- along with the capabilities webring it's some of
the most educational stuff I've read this year.  One of your posts
from February seems to show a misconception worth pointing out, though
it's not one that would harm E, except insofar as it damages your
credibility with mainstream language theorists.  You wrote:

  In any case, as far as normal type theories are concerned, the only
  thing they're protecting you against is a runtime occurrence of
  "MessageNotUnderstood".  Why should we care?  If this particular
  surprise happens at runtime, at least it's fail-stop, which is vastly
  safer than other things we worry about.  Also, actual experience with
  Smalltalk says that these don't happen too often, and it's not too
  hard to beat them out of a program with runtime debugging.
  Conventional static type checking is like painting the Titanic -- a
  fine thing to do once greater dangers have been taken care of.

I see two nits to pick.  First, a type error is not necessarily
fail-stop with MessageNotUnderstood, because swords and pictures can
both take a draw() message.  This is a minor problem except in
combination with the other problem, which takes more explaining.

People who like modern type systems want you to use them aggressively
to encode the structure of your programs, not just express a few
simple constraints on your variables.  For example, I wrote a compiler
based on program transformation (like Rabbit, Twobit, etc.), with many
phases working on the same data structure, each phase doing some
relatively-simple transformation adding a new invariant.  How do you
know a later phase doesn't mess up an invariant established by an
earlier one?  You might discover a problem only when you run the
compiler's output.  We'd like to see an error as soon as an invariant
is broken, instead.  So a typeful programmer will make a new type for
each restriction of this compiler's input language, and satisfy
himself that the type's constructors establish the invariant, assuming
the inputs satisfy their own invariants.  Now that we have a bunch of
related types that all understand the same set of messages,
MessageNotUnderstood is not going to save us -- we need explicit type
checks.

In other words, in Smalltalk type errors aren't a big deal because
you're not using types for much.

(If all these separate types seem terribly cumbersome, check out
refinement types.)

Of course, to a static typer we're still discovering the error too
late, and worse, we're thinking about it wrong.  We should think of
the program first as a constructive proof that the right sort of
output can be gotten from its input.  By using fine-grained types
we're given fine-grained guidance in how to write our code -- once it
typechecks, it usually works.  I can vouch that this really happens
when using a language that supports it.  (This reminds me of things
MarcS has written about E's capability nature giving him guidance --
once it works, it's usually secure, too.  I'm not sure if there's a
connection.)  You can see all this as a way of leaning on the computer
for automatic theorem proving without needing the full glory of a
general-purpose theorem prover.  Staticness is so basic to this
worldview that one proponent I was arguing with used scare-quotes when
talking about `dynamic "typing"'.  To them, Scheme doesn't have types,
it has just one type.

That worldview isn't mine -- I'm happy with soft typing getting us
most of the benefits without the liabilities.  I do think typeful
programming is a very valuable programming pattern and could turn out
to be just as valuable as a security pattern.  As yet another thing
the mainstream doesn't appreciate, though, it's hardly the top
priority.  But maybe this could lead to some useful/reassuring
discussion in Walnut -- there's still lots of sentiment in favor of
static types out in the world.

Sorry if none of this lecture is new to you.  This quote suggests it
isn't: 

  I strongly suspect that the impressive formal machinery created by
  type checking folks can be retargetted to this far more important
  problem.

Also, I'm not an expert on modern type theory, there's just a basic
set of ideas I've found helpful.

-Darius