[Haskell] Eliminating Array Bound Checking through Non-dependent types

[Bjorn Lisper]

( A really interesting post on static elimination of array bounds checking
by Oleg...)

Some questions and suggestions:

What is the relation to the sized types by Lars Pareto and John Hughes?

What is the relation to classical range analyses for (e.g.) array index
expressions, which have been known for a long time for imperative languages?

A program analysis like range analysis is not exact, of course: it must make
safe approximations sometimes and will sometimes say that an array index
might be out of bounds when it actually won't. In your framework, this seems
to correspond to the fact that you must verify your propositions about index
expressions. If the formulae fall into some decidable category, then they
can be verified automatically, otherwise an automatic method based on your
framework will have to give up sometimes, just like a conventional program
analysis. The formulae you give in your example are all Presburger
formulae, for which there are decision procedures, and you could use a
public domain Presburger solver like the Omega Test by Bill Pugh. Have you
though of this possibility?

Björn Lisper