What is a type error?

[Pascal Costanza]

Chris Smith wrote:
> Pascal Costanza <pc at p-cos.net> wrote:
>> Consider division by zero: appropriate arguments for division are 
>> numbers, including the zero. The dynamic type check will typically not 
>> check whether the second argument is zero, but will count on the fact 
>> that the processor will raise an exception one level deeper.
> 
> 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?)

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.

>> This is maybe better understandable in user-level code. Consider the 
>> following class definition:
>>
>> class Person {
>>    String name;
>>    int age;
>>
>>    void buyPorn() {
>>     if (< this.age 18) throw new AgeRestrictionException();
>>     ...
>>    }
>> }
>>
>> The message p.buyPorn() is a perfectly valid message send and will pass 
>> both static and dynamic type tests (given p is of type Person in the 
>> static case).
> 
> It appears you've written the code above to assume that the type system 
> can't cerify that age >= 18... otherwise, the if statement would not 
> make sense.

Right.

> It also looks like Java, in which the type system is indeed 
> not powerfule enough to do that check statically.

Right.

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

> If so, that's not correct.  If such a thing were checked at 
> compile-time by a static type check, then failing to actually provide 
> that guarantee would be a type error, and the compiler would tell you 
> so.

That's fine, but not relevant in this specific subplot.


Pascal

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