What is a type error?

[Chris Smith]

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
MindIQ Corporation