What is a type error?

[George Neuner]

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.

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

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.

George
--
for email reply remove "/" from address