What is a type error?

[David Hopwood]

George Neuner wrote:
> On Tue, 11 Jul 2006 14:59:46 GMT, David Hopwood
> <david.nospam.hopwood at blueyonder.co.uk> wrote:
> 
>>What matters is that, over the range
>>of typical programs written in the language, the value of the increased
>>confidence in program correctness outweighs the effort involved in both
>>adding annotations, and understanding whether any remaining run-time checks
>>are guaranteed to succeed.
> 
> Agreed, but ...
> 
>>Look at it this way: suppose that I *need* to verify that a program has
>>no range errors. Doing that entirely manually would be extremely tedious.
>>If the compiler can do, say, 90% of the work, and point out the places that
>>need to be verified manually, then that would be both less tedious, and
>>less error-prone.
> 
> All of this presupposes that you have a high level of confidence in
> the compiler.  I've been in software development for going in 20 years
> now and worked 10 years on high performance, high availability
> systems.  In all that time I have yet to meet a compiler ... or
> significant program of any kind ... that is without bugs, noticeable
> or not.

That's a good point. I don't think it would be an exaggeration to say
that the some of the most commonly used compilers are riddled with bugs.
gcc is a particularly bad offender, and at the moment seems to be introducing
bugs with each new version at a faster rate than they can be fixed. Sun's
javac also used to be poor in this respect, although I haven't used recent
versions of it.

One of the main reasons for this, IMHO, is that many compilers place too
much emphasis on low-level optimizations of dubious merit. For C and
Java, I've taken to compiling all non-performance-critical code without
optimizations, and that has significantly reduced the number of compiler
bugs that I see. It has very little effect on overall execution performance
(and compile times are quicker).

I don't think that over-complex type systems are the cause of more than a
small part of the compiler bug problem. In my estimation, the frequency of
bugs in different compilers *for the same language* can vary by an order of
magnitude.

> I'm a fan of static typing but the major problem I have with complex
> inferencing (in general) is the black box aspect of it.  That is, when
> the compiler rejects my code, is it really because a) I was stupid, b)
> the types are too complex, or c) the compiler itself has a bug.

Rejecting code incorrectly is much less of a problem than accepting it
incorrectly. *If* all compiler bugs were false rejections, I would say that
this would not be too much of an issue.

Unfortunately there are plenty of bugs that result in silently generating
bad code. But I don't think you can avoid that by using a language with a
simpler type system. The quality of a compiler depends much more on the
competence and attitudes of the language implementation developers, than
it does on the language itself.

[Although, choosing a language with a more quality-conscious compiler
development team doesn't necessarily help if it is compiling to C, since
then you still have to deal with C compiler bugs, but on autogenerated
code :-(.]

> It's certainly true that the vast majority of my problems are because
> I'm stupid, but I've run into actual compiler bugs far too often for my
> liking (high performance coding has a tendency to uncover them).

Yes. Cryptographic algorithms, and autogenerated code also tend to do that.

> I think I understand how to implement HM inferencing ... I haven't
> actually done it yet, but I've studied it and I'm working on a toy
> language that will eventually use it.  But HM itself is a toy compared
> to an inferencing system that could realistically handle some of the
> problems that were discussed in this and Xah's "expressiveness" thread
> (my own beef is with *static* checking of range narrowing assignments
> which I still don't believe can be done regardless of Chris Smith's
> assertions to the contrary).
> 
> It seems to me that the code complexity of such a super-duper
> inferencing system would make its bug free implementation quite
> difficult and I personally would be less inclined to trust a compiler
> that used it than one having a less capable (but easier to implement)
> system.

I don't think that the complexity of such a system would need to be
any greater than that of the optimization frameworks used by many
compilers. IIUC, what Chris Smith is suggesting is essentially equivalent
to doing type inference on the SSA form of the program.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>