RE: dynamic vs. static typing

["Anton van Straaten" <address@hidden>]

Joe Marshall wrote:
> Howard Stearns <stearns@alum.mit.edu> writes:
>
> > OK, how's this:
> >
> >    "1. Without early spellchecking, the proportion of typos which
> >    manifest during later stages rises significantly.
> >
> >    "2. Often, the nature of those typos isn't identified as clearly
> >    during compiling, testing, or runtime as it would be by a
> >    spell-checker, so they take longer to track down.
> >
> > I don't agree when Anton writes 1 and 2 about type
> > checking, and I do believe the same unscientific argument about spell
> > checking.
>
> Anton's number one is just an observation that bugs that are fixed
> early don't have to be fixed later.  Hard to argue that.
>
> I'm less sure about #2.  Even if it is true, I could counter with
> ``Often, the nature of the type error isn't identified as clearly
> during type checking as it would be by a dynamic test, so they take
> longer to track down.''  This is not as absurd as it sounds at first
> glance.  Olaf Chitil gives this example:
>
>   reverse [] = []
>   reverse (x:xs) = reverse xs ++ x
>
>   last xs = head (reverse xs)
>   init = reverse . tail . reverse
>
>   rotateR xs = last xs : init xs
>
> yields this error:
>
>   ERROR (line 7): Type error in application
>   *** Expression     : last xs : init xs
>   *** Term           : last xs
>   *** Type           : [a]
>   *** Does not match : a
>   *** Because        : unification would give
>                        infinite type
>
> It sure looks like a bug in line 7, but the bug is actually in line 2.
>   reverse (x:xs) = reverse xs ++ [x]
>
> Now if this were an error discovered at runtime in a dynamically typed
> language it would show us that the second argument to the list
> concatenation wasn't a list, but rather a list element.  The error
> would be discovered right in the erring routine.

This might be an argument for soft typechecking: if you don't understand
what the typechecker is telling you, run unit tests to debug the problem.
Another reason that multiple layers can help.

Most of my real-world experience with static typecheckers has been with
languages like C++ and Java, which don't seem to suffer from the above
phenomenon as much - presumably, mainly because the type systems are less
ambitious, e.g. non-inferencing.  When they do get more ambitious - e.g.
with type parameterization in templates/generics - the error messages tend
to get correspondingly more cryptic.

Perhaps this would be a good time for Shriram to expand on an earlier
comment he made (on Tue 11/18/2003 at 4:58 PM):

> type systems that work by inference, rather than annotation
> checking, often do not explicitly "check".  This phenomenon
> is why they sometimes provide incomprehensible type errors.
> (I can explain this in a bit more detail if anyone cares.)

I understand the general principle that the more abstract a piece of code
is, the harder it becomes to produce errors (and other information) that are
meaningful to the domain to which the code is being applied.  Is there
anything more specific at work in the type inferencing case that makes more
meaningful errors more difficult (or impossible)?

With highly abstract code, it's often possible to do a better job of error
reporting by providing additional information when specializing the code.  I
suppose one type system equivalent would simply be to provide explicit
annotations, thus possibly losing both polymorphism and inferencing.  Are
there better options?

Anton