What is a type error?

java-programmer, What is a type error? David Hopwood <email***@***.com> wrote:
> Typical programming languages have many kinds of semantic error that can occur
> at run-time: null references, array index out of bounds, assertion failures,
> failed casts, "message not understood", ArrayStoreExceptions in Java,
> arithmetic overflow, divide by zero, etc.
>
> Conventionally, some of these errors are called "type errors" and some are
> not. But there seems to be little rhyme or reason to this categorization, as
> far as I can see. If in a particular language, both array index bounds errors
> and "message not understood" can occur at run-time, then there's no objective
> reason to call one a type error and the other not. Both *could* potentially
> be caught by a type-based analysis in some cases, and both *are not* caught
> by such an analysis in that language.

Incidentally, yes! Filtering out the terminology stuff [as hard as this
may be to believe on USENET where half the world seems to be trolls, I
really was not so aware when I originally posted of how some communities
use terminology and where the motivations come from], this was my
original point. In the static sense, there is no such thing as a type
error; only an error that's caught by a type system. I don't know if
the same can be said of dynamic types. Some people here seem to be
saying that there is a universal concept of "type error" in dynamic
typing, but I've still yet to see a good precise definition (nor a good
precise definition of dynamic typing at all).

In either case it doesn't make sense, then, to compare how static type
systems handle type errors versus how dynamic systems handle type
errors. That's akin to asking how comparing how much many courses are
offered at a five star restaurant versus how many courses are offered by
the local university. (Yes, that's an exaggeration, of course. The
word "type" in the static/dynamic typing world at least has a closer to
common root.)

> A more consistent terminology would reserve "type error" for errors that
> occur when a typechecking/inference algorithm fails, or when an explicit
> type coercion or typecheck fails.

I am concerned as to whether that actually would turn out to have any
meaning.

If we are considering array length bounds checking by type systems (and
just to confuse ourselves, by both static and dynamic type systems),
then is the error condition that gets raised by the dynamic system a
type error? Certainly, if the system keeps track of the fact that this
is an array of length 5, and uses that information to complain when
someone tries to treat the array as a different type (such as an array
of length >= 7, for example), certainly that's a type error, right?
Does the reference to the seventh index constitute an "explicit" type
coercion? I don't know. It seems pretty explicit to me, but I suspect
some may not agree.

The same thing would certainly be a type error in a static system, if
indeed the static system solved the array bounds problem at all.

While this effort to salvage the term "type error" in dynamic languages
is interesting, I fear it will fail. Either we'll all have to admit
that "type" in the dynamic sense is a psychological concept with no
precise technical definition (as was at least hinted by Anton's post
earlier, whether intentionally or not) or someone is going to have to
propose a technical meaning that makes sense, independently of what is
meant by "type" in a static system.

> In the terminology I'm suggesting, the object has no type in this language
> (assuming we're talking about a Smalltalk-like language without any type system
> extensions).

I suspect you'll see the Smalltalk version of the objections raised in
response to my post earlier. In other words, whatever terminology you
think is consistent, you'll probably have a tough time convincing
Smalltalkers to stop saying "type" if they did before. If you exclude
"message not understood" as a type error, then I think you're excluding
type errors from Smalltalk entirely, which contradicts the psychological
understanding again.

--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation

java-programmer >> What is a type error? Chris Smith wrote:

> While this effort to salvage the term "type error" in dynamic languages
> is interesting, I fear it will fail. Either we'll all have to admit
> that "type" in the dynamic sense is a psychological concept with no
> precise technical definition (as was at least hinted by Anton's post
> earlier, whether intentionally or not) or someone is going to have to
> propose a technical meaning that makes sense, independently of what is
> meant by "type" in a static system.

What about this: You get a type error when the program attempts to
invoke an operation on values that are not appropriate for this operation.

Examples: adding numbers to strings; determining the string-length of a
number; applying a function on the wrong number of parameters; applying
a non-function; accessing an array with out-of-bound indexes; etc.

