What is a type error?

[Pascal Costanza]

Chris Smith wrote:
> 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.

Yes it does. All static type systems define only a strict subset of all 
possible errors to be covered, and leave others as runtime errors. The 
same holds for dynamic type systems.

>>> 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.

I didn't know I was supposed to give a definition.

> 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.

Do you mean this one? "A type system is a tractable syntactic method for 
proving the absence of certain program behaviors by classifying phrases 
according to the kinds of values they compute." This isn't really such a 
strong definition because it shifts the problem of what exactly a type 
system is to finding a definition for the word "kind".

But if this makes you happy, here is an attempt:

"A dynamic type system is a tractable syntactic method for proving the 
absence of certain program behaviors by classifying values according to 
their kinds."

Basically, this correlates with the typical approach of using tags to 
indicate the type/kind/class of values. And indeed, this is what dynamic 
type systems typically do: they check tags associated with values. Other 
kinds of runtime errors are not raised because of such checks, but 
because of other reasons. Therefore, there is naturally a distinction 
between runtime errors that are type errors and those that are not.

I am not convinced that this definition of mine is a lot clearer than 
what I have said before, but I am also not convinced that Pierce's 
definition is any clearer either. It is merely a characterization of 
what static type systems do.

The preciseness comes into play when actually defining a type system: 
then you have to give definitions what the errors at runtime are that 
you want to prove absent by way of the static type system, give the 
typing rules for the type system, and then prove soundness by showing 
that the typing rules correlate precisely to the runtime errors in the 
first stage. Since you have to map two different views of the same thing 
to each other you have to be precise in giving definitions that you can 
then successfully use in your proofs.

In dynamic type system, this level of precision is not necessary because 
proving that dynamic type errors is what the dynamic type system catches 
is trivially true, and most programmers don't care that there is a 
distinction between runtime type errors and runtime "other" errors. But 
this doesn't mean that this distinction doesn't exist.


Pascal

-- 
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/