So your language of choice requires nothing of what you type in?  What
if your cat runs across the keyboard?  Will that necessarily produce
runnable code?

Of course you don't mean that.  You have a firmly held opinion, and
you're frustrated that others don't share it.  I'm in great danger of
making an analogy with certain politicians.

The only solid argument I've seen that static typing is significantly in
the way came from one of the static typers (Was it Joachim?), who
pointed out that it can sometimes take an annoyingly long time to finish
propagating a change.  The rest seem to be claims that a message queue
could have lots of types of message, which is conveniently done as a
list of heterogeneous types, and can as easily be done as a list of a
sum type, or heterogeneous lists used where a tuple is really the right
data structure.

Personally, I can see the value in both approaches.  Which means that I
agree with your calm, deliberative opinion that static typing is not the
ultimate good, while I disagree with your hysterical opinion that it is
necessarily bad.

Also, remember that Lisp is fundamentally a language for defining languages
(usually with sexp-syntax, of course).  AFAIK, there IS a completely
statically-typed language built with Lisp, though the name escapes me (had
Q in it maybe?).

But note that subtyping does not strictly require type annotations. Type
inference with subtyping *is* possible, but it is too expensive to be
considered worthwhile.

A slighlty different approach to achieve something "subtyping-like" which is
more appropriate for type inference, is row polymorphism, as employed in
O'Caml. Actually, I'm pretty certain that the combination of universal and
existential row polymorphism would be much more powerful than subtyping
anyway.

        - Andreas

--
Andreas Rossberg, rossb...@ps.uni-sb.de

Prelude> let x = 5 :: Int
Prelude> let y = 9 :: Double
Prelude> x + y

"Formal Analysis of the Remote Agent Before and After Flight"

Klaus Havelund, Mike Lowry, SeungJoon Park, Charles Pecheur, John Penix ,
Willem Visser, Jon L. White

Abstract: This paper describes two separate efforts that used the SPIN
model checker to verify deep space autonomy flight software. The first
effort occurred at the beginning of a spiral development process and found
five concurrency errors early in the design cycle that the developers
acknowledge would not have been found through testing. This effort
required a substantial manual modeling effort involving both abstraction
and translation from the prototype LISP code to the PROMELA language used
by SPIN.

Interestingly, no one brought up the well known (or at least it ought to
be well known) story of the race condition in the Remote Agent as a
counterexample to my claim that an undue emphasis on static typing led to
neglecting what ultimately turned out to be the real problem in the
billing system, so I'll do it myself.

The Remote Agent was written in Lisp, and it also suffered a potentially
catastrophic race-induced problem (a deadlock this time) in flight.
However, there was one significant difference: the race condition existed
not because we didn't try to find them.  We did, and in fact the methods
that we used to find them were successful.  However, we only applied them
to part of the codebase, and the bug turned up in a part of the code that
we hadn't analyzed.

If we had analyzed the entire code base it would have saved us a lot of
grief.  The reason we didn't is because 1) using SPIN is very labor
intensive and we had a lot of code, so we didn't have time to do it all.
To use SPIN you have to essentially re-code your algorithm into SPIN's own
language (PREOMLA).  And 2) We thought that if we built a small core that
was analyzed by SPIN, then we could get away with not analyzing the rest
of the code as long as it was built on top of this proven-safe core.  The
RA bug showed that this doesn't work in general.  (BTW, this is also a
counterexample to the theory that you can't learn anything from a single
data point.)

The pernicious nature of multithreading bugs is well enough documented
that IMO no mission-criticial multithreaded code should ever be used
without running it through SPIN or something equivalent.  Of course, it
would be nice if there were a programmign language that had SPIN's
analysis built-in to it so that it weren't so expensive to do.  There's no
reason why this can't be done, it just hasn't been.  And yes, I think this
can be attributed at least in part to the undue emphasis placed on static
typing.

   val r = ref []

Then r would have the type 'a list ref.  So, I should be able to do
something like:

   r := 2 :: !r

and also something like:

   r := "three" :: !r

But this is obviously unsound.  You can think of the ref cell as acting
as a channel of communication between different parts of a program that
aren't type checked against each other.

The solution in SML'97 is that when you write

   val v = some expression

the free type variables in can only be generalized (that is, bound by
forall) if "some expression" is guaranteed syntactically not to cause
a problem.  Specifically, you can have constants, variables, lambda
abstraction, and constructors (other than ref) applied to the those
same things.  Values can be polymorphic, but expressions that might
do some computation can't, so you can't have function application there.

SML'90 had a different restriction, and I don't know what Ocaml does.
I'm sure Andreas or Matthias could explain this better.

