[E-Lang] static typing

Marc Stiegler marcs@skyhunter.com
Tue, 12 Jun 2001 12:15:01 -0700

> 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.

On a good day, static type checking has historically helped me write correct
programs much as capabilities have helped me write secure programs. This is
particularly noticeable writing servlets, for which my testing cycle for a
1-line change is enormous (sometimes requiring a restart of the web server).
On a bad day it just gets in the way and makes me write enormous amounts of
code to do a simple thing (when interfacing to a DBMS, for example). As you
can tell, I have a love/hate relationship with static type checking :-)

> 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.

I have wrestled with the question of what to say about static/dynamic
checking in Walnut at some length. While your discussion here is
illuminating, it doesn't change the following truth, which is approximately
what I say in Walnut (in the Introduction) now: you could write a book just
about the pros and cons of static type checking. E has chosen dynamic type
checking. Lots of excellent real world software has been written with
dynamic type checking. If you the reader are a static type checking
aficionado, all we can say is try E anyway, we think you'll be pleased.