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

[Conor T McBride]

Hello again

Me:

>>What if I don't trust your kernel?

[..]

>>What's the downloadable object that can be machine-checked to satisfy
>>my paranoid insurance company?

Oleg:
> I hope that you can forgive me if I reply by
> quoting the above two paragraphs back to you, with the substitution 
> s/kernel/compiler/.
> 
> 	What if I don't trust your compiler?
> 
> I have heard a similar question asked of J. Strother Moore and
> J. Harrison. J. Strother Moore said that most of ACL2 is built by
> bootstrapping, from lemmas and strategies that ACL2 itself has
> proven. However, the core of ACL2 just has to be trusted.

It's not an issue of forgiveness. I actively encourage such questions,
of myself and other people. I'd also recommend this paper by Randy
Pollack:

   `How to believe a machine-checked proof'
   http://www.dcs.ed.ac.uk/home/rap/export/believing.ps.gz

But the one-line summary is `by rechecking it independently'.
Of course, we'll never achieve _certainty_ in any absolute
sense, but we can do a lot better than `I can't show you the
evidence for security reasons, but there's no doubt that...'.
In order to do that, you need more than a machine which
says `yes'. You need a language of evidence which is simple
enough that people can write their own checker in whatever way
they choose. Martin-Loef's type theory provides a source of
good candidates for such a language of evidence. Its core
proof-checking/type-checking algorithm is very small. This is
what comes out the other end of the Epigram elaborator.

[..]

>>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.
> 
> Actually, as far as the PLDI'98 paper is concerned, they specifically say
> they do not use the full Presburger arithmetics. Rather, they solve
> the constraints by Fourier variable elimination. Anyway, even if
> the various elaboration and decision rules are proven to be sound and
> complete, what is the evidence that their implementation in the
> extended SML compiler is also sound and complete?

