Why do some people insist on static type checking? (was Re: Why would anyone want opacity?)

[Michael R. Blair <ziggy@martigny.ai.mit.edu>]

> From: Gerald Jay Sussman <gjs@martigny.ai.mit.edu>
> Subject: Why would anyone want opacity?
> Date: Thu, 9 May 96 15:38:03 -0400
> 
> > I don't see how ENFORCEMENT of a restriction, such as strong typing,
> > has anything to do with thinking.  ENFORCEMENT is a management tool.

> To which Matthias responded:
>
>  For me ... types are a restriction. This also frees brain capacity, thereby
>  helping us focus on the more important aspects of program design.

Sigh. How many more times are we going to have to sit through this
re-hashing of people's positions on whether or not strong, explicit,
syntactic type declarations are The Right Thing (tm)?

Why can't we achieve some reasonable compromise?  For example:

NOTE: THIS IS NOT A PROPOSAL
--------------------------------------------------------------------------
In MIT Scheme, the reader allows the following syntactic extension to
LAMBDA parameter lists:

(LAMBDA ((<var> <declaration-stuff>)
         (<var> <declaration-stuff>))
   ...)

No mention is made as to what the <declaration-stuff> is.  In fact, the MIT
Scheme compiler/reader completely ignores it (so far as I can tell).
--------------------------------------------------------------------------
NOTE: THAT WAS NOT A PROPOSAL

It was put there by Bill Rozas to make Jonathan Rees happy so he could
implement mini-FX in MIT Scheme (where mini-FX is a strong, explicit,
static type declaring syntactic extension to standard Scheme).  It is just
a syntactic extension.  What people do with it is their own business.

So Jonathan Rees (and Matthias Blume) can type:

    (LAMBDA ((x fixnum) (y flonum)) ...)

...and Bill Rozas can write...

    (LAMBDA ((p prime?)
             (n (lambda (x) (or (odd? x) (schticklegrueber? x)))))
      ...)

...and Gerry Sussman can write...

    (LAMBDA (x y) (+ x y))

...and we can all stop fighting about the benefits/drawbacks of strong,
explicit, syntactic type declarations.

Some implementations will choose to enforce these declarations.  Some will
do it at compile time.  Some will do it at run-time.  And some will ignore
them completely, using them only for embedded comments (read: as an aid or
hindrance to thinking w/o implications on any mechanizations). Any
particular compiler that expects a particular syntax for the type spec part
of the declarations (like FLONUM v. PRIME? v. SHORT) could just emit
warnings if the expected declaration syntax is violated or whatever
enforcement policy a compiler writer might decide to impose.

Some people will annotate their code with them and some will not.  But all
will be re-assured that whatever they do is portable syntax, even if some
compilers might snub their nose at specific type specs.

--

Rather than sit through yet another round of the perennial filibuster on
static typing, I'd much prefer to see a fresh, thought-provoking,
non-binding, syntactic extension to Scheme that would allow people to
experiment in a standard way so that if there _is_ a dominant factor that
might sway the majority to one conclusion or the other about the benefits
of static typing, then Scheme community might collectively achieve
consensus.

I'm not proposing we make any effort to solve the general DECLARE problem
(a la Common Lisp).  I'm just suggesting non-binding syntactic extension
what might be expounded upon in an R5RS appendix-style implementations
straw-man library section.

We already have '[' & ']' as non-binding potential syntactic extensions.
Why not a slightly generalized LAMBDA parameter list syntax as well?

So, is anyone who proselytizes the virtues of static typing willing to put
in the time and effort to devise a proposal for some sort of non-binding
syntactic extension like this which implementations can choose to ignore
but which all will accept as compliant syntax?

If not, then what could you possibly hope to achieve by bringing it up on
the RnRS authors list?

Or would those who don't like type declarations categorically oppose any
such syntactic extension, even if it _were_ non-binding?  (Gerry, you're
not allowed to object because MIT Scheme already has it ;-).

--

I would hope that some such non-binding syntactic compromise might allow us
to all live together in peace even if we might continue to disagree on the
merits of type declarations.

So, is `type declaration detente' possible in our time or are we hopelessly
grid-locked on this issue (too)?