What is a type error?

[Chris Smith]

Marcin 'Qrczak' Kowalczyk <qrczak at knm.org.pl> wrote:
> Chris Smith <cdsmith at twu.net> writes:
> >> No what happens if right here you code
> >>    b := 16;
> >> 
> >> Does that again change the type of "b"? Or is that an illegal 
> >> instruction, because "b" has the "local type" of (18..22)?
> >
> > It arranges that the expression "b" after that line (barring further 
> > changes) has type int{16..16}, which would make the later call to 
> > signContract illegal.
> 
> The assignment might be performed in a function called there, so it's
> not visible locally.

Indeed, I pointed that out a few messages ago.  That doesn't mean it's 
impossible, but it does mean that it's more difficult.  Eventually, the 
compiler will have to stop checking something, somewhere.  It certainly 
doesn't, though, have to stop at the first functional abstraction it 
comes to.  The ways that a function modifies the global application 
state certainly ought to be considered part of the visible API of that 
function, and if we could reasonably express that in a type system, then 
that's great!  Granted, designing such a type system for an arbitrary 
imperative language seems a little scary.

> Propagating constraints from conditionals is not applicable to mutable
> variables, at least not easily.

Certainly it worked in the code from my original response to George.  
Regardless of whether it might not work in more complex scenarios (and I 
think it could, though it would be more challenging), it still doesn't 
seem reasonable to assert that the technique is not applicable.  If the 
type system fails, then it fails conservatively as always, and some 
programmer annotation and runtime check is needed to enforce the 
condition.

> I think that constant bounds are not very useful at all. Most ranges
> are not known statically, e.g. a variable can span the size of an
> array.

I think you are overestimating the difficulties here.  Specialized 
language already exist that reliably (as in, all the time) move array 
bounds checking to compile time; that means that there exist at least 
some languages that have already solved this problem.  Going back to my 
handy copy of Pierce's book again, he claims that range checking is a 
solved problem in theory, and the only remaining work is in how to 
integrate it into a program without prohibitive amounts of type 
annotation.

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