>> In the terminology I'm suggesting, the object has no type in this language
>> (assuming we're talking about a Smalltalk-like language without any type system
>> extensions).
>
> I suspect you'll see the Smalltalk version of the objections raised in
> response to my post earlier. In other words, whatever terminology you
> think is consistent, you'll probably have a tough time convincing
> Smalltalkers to stop saying "type" if they did before. If you exclude
> "message not understood" as a type error, then I think you're excluding
> type errors from Smalltalk entirely, which contradicts the psychological
> understanding again.

Sending a message to an object that does not understand that message is
a type error. The "message not understood" machinery can be seen either
as a way to escape from this type error in case it occurs and allow the
program to still do something useful, or to actually remove (some)
potential type errors. Which view you take probably depends on what your
concrete implementation of "message not understood" does. For example,
if it simply forwards the message to another object that is known to be
able to respond to it, then you remove a potential type error; however,
if it pops up a dialog box to ask the user how to continue from here, it
is still a type error, but just gives you a way to deal with it at runtime.

Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

java-programmer >> What is a type error? Pascal Costanza <email***@***.com> writes:

> Chris Smith wrote:
>
>> While this effort to salvage the term "type error" in dynamic
>> languages is interesting, I fear it will fail. Either we'll all
>> have to admit that "type" in the dynamic sense is a psychological
>> concept with no precise technical definition (as was at least hinted
>> by Anton's post earlier, whether intentionally or not) or someone is
>> going to have to propose a technical meaning that makes sense,
>> independently of what is meant by "type" in a static system.
>
> What about this: You get a type error when the program attempts to
> invoke an operation on values that are not appropriate for this
> operation.
>
> Examples: adding numbers to strings; determining the string-length of
> a number; applying a function on the wrong number of parameters;
> applying a non-function; accessing an array with out-of-bound indexes;
> etc.

Yes, the phrase "runtime type error" is actually a misnomer. What one
usually means by that is a situation where the operational semantics
is "stuck", i.e., where the program, while not yet arrived at what's
considered a "result", cannot make any progress because the current
configuration does not match any of the rules of the dynamic
semantics.

The reason why we call this a "type error" is that such situations are
precisely the ones we want to statically rule out using sound static
type systems. So it is a "type error" in the sense that the static
semantics was not strong enough to rule it out.

> Sending a message to an object that does not understand that message
> is a type error. The "message not understood" machinery can be seen
> either as a way to escape from this type error in case it occurs and
> allow the program to still do something useful, or to actually remove
> (some) potential type errors.

I disagree with this. If the program keeps running in a defined way,
then it is not what I would call a type error. It definitely is not
an error in the sense I described above.

java-programmer >> What is a type error? Pascal Costanza <email***@***.com> wrote:
> What about this: You get a type error when the program attempts to
> invoke an operation on values that are not appropriate for this operation.
>
> Examples: adding numbers to strings; determining the string-length of a
> number; applying a function on the wrong number of parameters; applying
> a non-function; accessing an array with out-of-bound indexes; etc.

Hmm. I'm afraid I'm going to be picky here. I think you need to
clarify what is meant by "appropriate". If you mean "the operation will
not complete successfully" as I suspect you do, then we're closer... but
this little snippet of Java (HORRIBLE, DO NOT USE!) confuses the matter
for me:

int i = 0;

try
{
while (true) process(myArray[i++]);
}
catch (IndexOutOfBoundsException e) { }

That's an array index from out of bounds that not only fails to be a
type error, but also fails to be an error at all! (Don't get confused
by Java's having a static type system for other purposes... we are
looking at array indexing here, which Java checks dynamically. I would
have used a dynamically typed language, if I could have written this as
quickly.)

I'm also unsure how your definition above would apply to languages that
do normal order evaluation, in which (at least in my limited brain) it's
nearly impossible to break down a program into sequences of operations
on actual values. I suppose, though, that they do eventually happen
with primitives at the leaves of the derivation tree, so the definition
would still apply.

--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation

java-programmer >> What is a type error? Chris Smith wrote:

> Some people here seem to be
> saying that there is a universal concept of "type error" in dynamic
> typing, but I've still yet to see a good precise definition (nor a good
> precise definition of dynamic typing at all).

