What is a type error?

[Chris Smith]

Chris Uppal <chris.uppal at metagnostic.REMOVE-THIS.org> wrote:
> >     if (x != 0) y = 1 / x;
> >     else y = 999999999;
> >
> > is not all that much different from:
> >
> >     try { y = 1 / x; }
> >     catch (ArithmeticException e) { y = 999999999; }

> My immediate thought is that the same question is equally applicable (and
> equally interesting -- i.e. no simple answer ;-) for static typing.

I don't see that.  Perhaps I'm missing something.  If I were to define a 
type system for such a language that is vaguely Java-based but has 
NotZero as a type, it would basically implement your option [D], and 
contain the following rules:

1. NotZero is a subtype of Number
2. Zero is a subtype of Number

3. If x : Number and k : Zero, then "if (x != k) a else b" is well-typed 
iff "a" is well-typed when the type-environment is augmented with the 
proposition "x : NotZero" and "b" is well-typed when the type-
environment is augmented with the new proposition "x : Zero".

Yes, I know that Java doesn't do this right now in similar places (e.g., 
instanceof), and I don't know why not.  This kind of thing isn't even 
theoretically interesting at all, except that it makes the proof of 
type-soundness look different.  As far as I can see, it ought to be 
second-nature in developing a type system for a language.

In that case, the first example is well-typed, and also runs as 
expected.  The second bit of code is not well-typed, and thus 
constitutes a type error.  The way we recognize it as a type error, 
though, is in the fact that the compiler aborts while checking the 
typing relation, rather than because of the kind of problem prevented.  
Of course, it would be possible to build a static type system in which 
different things are true.  For example, Java itself is a system in 
which both terms are well-typed.

>From a dynamic type perspective, the litany of possibilities doesn't 
really do much for defining a dynamic type system, which I thought was 
our goal in this bit of the thread.  I may not have been clear enough 
that I was look for an a priori grounds to classify these two cases by 
the definition.  I was assuming the existing behavior of Java, which 
says that both accomplish the same thing and react in the same way, yet 
intuitively we seem to think of one as a type error being "solved", 
whereas the other is not.

Anyway, you just wrote another message that is far closer to what I feel 
we ought to be thinking about than my question here... so I will get to 
reading that one, and perhaps we can take up this point later when and 
if it is appropriate.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation