What is a type error?

[Chris Smith]

Pascal Costanza <pc at p-cos.net> wrote:
> > Clearly, in this example, the program 
> > is invoking an operation (division) on values that are not appropriate 
> > (zero for the second argument).  Hence, if your definition really is a 
> > definition, then this must qualify.
> 
> Here, you are asking more from dynamic type systems than any existing 
> type system provides. The definition of what is considered to be a type 
> error and what not is always part of the specification of a type system.

No, I'm not.  Were we to follow this path of definition, it would not 
require that dynamic type systems catch ALL type errors; only that they 
catch some.  Not that it matters, though.  I am analyzing the logical 
consequences of your own definition.  If those logical consequences were 
impossible to fulfill, that would be an even more convincing reason to 
find a new definition.  Concepts of fairness don't enter into the 
equation.

> > If you want to make a statement instead of the sort you've implied 
> > above... namely that a type error is *any* error that's raised by a type 
> > system, then that's fine.  It certainly brings us closer to static 
> > types.  Now, though, the task is to define a type system without making 
> > a circular reference to types.  You've already rejected the statement 
> > that all runtime errors are type errors, because you specifically reject 
> > the division by zero case as a type error for most languages.  What is 
> > that distinction?
> 
> I don't need such a distinction. I can just define what is covered by a 
> type system and what is not. All type systems work that way.

You've got to define something... or, I suppose, just go on using words 
without definitions.  You claimed to give a definition, though.

I have been led by others to believe that the right way to go in the 
dynamic type sense is to first define type errors, and then just call 
anything that finds type errors a type system.  That would work, but it 
would require a type error.  You seem to want to push that work off of 
the word "type error" and back onto "type system", but that requires 
that you define what a type system is.  It doesn't work for you to say 
BOTH that a type system is anything that catches type errors, AND that a 
type error is anything that's caught by a type system.  That's not a 
definition; it's just circular reasoning.  If I can plug in: type error 
= fly, type system = frog, and get a valid instance of your definitions, 
then you aren't giving much of a definition.  (Unless you think that 
frogs are perfectly good examples of type systems.)

Incidentally, in the case of static type systems, we define the system 
(for example, using the definition given from Pierce many times this 
thread), and then infer the definition of types and type errors from 
there.  Because a solid definition has been given first for a type 
system without invoking the concepts of types or type errors, this 
avoids being circular.

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