What is a type error?

[Marshall]

Chris Uppal wrote:
>  /Given/ a set of operations which I want to forbid,
> I would like to say that a "dynamic type system" which prevents them executing
> is doing very much the same job as a static type system which stops the code
> compiling.

There are similarities, (classifying values into categories, and
checking
whether functions are sensibly invoked according these categories)
and there are differences (in the difference between existential
quantification of success vs. universal quantification of success.)
They are certainly not identical. (I'm not sure if by "very much the
same" you meant identical or not.)


> Of course, we can talk about what kinds of operations we want to forbid, but
> that seems (to me) to be orthogonal to this discussion.   Indeed, the question
> of dynamic/static is largely irrelevant to a discussion of what operations we
> want to police, except insofar as certain checks might require information
> which isn't available to a (feasible) static theorem prover.

Sometimes the things you want to check are emergent properties
of a progam rather than local properties. I don't see how runtime
checks can do anything with these properties, at least not without
a formal framework. An example is deadlock freedom. There
exist type systems that can prove code free of deadlock or
race conditions. How woud you write a runtime check for that?


Marshall