What is a type error?
cdsmith at twu.net
Thu Jun 22 20:34:17 CEST 2006
Chris Uppal <chris.uppal at metagnostic.REMOVE-THIS.org> wrote:
> I think we're agreed (you and I anyway, if not everyone in this thread) that we
> don't want to talk of "the" type system for a given language. We want to allow
> a variety of verification logics. So a static type system is a logic which can
> be implemented based purely on the program text without making assumptions
> about runtime events (or making maximally pessimistic assumptions -- which comes
> to the same thing really). I suggest that a "dynamic type system" is a
> verification logic which (in principle) has available as input not only the
> program text, but also the entire history of the program execution up to the
> moment when the to-be-checked operation is invoked.
I am trying to understand how the above statement about dynamic types
actually says anything at all. So a dynamic type system is a system of
logic by which, given a program and a path of program execution up to
this point, verifies something. We still haven't defined "something",
though. We also haven't defined what happens if that verification
fails. One or the other or (more likely) some combination of the two
must be critical to the definition in order to exclude silly
applications of it. Presumably you want to exclude from your definition
of a dynamic "type system" which verifies that a value is non-negative,
and if so executes the block of code following "then"; and otherwise,
executes the block of code following "else". Yet I imagine you don't
want to exclude ALL systems that allow the programmer to execute
different code when the verification fails (think exception handlers)
versus succeeds, nor exclude ALL systems where the condition is that a
value is non-negative.
In other words, I think that everything so far is essentially just
defining a dynamic type system as equivalent to a formal semantics for a
programming language, in different words that connote some bias toward
certain ways of looking at possibilities that are likely to lead to
incorrect program behavior. I doubt that will be an attractive
definition to very many people.
> Note that not all errors that I would want to call type errors are necessarily
> caught by the runtime -- it might go happily ahead never realising that it had
> just allowed one of the constraints of one of the logics I use to reason about
> the program. What's known as an undetected bug -- but just because the runtime
> doesn't see it, doesn't mean that I wouldn't say I'd made a type error. (The
> same applies to any specific static type system too, of course.)
In static type system terminology, this quite emphatically does NOT
apply. There may, of course, be undetected bugs, but they are not type
errors. If they were type errors, then they would have been detected,
unless the compiler is broken.
If you are trying to identify a set of dynamic type errors, in a way
that also applies to statically typed languages, then I will read on.
> But the checks the runtime does perform (whatever they are, and whenever they
> happen), do between them constitute /a/ logic of correctness. In many highly
> dynamic languages that logic is very close to being maximally optimistic, but
> it doesn't have to be (e.g. the runtime type checking in the JMV is pretty
> pessimistic in many cases).
> Anyway, that's more or less what I mean when I talk of dynamically typed
> language and their dynamic type systems.
So my objections, then, are in the first paragraph.
> [**] Although there are operations which are not possible, reading another
> object's instvars directly for instance, which I suppose could be taken to
> induce a non-trivial (and static) type logic.
In general, I wouldn't consider a syntactically incorrect program to
have a static type error. Type systems are, in fact, essentially a tool
so separate concerns; specifically, to remove type-correctness concerns
from the grammars of programming languages. By doing so, we are able at
least to considerably simplify the grammar of the language, and perhaps
also to increase the "tightness" of the verification without risking
making the language grammar context-sensitive. (I'm unsure about the
second part of that statement, but I can think of no obvious theoretical
reason to assume that combining a type system with a regular context-
free grammar would yield another context-free grammar. Then again,
formal languages are not my strong point.)
Chris Smith - Lead Software Developer / Technical Trainer
More information about the Python-list