What is Expressiveness in a Computer Language

[Chris Smith]

George Neuner <gneuner2/@comcast.net> wrote:
> >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?

The annotation doesn't make the narrowing conversion safe; it prevents 
the narrowing conversion from happening.  If, for example, I need to 
subtract two numbers and all I know is that they are both between 2 and 
40, then I only know that the result is between -38 and 38, which may 
contain invalid array indices.  However, if the numbers were part of a 
pair, and I knew that the type of the pair was <pair of numbers, 2 
through 40, where the first number is greater than the second>, then I 
would know that the difference is between 0 and 38, and that may be a 
valid index.

Of course, the restrictions on code that would allow me to retain 
knowledge of the form [pair of numbers, 2 through 40, a > b] may be 
prohibitive.  That is an open question in type theory, as a matter of 
fact; whether types of this level of power may be inferred by any 
tractable procedure so that safe code like this may be written without 
making giving the development process undue difficulty by requiring ten 
times as much type annotations as actual code.  There are attempts that 
have been made, and they don't look too awfully bad.

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