What is Expressiveness in a Computer Language

[Greg Buchholz]

George Neuner wrote:
> You can't totally prevent it ... if the index computation involves
> types having a wider range, frequently the solution is to compute a
> wide index value and then narrow it.  But if the wider value is out of
> range for the narrow type you have a problem.
>
...snip...
>
> 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.

    I haven't been following this thread too closely, but I thought the
following article might be of interest...

Eliminating Array Bound Checking through Non-dependent types.
http://okmij.org/ftp/Haskell/types.html#branding

"There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a non-empty
list, we must give up on something significant: on data structures such
as arrays (to be replaced with nested tuples), on general recursion, on
annotation-free programming, on clarity of code, on well-supported
programming languages. That does not have to be the case. The present
messages show non-trivial examples involving native Haskell arrays,
index computations, and general recursion. All arrays indexing
operations are statically guaranteed to be safe -- and so we can safely
use an efficient unsafeAt provided by GHC seemingly for that purpose.
The code is efficient; the static assurances cost us no run-time
overhead. The example uses only Haskell98 + higher-ranked types. No new
type classes are introduced. The safety is based on: Haskell type
system, quantified type variables, and a compact general-purpose
trusted kernel."