What is Expressiveness in a Computer Language

[George Neuner]

On Sun, 25 Jun 2006 14:28:22 -0600, Chris Smith <cdsmith at twu.net>
wrote:

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

That was my point ... you get a program that won't compile.


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

I worked in signal and image processing for many years and those are
places where narrowing conversions are used all the time - in the form
of floating point calculations reduced to integer to value samples or
pixels, or to value or index lookup tables.  Often the same
calculation needs to be done for several different purposes.

I can know that my conversion of floating point to integer is going to
produce a value within a certain range ... but, in general, the
compiler can't determine what that range will be.  All it knows is
that a floating point value is being truncated and the stupid
programmer wants to stick the result into some type too narrow to
represent the range of possible values.

Like I said to Ben, I haven't seen any _practical_ static type system
that can deal with things like this.  Writing a generic function is
impossible under the circumstances, and writing a separate function
for each narrow type is ridiculous and a maintenance nightmare even if
they can share the bulk of the code.

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