What is a type error?

[David Hopwood]

Chris Smith wrote:
> David Hopwood <david.nospam.hopwood at blueyonder.co.uk> wrote:
> 
>>1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
>>than types.
> 
> One of us is missing the other's meaning here.  If 3 to 5 were expressed 
> as assertions rather than types, then the type system would become 
> incomplete, requiring frequent runtime-checked type ascriptions to 
> prevent it from becoming impossible to write software.  That's not my 
> idea of a usable language.

Maybe I'm not understanding what you mean by "complete". Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about the types of expressions.

So yes, some assertions would need to be checked at runtime (others could be
proven to always hold by a theorem prover).

Why is this a problem? The goal is not to check everything at compile time;
the goal is just to support writing correct programs.

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