What is a type error?

[Chris Uppal]

Chris Smith wrote:

[me:]
> > 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.

That was the point of my first sentence (quoted above).  I take it, and I
assumed that you shared my view, that there is no single "the" type system -- 
that /a/ type system will yield judgements on matters which it has been
designed to judge.  So unless we either nominate a specific type system or
choose what judgements we want to make (today) any discussion of types is
necessarily parameterised on the class(es) of <Judgements>.  So, I don't -- 
can't -- say /which/ judgements my "dynamic type systems" will make.  They may
be about nullablity, they may be about traditional "type", they may be about
mutability...

When we look at a specific language (and its implementation), then we can
induce the logic(s) that whatever dynamic checks it applies define.
Alternatively we can consider other "dynamic type systems" which we would like
to formalise and mechanise, but which are not built into our language of
choice.


> We also haven't defined what happens if that verification
> fails.

True, and a good point.  But note that it only applies to systems which are
actually implemented in code (or which are intended to be so).

As a first thought, I suggest that a "dynamic type system" should specify a
replacement action (which includes, but is not limited to, terminating
execution).  That action is taken /instead/ of the rejected one.  E.g. we don't
actually read off the end of the array, but instead a signal is raised. (An
implementation might, in some cases, find it easier to implement the checks by
allowing the operation to fail, and then backtracking to "pretend" that it had
never happened, but that's irrelevant here).  The replacement action must -- of
course -- be valid according to the rules of the type system.

Incidentally, using that idea, we get a fairly close analogy to the difference
between strong and weak static type systems.  If the "dynamic type system"
doesn't specify a valid replacement action, or if that action is not guaranteed
to be taken, then it seems that the type system or the language implementation
is "weak" in very much the same sort of way as -- say -- the 'C' type system is
weak and/or weakly enforced.

I wonder whether that way of looking at it -- the "error" never happens since
it is replaced by a valid operation -- puts what I want to call dynamic type
systems onto a closer footing with static type systems.  Neither allows the
error to occur.

(Of course, /I/ -- the programmer -- have made a type error, but that's
different thing.)


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

My only objections to this are:

a) I /want/ to use the word "type" to describe the kind of reasoning I do (and
some of the mistakes I make)

b) I want to separate the systems of reasoning (whether formal or informal,
static or dynamic, implemented or merely conceptual, and /whatever/ we call 'em
;-) from the language semantics.  I have no objection to <some type system>
being used as part of a language specification, but I don't want to restrict
types to that.


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

Sorry, I wasn't clear.  I was thinking here of my internal analysis (which I
want to call a type system too).  Most of what I was trying to say is that I
don't expect a "dynamic type system" to be complete, any more than a static
one.   I also wanted to emphasise that I am happy to talk about type systems
(dynamic or not) which have not been implemented as code (so they yield
judgements, and provide a framework for understanding the program, but nothing
in the computer actually checks them for me).


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

Have I answered that now ?  /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.

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.

    -- chris