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

[Conor T McBride]

Hello Oleg, hello all

I agree with you on this:

oleg at pobox.com wrote:
> 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.

However, anyone who would argue (and I'm not saying you do) that work
to try to make more advanced type systems and stronger static
guarantees more convenient and `well-supported' is not necessary
because it happens to be possible to bang out this or that example
in Haskell as it stands if you think about it hard enough, is
adopting the position of the ostrich. Of course, there might be
other, better reasons why, in particular, dependently typed
programming might turn out to be unrealistic: if anybody finds
them, I'll give up.

But, Oleg,...

> This message shows a non-trivial example 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.

...here you go too far for two reasons

(1) What's a static guarantee?

> The safety is based on:
> Haskell type system, quantified type variables, and a compact
> general-purpose trusted kernel.

What if I don't trust your kernel? The guarantees you require of
your kernel are not statically checked. What guarantee do I have
that the propositions which you identify are even the ones which
are really needed to eliminate bounds checking? How does the
machine replace ! by unsafeAt reliably, all by itself?

Yes, you can convince _me_ that something of the sort will do, because
I can follow the math. But what is the mechanism? What is the evidence?
What's the downloadable object that can be machine-checked to satisfy
my paranoid insurance company?

> Our example is `bsearch', taken from the famous paper "Eliminating
> Array Bound Checking Through Dependent Types" by Hongwei Xi and Frank
> Pfenning (PLDI'98).  Hongwei Xi's code was written in SML extended
> with a restricted form of dependent types. Here is the original code
> of the example (taken from Figure 3 of that paper, see also
> http://www-2.cs.cmu.edu/~hwxi/DML/examples/)

Hongwei Xi's code contains the evidence I'm asking for.
The verification conditions are added by hand in the program as
annotations, just as yours are annotations outside the program.
His are checked by Presburger arithmetic, just as yours could
be.

[..]

(2) And I hate to be a smartass, but...

>>bbounds:: (Ix i) => BArray s i a -> (BIndex s i, BIndex s i)
>>bbounds (BArray a) = let (l,h) = bounds a in (BIndex l, BIndex h)
> 
> Proposition: the two indices returned by bbounds are within the range
> of the array 'a'. Proof: from the semantics of the function `bounds',
> taken here as an axiom.

...this proposition is false. The bounds function returns bounds which
are outside the range of the array when the array is empty.
You'll notice that Hongwei Xi's program correctly handles this case.

Don't get me wrong: I think your branded arrays and indices are a very
good idea. You could clearly fix this problem by Maybe-ing up bbounds
or (better?) by refusing to brand empty arrays in the first place.

My point is merely this: if your guarantees really were static, you'd
have fixed this bug already.

Cheers

Conor