How about this, at least as a strawman:

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 don't mean to imply that an operation /must/ not be checked until it is
invoked (although a particular logic/implementation might not do so). For
instance an out-of-bound array access might be rejected:
When the attempt was made to read that slot.
When, in the surrounding code, it first became
unavoidable that the about read /would/ be reached.
When the array was first passed to a function which
/might/ read that slot.
...and so on...

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

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.

> I suspect you'll see the Smalltalk version of the objections raised in
> response to my post earlier. In other words, whatever terminology you
> think is consistent, you'll probably have a tough time convincing
> Smalltalkers to stop saying "type" if they did before. If you exclude
> "message not understood" as a type error, then I think you're excluding
> type errors from Smalltalk entirely, which contradicts the psychological
> understanding again.

Taking Smalltalk /specifically/, there is a definite sense in which it is
typeless -- or trivially typed -- in that in that language there are no[*]
operations which are forbidden[**], and none which might not be invoked
deliberately (e.g. I have code which deliberately reads off the end of a
container object -- just to make sure I raise the "right" error for that
container, rather than raising my own error). But, on the other hand, I do
still want to talk of type, and type system, and type errors even when I
program Smalltalk, and when I do I'm thinking about "type" in something like
the above sense.

-- chris

[*] I can't think of any offhand -- there may be a few.

[**] 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.

java-programmer >> What is a type error? Chris Uppal <email***@***.com> 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

java-programmer >> What is a type error?

> Chris Smith wrote:
>>I suspect you'll see the Smalltalk version of the objections raised in
>>response to my post earlier. In other words, whatever terminology you
>>think is consistent, you'll probably have a tough time convincing
>>Smalltalkers to stop saying "type" if they did before. If you exclude
>>"message not understood" as a type error, then I think you're excluding
>>type errors from Smalltalk entirely, which contradicts the psychological
>>understanding again.
>
Chris Uppal wrote:

>
> Taking Smalltalk /specifically/, there is a definite sense in which it is
> typeless -- or trivially typed -- in that in that language there are no[*]
> operations which are forbidden[**],

Come one Chris U. One has to distinguish an attempt to invoke an
operation with it being carried out. There is nothing in Smalltalk to
stop one attempting to invoke any "operation" on any object. But one
can only actually carry-out operations on objects that implement them.
So, apart from the argument about inadvertent operation name overloading
(which is important, but avoidable), Smalltalk is in fact
strongly-typed, but not statically strongly-typed.

--
_______________,,,^..^,,,____________________________
Eliot Miranda Smalltalk - Scene not herd

java-programmer >> What is a type error? Eliot Miranda wrote:
> can only actually carry-out operations on objects that implement them.

