What is a type error?

[Pascal Costanza]

Chris Smith wrote:
> Pascal Costanza <pc at p-cos.net> wrote:
>> Chris Smith wrote:
>>> Of course zero is not appropriate as a second argument to the division 
>>> operator!  I can't possibly see how you could claim that it is.  The 
>>> only reasonable statement worth making is that there doesn't exist a 
>>> type system in widespread use that is capable of checking this.
>> ...and this is typically not even checked at the stage where type tags 
>> are checked in dynamically-typed languages. Hence, it is not a type 
>> error. (A type error is always what you define to be a type error within 
>>   a given type system, right?)
> 
> Sure, it's not a type error for that language.
> 
>> Note, this example was in response to David's reply that my definition 
>> turns every runtime error into a type error. That's not the case, and 
>> that's all I want to say.
> 
> But your definition does do that.  Your definition of a type error was 
> when a program attempts to invoke an operation on values that are not 
> appropriate for this operation. 

In my definition, I didn't say who or what decides what values are 
appropriate for operations.

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

>>> However, it sounds as 
>>> if you're claiming that it wouldn't be possible for the type system to 
>>> do this?
>> No. I only need an example where a certain error is not a type error in 
>> _some_ language. I don't need to make a universal claim here.
> 
> Definitions are understood to be statements of the form "if and only 
> if".  They assert that /everything/ that fits the definition is 
> describable by the word, and /everything/ that doesn't is not 
> describable by the word.  If that's not what you meant, then we are 
> still in search of a definition.
> 
> 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.


Pascal

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