Hello Oleg, hello all I agree with you on this: oleg@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