What is a type error?

[Benjamin Franksen]

Darren New wrote:
> Chris Smith wrote:
>> Specialized
>> language already exist that reliably (as in, all the time) move array
>> bounds checking to compile time;
> 
> It sounds like this means the programmer has to code up what it means to
> index off an array, yes? Otherwise, I can't imagine how it would work.
> 
> x := read_integer_from_stdin();
> write_to_stdout(myarray[x]);
> 
> What does the programmer have to do to implement this semantic in the
> sort of language you're talking about? Surely something somewhere along
> the line has to  "fail" (for some meaning of failure) at run-time, yes?

You should really take a look at Epigram. One of its main features is that
it makes it possible not only to statically /check/ invariants, but also
to /establish/ them.

In your example, of course the program has to check the integer at runtime.
However, in a dependent type system, the type of the value returned from
the check-function can very well indicate whether it passed the test (i.e.
being a valid index for myarray) or not.

Ben