What is a type error?

[Chris Smith]

Chris Uppal <chris.uppal at metagnostic.REMOVE-THIS.org> 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