What is a type error?

[Chris Uppal]

Chris Smith wrote:

>  Some people here seem to be
> saying that there is a universal concept of "type error" in dynamic
> typing, but I've still yet to see a good precise definition (nor a good
> precise definition of dynamic typing at all).

How about this, at least as a strawman:

I think we're agreed (you and I anyway, if not everyone in this thread) that we
don't want to talk of "the" type system for a given language.  We want to allow
a variety of verification logics.  So a static type system is a logic which can
be implemented based purely on the program text without making assumptions
about
runtime events (or making maximally pessimistic assumptions -- which comes to
the same thing really).  I suggest that a "dynamic type system" is a
verification logic which (in principle) has available as input not only the
program text, but also the entire history of the program execution up to the
moment when the to-be-checked operation is invoked.

I don't mean to imply that an operation /must/ not be checked until it is
invoked (although a particular logic/implementation might not do so).  For
instance an out-of-bound array access might be rejected:
    When the attempt was made to read that slot.
    When, in the surrounding code, it first became
      unavoidable that the about read /would/ be reached.
    When the array was first passed to a function which
      /might/ read that slot.
    ...and so on...

Note that not all errors that I would want to call type errors are necessarily
caught by the runtime -- it might go happily ahead never realising that it had
just allowed one of the constraints of one of the logics I use to reason about
the program.  What's known as an undetected bug -- but just because the runtime
doesn't see it, doesn't mean that I wouldn't say I'd made a type error.  (The
same applies to any specific static type system too, of course.)

But the checks the runtime does perform (whatever they are, and whenever they
happen), do between them constitute /a/ logic of correctness.  In many highly
dynamic languages that logic is very close to being maximally optimistic, but
it doesn't have to be (e.g. the runtime type checking in the JMV is pretty
pessimistic in many cases).

Anyway, that's more or less what I mean when I talk of dynamically typed
language and their dynamic type systems.


> I suspect you'll see the Smalltalk version of the objections raised in
> response to my post earlier.  In other words, whatever terminology you
> think is consistent, you'll probably have a tough time convincing
> Smalltalkers to stop saying "type" if they did before.  If you exclude
> "message not understood" as a type error, then I think you're excluding
> type errors from Smalltalk entirely, which contradicts the psychological
> understanding again.

Taking Smalltalk /specifically/, there is a definite sense in which it is
typeless -- or trivially typed -- in that in that language there are no[*]
operations which are forbidden[**], and none which might not be invoked
deliberately (e.g. I have code which deliberately reads off the end of a
container object -- just to make sure I raise the "right" error for that
container, rather than raising my own error).  But, on the other hand, I do
still want to talk of type, and type system, and type errors even when I
program Smalltalk, and when I do I'm thinking about "type" in something like
the above sense.

    -- chris

[*] I can't think of any offhand -- there may be a few.

[**] Although there are operations which are not possible, reading another
object's instvars directly for instance, which I suppose could be taken to
induce a non-trivial (and static) type logic.