What is a type error?
pc at p-cos.net
Tue Jun 27 22:57:34 CEST 2006
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
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
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.
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
More information about the Python-list