What is a type error?

[Chris Uppal]

Chris Smith wrote:

> But then, I
> dislike discussion of strong/weak type systems in the first place.  It
> doesn't make any sense to me to say that we verify something and then
> don't do anything if the verification fails.  In those cases, I'd just
> say that verification doesn't really exist or is incorrectly
> implemented.

Hmm, that seems to make what we are doing when we run some tests dependent on
what we do when we get the results.  If I run a type inference algorithm on
some of my Smalltalk code, and it tells me that something is type-incorrect,
then I think I'd like to be able to use the same words for the checking
regardless of whether, after due consideration, I decide to change my code, or
that it is OK as-is.  Minor point, though...

Anyway:

>     if (x != 0) y = 1 / x;
>     else y = 999999999;
>
> is not all that much different from (now restricting to Java):
>
>     try { y = 1 / x; }
>     catch (ArithmeticException e) { y = 999999999; }
>
> So is one of them a use of a dynamic type system, where the other is
> not?

My immediate thought is that the same question is equally applicable (and
equally interesting -- i.e. no simple answer ;-) for static typing.  Assuming
Java's current runtime semantics, but positing different type checkers,  we can
get several answers.

A] Trivial: neither involves the type system at all.  What we are seeing
is a runtime check (not type check) correctly applied, or made unnecessary by
conditional code.  And, obviously we can take the same line for the "dynamic
type checking" -- i.e. that no type checking is involved.

B] More interesting, we could extend Java's type system with a NotZero
numeric type (or rather, about half a dozen such), and decree that 1 / x was
only legal if
    x : NotZero
Under that type system, neither of the above would be type legal, assuming x is
declared int.  Or both would be legal if it was declared NotZero -- but in both
cases there'd be a provably unnecessary runtime check.  The nearest "dynamic
type system" equivalent would be quite happy with x : int.  For the first
example, the runtime checks would never fire (though they would execute).  For
the second the runtime "type" might come into play, and if it did, then the
assignment of 999999999 would take place /because/ the illegal operation (which
can be thought of as casting 0 to NotZero) had been replaced by a specific
legal one (throwing an ArithmeticException in this case).

C] A different approach would be to type the execution, instead of the value,
so we extend Java's type system so that:
    1 / x
had type (in part) <computation which can throw ArithmeticException>.  The
first example as a whole then would also have (in part) that type, and the
static type system would deem that illegal.  The second example, however, would
be type-legal.  I hope I don't seem to be fudging the issue, but I don't really
think this version has a natural "dynamic type system" equivalent -- what could
the checker check ?  It would see an attempt to throw an exception from a place
where that's not legal, but it wouldn't make a lot of sense to replace it with
an IllegalExceptionException ;-)

D] Another possibility would be a static type checker after the style of [B]
but extended so that it recognised the x != 0 guard as implicitly giving x :
NonZero.  In that case, again, the first example is static type-correct but the
second is not.  In this case the corresponding "dynamic type system" could, in
principle, avoid testing x for zero the second time.  I don't know whether that
would be worth the effort to implement.  In the second example, just as in
[B], the reason the program doesn't crash when x == 0 is that the "dynamic type
system" has required that the division be replaced with a throw.

One could go further (merge [B] and [C], or [C] and [D] perhaps), but I don't
think it adds much, and anyway I'm getting a bit bored....   (And also getting
sick of putting scare quotes around "dynamic type system" every time ;-)

Personally, of the above, I find [B] most appealing.

    -- chris