What is Expressiveness in a Computer Language

[George Neuner]

On Sun, 25 Jun 2006 13:42:45 +0200, Joachim Durchholz
<jo at durchholz.org> wrote:

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

Yes ... the problem is undecidable and that can be statically checked.
But the result is that your program won't compile even if it can be
proved at runtime that an illegal value would never be possible.


>Undecidability can always be avoided by adding annotations, but of 
>course that would be gross overkill in the case of index type widening.

Just what sort of type annotation will convince a compiler that a
narrowing conversion which could produce an illegal value will, in
fact, never produce an illegal value?

[Other than "don't check this" of course.]

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