Execpt that every operation is implemented by every object in Smalltalk.
Unless you specify otherwise, the implementation of every method is to
call the receiver with doesNotUnderstand. (I don't recall whether the
class of nil has a special rule for this or whether it implements
doesNotUnderstand and invokes the appropriate "don't send messages to
nil" method.)

There are a number of Smalltalk extensions, such as
multiple-inheritance, that rely on implementing doesNotUnderstand.

--
Darren New / San Diego, CA, USA (PST)
Native Americans used every part
of the buffalo, including the wings.

java-programmer >> What is a type error? Matthias Blume wrote:
> Pascal Costanza <email***@***.com> writes:
>
>> Chris Smith wrote:
>>
>>> While this effort to salvage the term "type error" in dynamic
>>> languages is interesting, I fear it will fail. Either we'll all
>>> have to admit that "type" in the dynamic sense is a psychological
>>> concept with no precise technical definition (as was at least hinted
>>> by Anton's post earlier, whether intentionally or not) or someone is
>>> going to have to propose a technical meaning that makes sense,
>>> independently of what is meant by "type" in a static system.
>> What about this: You get a type error when the program attempts to
>> invoke an operation on values that are not appropriate for this
>> operation.
>>
>> Examples: adding numbers to strings; determining the string-length of
>> a number; applying a function on the wrong number of parameters;
>> applying a non-function; accessing an array with out-of-bound indexes;
>> etc.
>
> Yes, the phrase "runtime type error" is actually a misnomer. What one
> usually means by that is a situation where the operational semantics
> is "stuck", i.e., where the program, while not yet arrived at what's
> considered a "result", cannot make any progress because the current
> configuration does not match any of the rules of the dynamic
> semantics.
>
> The reason why we call this a "type error" is that such situations are
> precisely the ones we want to statically rule out using sound static
> type systems. So it is a "type error" in the sense that the static
> semantics was not strong enough to rule it out.
>
>> Sending a message to an object that does not understand that message
>> is a type error. The "message not understood" machinery can be seen
>> either as a way to escape from this type error in case it occurs and
>> allow the program to still do something useful, or to actually remove
>> (some) potential type errors.
>
> I disagree with this. If the program keeps running in a defined way,
> then it is not what I would call a type error. It definitely is not
> an error in the sense I described above.

If your view of a running program is that it is a "closed" system, then
you're right. However, maybe there are several layers involved, so what
appears to be a well-defined behavior from the outside may still be
regarded as a type error internally.

A very obvious example of this is when you run a program in a debugger.
There are two levels involved here: the program signals a type error,
but that doesn't mean that the system as a whole is stuck. Instead, the
debugger takes over and offers ways to deal with the type error. The
very same program run without debugging support would indeed simply be
stuck in the same situation.

So to rephrase: It depends on whether you use the "message not
understood" machinery as a way to provide well-defined behavior for the
base level, or rather as a means to deal with an otherwise unanticipated
situation. In the former case it extends the language to remove certain
type errors, in the latter case it provides a kind of debugging facility
(and it indeed may be a good idea to deploy programs with debugging
facilities, and not only use debugging tools at development time).

This is actually related to the notion of reflection, as coined by Brian
C. Smith. In a reflective architecture, you distinguish between various
interpreters, each of which interprets the program at the next level. A
debugger is a program that runs at a different level than a base program
that it debugs. However, the reflective system as a whole is "just" a
single program seen from the outside (with one interpreter that runs the
whole reflective tower). This distinction between the internal and the
external view of a reflective system was already made by Brian Smith.

Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

java-programmer >> What is a type error? Chris Smith wrote:
> Pascal Costanza <email***@***.com> wrote:
>> What about this: You get a type error when the program attempts to
>> invoke an operation on values that are not appropriate for this operation.
>>
>> Examples: adding numbers to strings; determining the string-length of a
>> number; applying a function on the wrong number of parameters; applying
>> a non-function; accessing an array with out-of-bound indexes; etc.
>
> Hmm. I'm afraid I'm going to be picky here. I think you need to
> clarify what is meant by "appropriate".

No, I cannot be a lot clearer here. What operations are appropriate for
what values largely depends on the intentions of a programmer. Adding a
number to a string is inappropriate, no matter how a program behaves
when this actually occurs (whether it continues to execute the operation
blindly, throws a continuable exception, or just gets stuck).

> If you mean "the operation will
> not complete successfully" as I suspect you do, then we're closer...

No, we're not. You're giving a purely technical definition here, that
may or may not relate to the programmer's (or "designer's")
understanding of the domain.

Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

java-programmer >> What is a type error? Eliot Miranda wrote:

[me:]
> > Taking Smalltalk /specifically/, there is a definite sense in which it
> > is typeless -- or trivially typed -- in that in that language there are
> > no[*] operations which are forbidden[**],
>
> Come one Chris U. One has to distinguish an attempt to invoke an
> operation with it being carried out. There is nothing in Smalltalk to
> stop one attempting to invoke any "operation" on any object. But one
> can only actually carry-out operations on objects that implement them.
> So, apart from the argument about inadvertent operation name overloading
> (which is important, but avoidable), Smalltalk is in fact
> strongly-typed, but not statically strongly-typed.

What are you doing /here/, Eliot, this is Javaland ? Smalltalk is thatta
way ->

;-)

But this discussion has been all about /whether/ it is ok to apply the notion
of (strong) typing to what runtime-checked languages do. We all agree that
the checks happen, but the question is whether it is
reasonable/helpful/legitimate to extend the language of static checking to the
dynamic case. (I'm on the side which says yes, but good points have been made
against it).

The paragraph you quoted doesn't represent most of what I have been saying --
it was just a side-note looking at one small aspect of the issue from a
different angle.

-- chris

java-programmer >> What is a type error? 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

java-programmer >> What is a type error? Chris Uppal <email***@***.com> wrote:
> 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.

Yes, I definitely agree.

My point was that if you leave BOTH the "something" and the response to
verification failure undefined, then your definition of a dynamic type
system is a generalization of the definition of a conditional
expression. That is (using Java),

if (x != 0) y = 1 / x;
else y = 999999999;

is not all that much different from (now restricting to Java):

try { y = 1 / x; }
catch (ArithmeticException e) { y = 999999999; }

So is one of them a use of a dynamic type system, where the other is
not?

> Incidentally, using that idea, we get a fairly close analogy to the difference
> between strong and weak static type systems.

I think, actually, that the analogy of the strong/weak distinction
merely has to do with how much verification is done. But then, I
dislike discussion of strong/weak type systems in the first place. It
doesn't make any sense to me to say that we verify something and then
don't do anything if the verification fails. In those cases, I'd just
say that verification doesn't really exist or is incorrectly
implemented. Of course, this would make the type system weaker.

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

Perhaps. I'm thinking some things over before I respond to Anton. I'll
do that first, and some of my thoughts there may end up being relevant
to this question.

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

In the pragmatic sense of this desire, I'd suggest that a way to
characterize this is that your type system is a set of changes to the
language semantics. By applying them to a language L, you obtain a
different language L' which you can then use. If your type system has
any impact on the set of programs accepted by the language (static
types) or on any observable behavior which they exhibit (dynamic types),
then I can't see a justification for claiming that the result is the
same language; and if it does not, then the whole exercise is silly.

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

Indeed, that is orthogonal to the discussion from the perspective of
static types. If you are proposing that it is also orthogonal with
respect to dynamic types, that will be a welcome step toward our goal of
a grand unified type theory, I suppose. I have heard from others in
this thread that they don't believe so. I am also interested in your
response to the specific example involving an if statement at the
beginning of this reply.

--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation

java-programmer >> What is a type error?

Darren New wrote:

> Eliot Miranda wrote:
>
>> can only actually carry-out operations on objects that implement them.
>
>
> Execpt that every operation is implemented by every object in Smalltalk.

No they are not. Objects implement the methods defined by their class
and (inherit) those implemented by the class's superclasses. Note that
classes do _not_ have to inherit from Object, and so one can create
classes that implement no methods at all. It is a common idiom to
create a class that implements two methods, an initialization method and
a doesNotUnderstand: method, so create a transparent proxy that
intercepts any and all messages sent to it other than the initialization
method (*).

[(*) With suitable hackery (since Smalltalk gives access to the
execution stack through thisContext) one can also invoke
doesNotUnderstand: if the initialization message is sent from any object
other than the class.]

> Unless you specify otherwise, the implementation of every method is to
> call the receiver with doesNotUnderstand. (I don't recall whether the
> class of nil has a special rule for this or whether it implements
> doesNotUnderstand and invokes the appropriate "don't send messages to
> nil" method.)

No. The run-time error of trying to invoke an operation that isn't
implemented by an object is to send the doesNotUnderstand: message.
This is another attempt to invoke an operation, i.e. whatever the
object's doesNotUnderstand: method is, if any. If the object doesn't
implement doesNotUnderstand:, which is quite possible, then the system,
will likely crash (either with an out of memory error as it goes into
infinite recursion) or hang (looping attempting to find an
implementation of doesNotUnderstand:).

> There are a number of Smalltalk extensions, such as
> multiple-inheritance, that rely on implementing doesNotUnderstand.

Which has nothing to do with the separation between message send and
method invocation, or the fact that doesNotUnderstand: is a message
send, not a hard call of a given doesNotUnderstand: method.
--
_______________,,,^..^,,,____________________________
Eliot Miranda Smalltalk - Scene not herd

java-programmer >> What is a type error? Eliot Miranda wrote:
> classes do _not_ have to inherit from Object,

I was unaware of this subtlety. Thanks!

--
Darren New / San Diego, CA, USA (PST)
Native Americans used every part
of the buffalo, including the wings.

java-programmer >> What is a type error? Chris Smith wrote:

> But then, I
> dislike discussion of strong/weak type systems in the first place. It
> doesn't make any sense to me to say that we verify something and then
> don't do anything if the verification fails. In those cases, I'd just
> say that verification doesn't really exist or is incorrectly
> implemented.

Hmm, that seems to make what we are doing when we run some tests dependent on
what we do when we get the results. If I run a type inference algorithm on
some of my Smalltalk code, and it tells me that something is type-incorrect,
then I think I'd like to be able to use the same words for the checking
regardless of whether, after due consideration, I decide to change my code, or
that it is OK as-is. Minor point, though...

Anyway:

> if (x != 0) y = 1 / x;
> else y = 999999999;
>
> is not all that much different from (now restricting to Java):
>
> try { y = 1 / x; }
> catch (ArithmeticException e) { y = 999999999; }
>
> So is one of them a use of a dynamic type system, where the other is
> not?

My immediate thought is that the same question is equally applicable (and
equally interesting -- i.e. no simple answer ;-) for static typing. Assuming
Java's current runtime semantics, but positing different type checkers, we can
get several answers.

A] Trivial: neither involves the type system at all. What we are seeing
is a runtime check (not type check) correctly applied, or made unnecessary by
conditional code. And, obviously we can take the same line for the "dynamic
type checking" -- i.e. that no type checking is involved.

B] More interesting, we could extend Java's type system with a NotZero
numeric type (or rather, about half a dozen such), and decree that 1 / x was
only legal if
x : NotZero
Under that type system, neither of the above would be type legal, assuming x is
declared int. Or both would be legal if it was declared NotZero -- but in both
cases there'd be a provably unnecessary runtime check. The nearest "dynamic
type system" equivalent would be quite happy with x : int. For the first
example, the runtime checks would never fire (though they would execute). For
the second the runtime "type" might come into play, and if it did, then the
assignment of 999999999 would take place /because/ the illegal operation (which
can be thought of as casting 0 to NotZero) had been replaced by a specific
legal one (throwing an ArithmeticException in this case).