Another very good question. Every time you appeal to a proof-search
oracle or to an axiomatization of a library, or anything which hides
the evidence, the amount of stuff you `just have to trust' gets
bigger, and the harder it is to perform independent rechecking.

But what if some bright spark (volunteers welcome) were to implement
Presburger Arithmetic in one of the following ways...?
   (1) External to the system, but outputting checkable proof terms,
         instead of just `yes' or `no'.
   (2) Within the system, with a checkable proof that its yea be
         yea and its nay be nay. [Traditional implementation and
         correctness proof.]
   (3) Within the system, with a type which actually guarantees
         what the algorithm proves in the first place. [The
         `two-level' approach.]

> The conclusion specifically states that the algorithm is currently
> incomplete.

Clearly, soundness is more important. But it is nice to have a good idea
which problems the machine will get and which it won't.

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

Oleg:
> I have noticed that the branding trick would work very well with
> number-parameterized types. The latter provide missing guarantees, for
> example, statically outlaw empty arrays. Hongwei Xi's code has another
> neat example: a dot product of two arrays where one array is
> statically known to be no longer that the other. Number-Parameterized
> types can statically express that inequality constraint too.

Yes, of course. And any dependently typed solution to these problems
would naturally parametrize the data-structures by their size,
represented as ordinary numbers. Statically expressing the constraints
is easy.

The abstract `brand' is just a type-level proxy for the bounding
interval, and the library of operations provides interval-respecting
operations on indices. This is a very neat solution in Haskell, but it
goes round an extra corner which isn't necessary with dependent types,
where you can just talk about the interval directly. The library-writer
would develop and verify the same convenient operations for working
with intervals and indices; the proofs would be independently
recheckable terms in type theory.

> The
> Number-Parameterized types paper considers a more difficult example --
> and indeed the typechecker forced me to give it a term that is
> verifiably a proof of the property (inequality on the sizes) stated in
> term's inferred type. The typecheker truly demanded a proof; shouting
> didn't help.

Rightly so. What tools would be useful in such a situation?

> Incidentally, the paper is being considered for JFP, I guess. I don't
> know if the text could be made available. I still can post the link to
> the code:
> 	http://pobox.com/~oleg/ftp/Haskell/number-param-vector-code.tar.gz
> 
> I should emphasize that all proper examples use genuine Haskell arrays
> rather than nested tuples.

[..]

There's no reason why a dependently typed language should not have
genuine arrays.

> Yet the type of the array includes its
> size, conveniently expressed in decimal notation. One can specify
> arithmetic equality and inequality constraints on the sizes of the
> array, in the type of the corresponding functions. The constraints can
> be inferred. One example specifically deals with the case when the
> sizes of those arrays are not known until the run-time -- moreover,
> change in the course of a computation that involves general
> recursion. It seems that branding trick nicely complements
> number-parameterized arrays and makes `dynamic' cases easier to
> handle.

Again, all of this sounds like a good thing to do, but less like hard
work if you have a language designed to support it.

I don't know why you emphasize general recursion. It's no big deal in
programs which we execute only at run-time. Sure, I prefer structural
recursion to general recursion, because I like to have termination for
free, and also to be able to use programs safely in types. But I am not 
a bottom-pincher: you can have general recursion at run-time and still
decide typechecking. Here's a cheap and nasty trick that does it (and
we're kicking around some less nasty tricks at the moment). Add a
hypothesis

   general :: forall p . (p -> p) -> p

This is all you need to write general recursive programs. In Epigram,
your program would invoke `general' once, and then make whatever
recursive calls you like. None of these programs can loop during
typechecking, because `general' has no computational behaviour. We
can tell which programs/proofs to trust by which use `general'. Only
when we output run-time code do we make

   general f = f (general f)

Of course, if you really want to run this program in types---at
your own risk---we plan to let you. There are three security levels:

   paradise:    a complete absence of generals
   purgatory:   there are generals, but their orders are not obeyed
   pandemonium: what happens when you listen to generals

A compiler-switch would do, but annotations on individual functions
would be better.

So please, everybody, no more `What about general recursion? What
about decidable typechecking?'. It's no big deal. Why do some people
presume that Cayenne's particular problems are intrinsic to any 
dependently typed language?

>>You'll notice that Hongwei Xi's program correctly handles this case.
> 
> But what if I specified the dependent type with a mistake that
> overlook the empty array case? Would the dependent ML compiler catch
> me red-handed? In all possible cases? Where is the formal proof of
> that?

I can't speak for dependent ML, but you wouldn't get away with it in
Epigram. Epigram rules out _provably_ impossible cases and provides
a language in which to provide this guarantee. In the mundane
majority of cases, this proof amounts to `constructors of datatype
indices are disjoint', which gets handled automatically.

> 	I have failed to emphasize the parallels between Hongwei Xi's
> annotations and the corresponding Haskell code.

It wasn't lost on me...

[..]

> Yes, there is a trusted kernel involved -- just
> as there is a Dependent SML system to be implicitly trusted.

I agree: the appeal to the constraint oracle is a weakness. As is
the appeal to informal proofs, or axiomatizations of the library.

> However,
> in the given example the trusted kernel is compact Haskell code plus
> the GHC system. The latter is complex -- but it is being used by
> thousands of people over extended period of time -- and so has higher
> confidence than experimental extensions (unless the latter have been
> formally proven -- I mean the code itself -- by a trusted system such as
> ACL2 or Coq).

Confidence of what? Remember that Haskell is logically unsound. I can
fake a branded index by taking the head of an empty list. Fortunately,
this fake will always be discovered at run-time before unsafeAt goes
haywire (that ain't true for the empty array bug). However, it somewhat
weakens the static guarantee!

> 	I do not wish to sound as being against Dependant Type
> systems and implementations. I merely wish to point out poor-man
> approaches.

Don't get me wrong either: I agree with you. I'm in favour of cranking
as much static confidence out of Haskell's type system as possible. And
some pretty good stuff is possible (modulo bottom). However, it's very
easy to pick up such programs, implemented by hook or by crook (I'm a
crook) in Haskell and say: `See? Who needs dependent types?'. The truth
of the matter is that these programs are rather like the dependently
typed programs you might write, except that you need to use type-level
proxies for values and type-level Prolog trickery, instead of ordinary
values and ordinary programs. The dependently typed versions of these
programs are simpler than the Haskell versions. In the short term,
Haskell is the here and now, so do what you can; in the longer term,
choosing type class unicycling over dependent types is a false economy.

[..]

> 	- Try to make `safety' checks algorithmical: use newtypes to
> `lift' the safety checks such as range checks and see if they can be
> merged with the tests the algorithm has to do anyway.

Yes, this is what often happens with dependently typed programs. The
key thing to ensure is that the tests have types which show their
meaning statically. A Bool is a bit uninformative.

> 	- Use explicitly-quantified type variables to associate
> `unforgeable' types with values, so that the following property holds:
> the equality of such types entails the equality of the corresponding
> values -- even if we don't know what they values are until the
> run-time.

Exactly: type-level proxies for values. It's the right thing to do
if you can't have values in types. I'm in favour of the `datakind'
idea: Haskell's type-level proxies for values should look as much
like values as possible!

> 	- Convenient (decimal) type arithmetics at compile time -- and
> even `semi-compile' time.

There's nothing which forces numbers in dependent type systems to be
unary. That's just the path of least resistance in prototypes. Also,
it reflects the importance of the inductive structure of numbers
when they are being used as indices. I wonder how much this really buys
you when you're developing indexed operations, as opposed to when you
want to type actual values. I guess I'll read the paper.

> I'm interested in just how far those principle may take me.

That's a good thing to do. I'm trying to deliver a language which makes
exactly that kind of program much easier to write. I hope that sounds
like a good thing too.

> 	Thank you very much for your message!

And thank you!

All the best

Conor