What is Expressiveness in a Computer Language

[Joachim Durchholz]

George Neuner schrieb:
> The point is really that the checks that prevent these things must be
> performed at runtime and can't be prevented by any practical type
> analysis performed at compile time.  I'm not a type theorist but my
> opinion is that a static type system that could, a priori, prevent the
> problem is impossible.

No type theory is needed.
Assume that the wide index type goes into a function and the result is 
assigned to a variable fo the narrow type, and it's instantly clear that 
the problem is undecidable.
Undecidability can always be avoided by adding annotations, but of 
course that would be gross overkill in the case of index type widening.

Regards,
Jo