C] A different approach would be to type the execution, instead of the value,
so we extend Java's type system so that:
1 / x
had type (in part) <computation which can throw ArithmeticException>. The
first example as a whole then would also have (in part) that type, and the
static type system would deem that illegal. The second example, however, would
be type-legal. I hope I don't seem to be fudging the issue, but I don't really
think this version has a natural "dynamic type system" equivalent -- what could
the checker check ? It would see an attempt to throw an exception from a place
where that's not legal, but it wouldn't make a lot of sense to replace it with
an IllegalExceptionException ;-)

D] Another possibility would be a static type checker after the style of [B]
but extended so that it recognised the x != 0 guard as implicitly giving x :
NonZero. In that case, again, the first example is static type-correct but the
second is not. In this case the corresponding "dynamic type system" could, in
principle, avoid testing x for zero the second time. I don't know whether that
would be worth the effort to implement. In the second example, just as in
[B], the reason the program doesn't crash when x == 0 is that the "dynamic type
system" has required that the division be replaced with a throw.

One could go further (merge [B] and [C], or [C] and [D] perhaps), but I don't
think it adds much, and anyway I'm getting a bit bored.... (And also getting
sick of putting scare quotes around "dynamic type system" every time ;-)

Personally, of the above, I find [B] most appealing.