You see it as dangerous, but people have been using this feature of lisp
for years and years, and yet we don't hear complaints about the "subtle
conversion bugs" that we've laid ourselves open to.

There's also an issue that a mind-set that works in academia may not
translate well to industry, because the constraints are different.  The
need to get product out the door often requires cutting corners, so you
can't apply all the cool ideas you developed in the research lab.

In my Smalltalk code that would include going through and changing the
method parameter names from anInteger to anIntegerOrString ;-)

    let x = big_hairy_expression in (f x, g x)

x is not a variable with some type, nor is it a
variable-that-holds-a-value-of-some-type.  It's just a name that I use
in place of big_hairy_expression so that I don't have to type it twice.
B_h_e has a type, so x has the same type because it's just a stand-in
for b_h_e.

Empirical evidence that Ada is more maintainable that C++ does seem to
exist.

Yes, that's why lispers are so productive - we can get lots of good lisp
programmers, since we're only paying them a can of Friskies a day.

The flame war would be about the extent to which Strongtalks
technology (polymorphic inline caches) have already been incorporated
into current Smalltalk implementations.

I find it helps to limit searches to Eliot Miranda's postings ;-)
http://groups.google.com/groups?q=strongtalk+miranda&hl=en&lr=&ie=UTF...

You may also find this seminar interesting:
"Bytecode-to-bytecode adaptive optimization for Smalltalk Compilation
and execution architecture for late-bound object-oriented programming
languages"

http://www.stanford.edu/class/ee380/Abstracts/030312.html

http://murl.microsoft.com/videos/stanford/ee380d/030312_OnDemand_100_...

BTW Erlang philosophy states that objects should /never/ be shared
across threads, and Erlang enforces this simply by offering no way to do
that, so it's easy enough to enfoce.
 From what I hear from the Erlang camp, the constraint isn't severe as
well; in fact, they consider this as a key property of systems that
remain stable in the presence of software errors.

Reading and writing the same name usually results in having both an
upwards /and/ a downwards restriction, making the name monomorphic.
In an OO context, this means that the name cannot be redefined at all in
a subclass without making the subclass a non-subtype.
In an FPL context, I suspect that HM typing will either be forced into
making the name monomorphic (not desirable since that directly inhibits
many forms of reuse), or fail because there is no valid types-to-names
association. (Hope I understood this correctly. Corrections welcome.)

Consider this simple example, from production code:

,----[ overlay.hh ]
| #ifndef OVERLAY_HH
| #define OVERLAY_HH
|
| #include "noncopyable.hh"
|
|
| template <typename T>
| class overlay : noncopyable
| {
| public:
|     typedef T value_type;
|
|     overlay(value_type& val,
|             const value_type& overlaid_value)
|         : val_( val ),
|           original_value_( val_ )
|     { val_ = overlaid_value; }
|
|     ~overlay()
|     { val_ = original_value_; }
|
| private:
|     value_type& val_;
|     const value_type original_value_;
| };
|
|
| #endif        // OVERLAY_HH
`----

An "overlay" is temporary, scoped assignment to some other mutable
variable that will be undone upon the overlay's destruction, similar
to Perl's "local" declaration or layered assignment to special
variables in CL.

Assuming that the value_type's assignment operator can't throw an
exception, using an overlay is safe and is safer than writing four
separate, explicit assignment statements (one to store the original
value, one to change the value, another to restore the original value
under normal exit, and yet another to restore the value in case of a
caught exception, presumably before rethrowing).

The cleanup is not represented syntactically, but the symmetric
promise is: I may change this variable here, and I will change it back
before going away.

{
   int i = 0;

   try
   {
      const overlay<int> o( i, 1 );
      // We're not leaving until i is 0 again.

      std::cout << i << '\n';

      throw std::runtime_error( "bang!" );
   }
   catch ( ... )
   { std::cout << i << '\n'; }

In fact, I often cite MCO as an example for my basic claim, which is that
languages mold people's thinking in often undesirable ways.  People write
"1.2" and "3.4" when what they really mean is "1.2 newtons" and "3.4
pounds" because the languages that they use understand "1.2" and "3.4" and
they don't understand "1.2 newtons" and "3.4 pounds".  If MCO code had
been written in a language that directly supported physical quantities (as
opposed to simply floating point numbers) or one where such a facility
could have been added things might have gone differently.

There are many, many examples of this sort of thing.  People think that
"ints" are integers, "floats" and "doubles" are reals, or that char*'s are
strings when none of these things are really true.  They do this because
the languages understand "int" and "float" and "double" and "char*" but
don't know about integers and reals and strings.  I suspect most of the
people reading this know this, but a lot of programmers don't, or at least
don't think about it when they code.