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 -- http://mail.python.org/mailman/listinfo/python-list