-- chris

java-programmer >> What is a type error? 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

java-programmer >> What is a type error? Chris Uppal <email***@***.com> wrote:
> > if (x != 0) y = 1 / x;
> > else y = 999999999;
> >
> > is not all that much different from:
> >
> > try { y = 1 / x; }
> > catch (ArithmeticException e) { y = 999999999; }

> My immediate thought is that the same question is equally applicable (and
> equally interesting -- i.e. no simple answer ;-) for static typing.

I don't see that. Perhaps I'm missing something. If I were to define a
type system for such a language that is vaguely Java-based but has
NotZero as a type, it would basically implement your option [D], and
contain the following rules:

1. NotZero is a subtype of Number
2. Zero is a subtype of Number

3. If x : Number and k : Zero, then "if (x != k) a else b" is well-typed
iff "a" is well-typed when the type-environment is augmented with the
proposition "x : NotZero" and "b" is well-typed when the type-
environment is augmented with the new proposition "x : Zero".

Yes, I know that Java doesn't do this right now in similar places (e.g.,
instanceof), and I don't know why not. This kind of thing isn't even
theoretically interesting at all, except that it makes the proof of
type-soundness look different. As far as I can see, it ought to be
second-nature in developing a type system for a language.

In that case, the first example is well-typed, and also runs as
expected. The second bit of code is not well-typed, and thus
constitutes a type error. The way we recognize it as a type error,
though, is in the fact that the compiler aborts while checking the
typing relation, rather than because of the kind of problem prevented.
Of course, it would be possible to build a static type system in which
different things are true. For example, Java itself is a system in
which both terms are well-typed.

