Joe Marshall <[EMAIL PROTECTED]> wrote:
> They *do* have a related meaning. Consider this code fragment:
> (car "a string")
My feeling is that this code is obviously wrong. It is so obviously
wrong, in fact, that the majority of automated error detection systems,
if written for Lisp, would probably manage to identify it as wrong at
some point. This includes the Lisp runtime. So far, I haven't
mentioned types.
> A string is *not* a valid argument to CAR. Ask anyone why and
> they will tell you `It's the wrong type.'
Indeed, they will. We're assuming, of course that they know a little
Lisp... otherwise, it may be entirely reasonable for someone to expect
that (car "a string") is 'a' and (cdr "a string") is " string"... but
I'll ignore that, even though I haven't yet convinced myself that it's
not relevant to why this is colloquially considered a type error.
I believe that in this sense, the 'anyone' actually means "type" in the
sense that you mean "type". The fact that a static type system detects
this error is somewhat coincidental (except for the fact that, again,
any general error-detection scheme worth its salt probably detects this
error), and orthogonal to whether it is considered a type error by our
hypothetical 'anyone'.
> Both `static typing' and `dynamic typing' (in the colloquial sense) are
> strategies to detect this sort of error.
I will repeat that static typing is a strategy for detecting errors in
general, on the basis of tractable syntactic methods. There are some
types of errors that are easier to detect in such a system than
others... but several examples have been given of problems solved by
static type systems that are not of the colloquial "It's the wrong
type" variety that you mention here. The examples so far have included
detecting division by zero, or array bounds checking. Other type
systems can check dimensionality (correct units).
Another particularly interesting example may be the following from
Ocaml:
let my_sqrt x = if x < 0.0 then None else Some(sqrt(x));;
Then, if I attempt to use my_sqrt in a context that requires a float,
the compiler will complain about a type violation, since the type of the
expression is "float option". So this is a type error *in Ocaml*, but
it's not the kind of thing that gets intuitively classified as a type
error. In fact, it's roughly equivalent to a NullPointerException at
runtime in Java, and few Java programmers would consider a
NullPointerException to be somehow "actually a type error" that the
compiler just doesn't catch. In this case, when the error appears in
Ocaml, it appears to be "obviously" a type error, but that's only
because the type system was designed to catch some class of program
errors, of which this is a member.
> It's hardly mythical. (car "a string") is obviously an error and you
> don't need a static type system to know that.
Sure. The question is whether it means much to say that it's a "type
error". So far, I'd agree with either of two statements, depending on
the usage of the word "type":
a) Yes, it means something, but Torben's definition of a static type
system was wrong, because static type systems are not specifically
looking for type errors.
or
b) No, "type error" just means "error that can be caught by the type
system", so it is circular and meaningless to use the phrase in defining
a kind of type system.
> I mean that this has been argued time and time again in comp.lang.lisp
> and probably the other groups as well.
My apologies, then. It has not been discussed so often in any newsgroup
that I followed up until now, though Marshall has now convinced me to
read comp.lang.functional, so I might see these endless discussions from
now on.
> In fact, we become rather confused when you say `a
> correctly typed program cannot go wrong at runtime' because we've seen
> plenty of runtime errors from code that is `correctly typed'.
Actually, I become a little confused by that as well. I suppose it
would be true of a "perfect" static type system, but I haven't seen one
of those yet. (Someone did email me earlier today to point out that the
type system of a specification language called LOTOS supposedly is
perfect in that sense, that every correctly typed program is also
correct, but I've yet to verify this for myself. It seems rather
difficult to believe.)
Unless I suddenly have some kind of realization in the future about the
feasibility of a perfect type system, I probably won't make that
statement that you say confuses you.
> > An attempt to generalize the definition of "type" from programming
> > language type theory to eliminate the requirement that they are
> > syntactic in nature yields something meaningless. Any concept of
> > "type" that is not syntactic is a completely different thing from
> > static types.
>
> Agreed. That is why there is the qualifier `dynamic'. This indicates
> that it is a completely different thing from static types.
If we agree about this, then there is no need to continue this
discussion. I'm not sure we do agree, though, because I doubt we'd be
right here in this conversation if we did.
This aspect of being a "completely different thing" is why I objected to
Torben's statement of the form: static type systems detect type
violations at compile time, whereas dynamic type systems detect type
violations at runtime. The problem with that statement is that "type
violations" means different things in the first and second half, and
that's obscured by the form of the statement. It would perhaps be
clearer to say something like:
Static type systems detect some bugs at compile time, whereas
dynamic type systems detect type violations at runtime.
Here's one interesting consequence of the change. It is easy to
recognize that static and dynamic type systems are largely orthogonal to
each other in the sense above. Java, for example (since that's one of
the newsgroups on the distribution list for this thread), restricting
the field of view to reference types for simplicity's sake, clearly has
both a very well-developed static type system, and a somewhat well-
developed dynamic type system. There are dynamic "type" errors that
pass the compiler and are caught by the runtime; and there are errors
that are caught by the static type system. There is indeed considerable
overlap involved, but nevertheless, neither is made redundant. In fact,
one way of understanding the headaches of Java 1.5 generics is to note
that the two different meanings of "type errors" are no longer in
agreement with each other!
> We're all rubes here, so don't try to educate us with your
> high-falutin' technical terms.
That's not my intention.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
--
http://mail.python.org/mailman/listinfo/python-list