From a dynamic type perspective, the litany of possibilities doesn't
really do much for defining a dynamic type system, which I thought was
our goal in this bit of the thread. I may not have been clear enough
that I was look for an a priori grounds to classify these two cases by
the definition. I was assuming the existing behavior of Java, which
says that both accomplish the same thing and react in the same way, yet
intuitively we seem to think of one as a type error being "solved",
whereas the other is not.

Anyway, you just wrote another message that is far closer to what I feel
we ought to be thinking about than my question here... so I will get to
reading that one, and perhaps we can take up this point later when and
if it is appropriate.

--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation

java-programmer >> What is a type error? Pascal Costanza wrote:
> Chris Smith wrote:
>
>> While this effort to salvage the term "type error" in dynamic
>> languages is interesting, I fear it will fail. Either we'll all have
>> to admit that "type" in the dynamic sense is a psychological concept
>> with no precise technical definition (as was at least hinted by
>> Anton's post earlier, whether intentionally or not) or someone is
>> going to have to propose a technical meaning that makes sense,
>> independently of what is meant by "type" in a static system.
>
> What about this: You get a type error when the program attempts to
> invoke an operation on values that are not appropriate for this operation.
>
> Examples: adding numbers to strings; determining the string-length of a
> number; applying a function on the wrong number of parameters; applying
> a non-function; accessing an array with out-of-bound indexes; etc.

This makes essentially all run-time errors (including assertion failures,
etc.) "type errors". It is neither consistent with, nor any improvement
on, the existing vaguely defined usage.

--
David Hopwood <email***@***.com>

java-programmer >> What is a type error? David Hopwood wrote:
> Pascal Costanza wrote:
>> Chris Smith wrote:
>>
>>> While this effort to salvage the term "type error" in dynamic
>>> languages is interesting, I fear it will fail. Either we'll all have
>>> to admit that "type" in the dynamic sense is a psychological concept
>>> with no precise technical definition (as was at least hinted by
>>> Anton's post earlier, whether intentionally or not) or someone is
>>> going to have to propose a technical meaning that makes sense,
>>> independently of what is meant by "type" in a static system.
>> What about this: You get a type error when the program attempts to
>> invoke an operation on values that are not appropriate for this operation.
>>
>> Examples: adding numbers to strings; determining the string-length of a
>> number; applying a function on the wrong number of parameters; applying
>> a non-function; accessing an array with out-of-bound indexes; etc.
>
> This makes essentially all run-time errors (including assertion failures,
> etc.) "type errors". It is neither consistent with, nor any improvement
> on, the existing vaguely defined usage.

Nope. This is again a matter of getting the levels right.

Consider division by zero: appropriate arguments for division are
numbers, including the zero. The dynamic type check will typically not
check whether the second argument is zero, but will count on the fact
that the processor will raise an exception one level deeper.

This is maybe better understandable in user-level code. Consider the
following class definition:

class Person {
String name;
int age;

void buyPorn() {
if (< this.age 18) throw new AgeRestrictionException();
...
}
}

The message p.buyPorn() is a perfectly valid message send and will pass
both static and dynamic type tests (given p is of type Person in the
static case). However, you will still get a runtime error.

Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/