Eliminating Array Bound Checking through Non-dependent types
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. 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. 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. 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/) ] datatype 'a answer = NONE | SOME of int * 'a ] ] assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a ] assert length <| {n:nat} 'a array(n) -> int(n) ] ] fun('a){size:nat} ] bsearch cmp (key, arr) = ] let ] fun look(lo, hi) = ] if hi >= lo then ] let ] val m = (hi + lo) div 2 ] val x = sub(arr, m) ] in ] case cmp(key, x) of ] LESS => look(lo, m-1) ] | EQUAL => (SOME(m, x)) ] | GREATER => look(m+1, hi) ] end ] else NONE ] where look <| ] {l:nat, h:int | 0 <= l <= size /\ 0 <= h+1 <= size } int(l) * int(h) ] -> 'a answer ] in ] look (0, length arr - 1) ] end ] where bsearch <| ('a * 'a -> order) -> 'a * 'a array(size) -> 'a answer The text after `<|' are dependent type annotations. They _must_ be specified by the programmer -- even for internal functions such as `look'. Here's our code, deliberately written to be as close to Hongwei Xi's code as possible (This message is the complete code):
{-# OPTIONS -fglasgow-exts #-} module Dep where import Data.Array
bsearch cmp (key, arr) = brand arr (\arr' -> bsearch' cmp (key, arr'))
bsearch' cmp (key,arr) = look lo hi where (lo,hi) = bbounds arr look lo hi = let m = bmiddle lo hi x = arr !. m in case cmp (key,x) of LT -> bpred lo m (look lo) Nothing EQ -> Just (unbi m, x) GT -> bsucc hi m (\m' -> look m' hi) Nothing
This code is just as algorithmically efficient as the Dependent SML code: one middle index computation, one element comparison, one index comparison, one index increment or decrement per iteration. There are no type annotations as none are needed. Operator (!.) is a statically safe array indexing operator. The type system and the trust properties of the kernel below guarantee that in the expression "arr !. m" the index `m' is positively in range of the array `arr' bounds.
barr1 = listArray (5,5 + (length s)-1) s where s = "abcdefgh" btest1 = bsearch (uncurry compare) ('c',barr1) btest2 = bsearch (uncurry compare) ('x',barr1)
The code relies on a compact general-purpose trusted kernel explained below. That code should be preferably put into a separate module. First we introduce tags for Branded arrays and Branded indices:
-- those two must *not* be exported! newtype BArray s i a = BArray (Array i a) newtype BIndex s i = BIndex i
unbi (BIndex i) = i
These are `newtype's and so impose no run-time overhead. Of interest is a phantom type variable 's', which marks a _brand_ of an array and of an array index. An index is branded if it is certainly within the range of the array of its brand. The type variable 's' is similar to that in the ST monad. The latter relies on 's' to enforce serialization. We, OTH, do not impose any linearity constraints on 's' -- it may be freely duplicated (see bbounds below) and discarded (see `unbi'). It is created however under controlled conditions. The safety depends on the trusted way of creating branded types: the constructors BIndex and BArray should be used in the trusted kernel only, and should not be available anywhere else. The uniqueness of 's' afforded by the explicit universal quantification prevents mixing up of different brands. We must re-iterate that safety depends on assurances of the code that constructs BIndex values. Because of the high assurance, we must formulate the safety properties as propositions, and prove them. Fortunately, the code below is compact and straightforward, as well as general purpose.
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.
bmiddle:: (Integral i) => BIndex s i -> BIndex s i -> BIndex s i bmiddle (BIndex i1) (BIndex i2) = BIndex ((i1 + i2) `div` 2)
Proposition: l <= i1 <= h, l <= i2 <= h |- l <= (i1 + i2) `div` 2 <= h Proof: plain arithmetics. We should stress that the type of bmiddle assures that all indices involved have the same brand -- that is, the same lower and upper boundaries. A brand 's' is a (type-level) representation of index bounds. At compile time, we don't know what they are, but the unforgeability of 's' (see below) statically guarantees that the same 's' represents the same bounds.
bsucc:: (Ord i,Num i) => BIndex s i -> BIndex s i -> (BIndex s i -> r) -> r -> r bsucc (BIndex upb) (BIndex i) on_within on_out = let i' = i + 1 in if i' <= upb then (on_within (BIndex i')) else on_out
The function `bsucc' takes two branded indices that correspond to the same bounds (see the variable 's'). The function also takes two continuations, on_within and on_out. The first index is considered to be an upper limit. The function increments the second index. If the result does not exceed the upper limit, we invoke on_within and pass it the result. Otherwise, we invoke `on_out'. Safety Proposition: l <= upb <= h, l <= i <= h, (i+1) <= upb |- l <= (i+1) <= h Proof: from i < (i+1) and properties of inequalities. The safety proposition justifies our use of the data constructor BIndex.
bpred:: (Ord i,Num i) => BIndex s i -> BIndex s i -> (BIndex s i -> r) -> r -> r bpred (BIndex lwb) (BIndex i) on_within on_out = let i' = i - 1 in if i' >= lwb then (on_within (BIndex i')) else on_out
The dual of `bsucc'. Safety Proposition: l <= lwb <= h, l <= i <= h, (i-1) >= lwb |- l <= (i-1) <= h Because a branded index is assuredly within the bounds of the array of the same brand, we can write
infixl 5 !. (!.):: (Ix i) => BArray s i e -> (BIndex s i) -> e (BArray a) !. (BIndex i) = a ! i
actually, we may _safely_ replace a ! i with `unsafeAt a i' Finally, we need an introduction rule for BArray:
brand:: (Ix i) => Array i e -> (forall s. BArray s i e -> w) -> w brand (a::Array i e) k = k ((BArray a)::BArray () i e)
The function has a higher-rank type. It is the existential quantification of 's' as well as the absence of BArray constructor elsewhere guarantees that the same brand entails the same bounds.
( 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
In article <200408060820.KAA13716@ripper.it.kth.se>, Bjorn Lisper <lisper@it.kth.se> wrote:
( A really interesting post on static elimination of array bounds checking by Oleg...)
Some questions and suggestions:
Am I right suspecting, that this method also solves the problem of assuring the right p in p-modular arithmetic (as complained by Sergei Mechveliani in his Basic Algebra proposal)? -- Dipl.-Math. Wilhelm Bernhard Kloke Institut fuer Arbeitsphysiologie an der Universitaet Dortmund Ardeystrasse 67, D-44139 Dortmund, Tel. 0231-1084-257
Hello! Bjorn Lisper wrote:
What is the relation to the sized types by Lars Pareto and John Hughes?
It is orthogonal and complementary, as the message in response to Conor T. McBride indicated.
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?
It is just like the classical range analysis, but _reified_ in the programming language itself. Given a piece of code: finda x arr = loop lo where (lo,hi) = bounds arr loop i = if i <= hi then if x == arr ! i then Just i else loop (i + 1) else Nothing the analysis sees that 'i' starts at the lower bound of 'arr' and is incremented afterwards. When the analysis sees the test "i <= hi" it infers that in the `then' branch of that test `i' does not exceed the upper bound of the array. Therefore, the indexing operation `arr ! i' is safe and no range check is needed. In the `branding' framework, the programmer makes the result of the test "i <= hi" and the corresponding implication that `i' is in range known to the type system, by branding the index `i'. To be more precise, the programmer would replace the first `if' statement with if_in_range:: (Ix i) => i -> BArray s i e -> (BIndex s i->r) -> r ->r if_in_range i arr on_within_range on_outside_rage ... If `i' turns out to be in range, that fact would be recorded by passing to the continuation on_within_range a branded index. Thus the logical implication that was implicit in the range checker is made explicit to the typechecker here.
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.
True, just as the range analysis must verify the rules of the analysis. The difference is that the conventional range analyzer is a part of the _compiler_, typically hidden from view (of a regular programmer). Here, the analyzer is a part of a _library_. It is also true that our analysis can't be exact: if the code includes let i = very_complex_function j and we know that j is in range, it may be very difficult to ascertain that 'i' will always be in range. In that case, we do the following let j_unbranded = unbrand j i = very_complex_function j_unbranded in if_in_range i arr on_within_range on_outside_rage That is, we intentionally forget the branding information, do a complex index transformation, followed by a run-time witnessing to recover the branding. If we somehow know that very_complex_function keeps its result in range, we can replace `on_outside_rage' with the function that raises an exception, crashes the computer, etc. If we are not sure if `i' is in range, then our program must do the range check anyway; if `i' turns out of range, the program should do what the algorithm prescribes in that case. The upshot is that `if_in_range' makes the programmer explicitly consider the consequences of the range check. We turn the range check from a routine safety check into an algorithmically significant decision. Incidentally, if we can prove that `very_complex_function' leaves the index in range, then we can make the function return a branded index, and thus eliminate the if_in_range check above. Because the creation of a branded index can only be done in a trusted kernel, we must put such a function into the kernel, after the appropriate rigorous verification -- perhaps formal verification.
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
Hello!
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?
That is very well said! 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. ACL2 has been used for quite a while and so there is a confidence in its soundness. Incidentally, both NSA and NIST found this argument persuasive, when they accepted proofs by ACL2 as evidence of high assurance, in awarding Orange book A1 and IFIPS 140-1 ratings -- the highest security ratings -- to some products.
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? Speaking of completeness, the procedure in PLDI'98 paper notes, "Note that we have been able to eliminate all the existential variables in the above constraint. This is true in all our examples, but, unfortunately, we have not yet found a clear theoretical explanation why this is so." The conclusion specifically states that the algorithm is currently incomplete.
...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.
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. 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. 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. 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.
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 have failed to emphasize the parallels between Hongwei Xi's annotations and the corresponding Haskell code. What Hongwei Xi expressed in types, the previously posted code expressed in terms. The terms were specifically designed in such a way so that consequences of various tests were visible to the type systems, and so the corresponding conclusions could be propagated as a part of regular type inference. Number-parameterized types also rely on the type inference of Haskell. Yes, there is a trusted kernel involved -- just as there is a Dependent SML system to be implicitly trusted. 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). I do not wish to sound as being against Dependant Type systems and implementations. I merely wish to point out poor-man approaches. Here are the principles, which I'm sorry to have failed to eluicidate: - 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. - 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. - Convenient (decimal) type arithmetics at compile time -- and even `semi-compile' time. I'm interested in just how far those principle may take me. Thank you very much for your message!
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
Hi, Inspired by Conor's and Oleg's discussion let's see which dependent types properties can be expressed in Haskell (and extensions). I use a very simple running example. -- append.hs -- append in Haskell data List a = Nil | Cons a (List a) append :: List a -> List a -> List a append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil We'd like to statically guarantee that the sum of the output list is the sum of the two input lists. In Hongwei Xi's DML or index types a la Christoph Zenger, we can write the following. -- append in DML/index types -- I use a slightly different syntax compared to DML data List a n = Nil where n=0 | Cons a (List a m) where n=m+1 append :: List a l -> List a m -> List a (l+m) append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil Each list carries now some information about its length. The type annotation states that the sum of the output list is the sum of the two input lists. [Conor: I don't know whether in Epigram you can specify the above property?] I like DML/index types but both systems are rather special-purpose. There might be other program properties which cannot be captured by index types. In the latest Chameleon version, we can encode the above DML/index types program as follows. [Side note: I encode dependent types in terms of singleton types] -- append.ch -- Chameleon encoding of append in DML/index types -- encoding of arithmetic data Zero data Succ x -- we introduce a ternary predicate symbol Add l m n -- which models l+m=n -- in my encoding I assume that l and m are given hconstraint Add rule Add l m n, Add l m n' ==> n=n' rule Add Zero m n <==> m=n rule Add (Succ l) m n <==> Add l m n', n=Succ n' -- type indexed data type -- we keep track of the length of the list data List a n = (n= Zero) => Nil | forall m. Add (Succ Zero) m n => Cons a (List a m) append :: Add l m n => List a l -> List a m -> List a n append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil Tim Sheard argues that no predicates other than equality are necessary. Here's an adaptation of a Omega example I found in one of his recent papers. -- append2.ch -- we introduce terms to represent addition data Z data S n data Sum w x y = (w=Z, x=y) => Base | forall m n. (w=S m, y=S n) => Step (Sum m x n) data Seq a n = (n=Z) => Nil | forall m. (n=S m) => Cons a (Seq a m) app :: Sum n m p -> Seq a n -> Seq a m -> Seq a p app Base Nil ys = ys app (Step p) (Cons x xs) ys = Cons x (app p xs ys) Well, now that we have "compiled" away arithmetic, why not get rid of equality? I rely on encoding trick used by Cheney, Hinze, Weirich, Xi and most likely many others. -- append3.hs -- we introduce terms to represent equality data E a b = E (a->b,b->a) -- a silent assumption is that for each monomorphic value E (g,h) -- functions g and h represent the identity -- can't be enforced by Haskell, must be guaranteed by the programmer data Z = Z data S n = S n data Sum w x y = Base (E w Z) (E x y) | forall m n. Step (Sum m x n) (E w (S m)) (E y (S n)) data Seq a n = Nil (E n Z) | forall m. Cons a (Seq a m) (E n (S m)) app :: Sum n m p -> Seq a n -> Seq a m -> Seq a p app (Base (E (g1,h1)) (E (g2,h2))) (Nil (E (g3,h3))) ys = cast2 (E (g2,h2)) ys app (Step p' (E (g1,h1)) (E (g2,h2))) (Cons x xs (E (g3,h3))) ys = Cons x (app p' (cast2 (E (cast1 (g1.h3),cast1 (g3.h1))) xs) ys) (E (g2,h2)) -- some magic, gs, hs and casts refer to term operations to mimic -- type-level equality operations. Note that if we erase all Es, gs, -- hs and casts we obtain append2.ch cast1 :: (S a->S b)->a->b cast1 f a = let S b = f (S a) in b cast2 :: E m p -> Seq a m -> Seq a p cast2 (E (g1,h1)) (Nil (E (g2,h2))) = (Nil (E (g2.h1, g1.h2))) cast2 (E (g1,h1)) (Cons x xs (E (g2,h2))) = (Cons x xs (E (g2.h1,g1.h2))) Conclusion: Note that append3.hs runs under Haskell. append2.ch runs under Omega, Haskell extension with generalized data types and Chameleon (note that append2.ch uses Chameleon syntax for data type definitions!). append.ch runs under Chameleon. To me it seems rather tedious to use (plain) Haskell for dependent types programming. Martin
Hi Martin Martin Sulzmann wrote:
Hi,
Inspired by Conor's and Oleg's discussion let's see which dependent types properties can be expressed in Haskell (and extensions). I use a very simple running example.
[..]
We'd like to statically guarantee that the sum of the output list is the sum of the two input lists.
A lovely old chestnut. I think I wrote that program (in Lego plus programming gadgets) back in 1998. [..]
Each list carries now some information about its length. The type annotation states that the sum of the output list is the sum of the two input lists.
[Conor: I don't know whether in Epigram you can specify the above property?]
It's basic stuff. Here's the Epigram source, ab initio, which I knocked up in about 30 seconds (the precise layout is the responsibility of my suboptimal prettyprinter): ---------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ---------------------------------------------------------------------- ( n, m : Nat ! let !----------------! ! plus n m : Nat ) plus n m <= rec n { plus x m <= case x { plus zero m => m plus (suc n) m => suc (plus n m) } } ---------------------------------------------------------------------- ( X : * ! ! ! ! n : Nat ! ( x : X ; xs : Vec X n ! data !---------! where (--------------! ; !-----------------------! ! Vec X n ! ! vnil : ! ! vcons x xs : ! ! : * ) ! Vec X zero ) ! Vec X (suc n) ) ---------------------------------------------------------------------- ( xs : Vec X n ; ys : Vec X m ! let !----------------------------------! ! vappend xs ys : Vec X (plus n m) ) vappend xs ys <= rec xs { vappend x ys <= case x { vappend vnil ys => ys vappend (vcons x xs) ys => vcons x (vappend xs ys) } } ---------------------------------------------------------------------- These programs were developed interactively: I only had to write the type signatures and the right-hand sides. Under those circumstances, <= rec xs and <= case x are rather less effort than typing the left-hand sides by hand. Moreover they provide guarantees of totality (structural recursion & exhaustiveness of patterns). I'm sorry I can only send this program in black-and-white. The editor uses foreground colour to indicate the status of each identifier and background colour to indicate the typechecker's opinion of each subexpression. You'll notice (or perhaps you won't) that there's rather a lot of type inference going on, both in figuring out indices, and in figuring out which variables should be implicitly quantified. You may also notice the number of fingers I need to lift to convince the machine that the arithmetic condition is satisfied. The definition of plus is sufficient: the marvellous thing about computation is that computers do it. You get partial evaluation for free, but if the constraints require more complex algebra, you have to do the work. Or teach a computer to do the work, hence the project to implement a certified Presburger Arithmetic solver in Epigram: that seems a worthy occupation for the other ten fingers. Or a PhD student.
I like DML/index types but both systems are rather special-purpose. There might be other program properties which cannot be captured by index types.
Not half. See `The view from the left' by myself and James McKinna for a typechecker (for simply-typed lambda-calculus) whose output is the result of checking _its input_. [..]
Tim Sheard argues that no predicates other than equality are necessary. Here's an adaptation of a Omega example I found in one of his recent papers.
This observation dates back to Henry Ford: `you can have any colour you like as long as it's black'. In a more technical context, it's certainly a lot older than me. Of course, it's a no-brainer to turn constraint-by-instantiation into constraint-by-equation if you have the right notion of equality. You have to deal somehow with the situation where things of apparently different types must be equal, but where the types will be identified if prior constraints are solved. One approach can be found in my thesis.
To me it seems rather tedious to use (plain) Haskell for dependent types programming.
Absolutely. But the fact that it's to some extent possible suggests that we could, if we put our minds to it, make it less tedious without fundamentally messing up anything under the bonnet. Cheers Conor
Martin Sulzmann stated the goal of the append exercise as follows: ] Each list carries now some information about its length. ] The type annotation states that the sum of the output list ] is the sum of the two input lists. I'd like to give a Haskell implementation of such an append function, which makes an extensive use of partial signatures and, in generally, relies on the compiler to figure out the rest of the constraints. We also separate the skeleton of the list from the type of the list elements. This solution differs from the Haskell solution append3.hs given in Martin Sulzmann's message. The latter solution relies on the trusted kernel: the equality datatype E. It is quite easy to subvert append3.hs if we set up E with particular run-time values. The error will not be discovered statically -- nor dynamically for that matter, in the given code. We can get the function app to produce a non-bottom list value whose dynamic size differs from its size type (and whose static size is patently not the arithmetic sum of the static sizes of the arguments). The solution in this message relies entirely on Haskell type system; there are no trusted terms. An attempt to write a terminating term that is to produce a list whose length differs from that stated in the term's type will be caught by the type checker at compile time.
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module LL where
data Z; data S a
First we state the Sum constraint:
class Add n m p | n m -> p instance Add Z a a instance Add n (S m) p => Add (S n) m p
Now we derive a number-parameterized list. We separate the shape type of the list from the type of the list elements:
data Nil len a = Nil deriving Show data Cons b len a = Cons a (b a) deriving Show
The constraint `List f' holds iff f is the shape type of a valid list:
class List ( lst :: * -> * ) instance List (Nil Z) instance (Add (S Z) n m, List (tail n)) => List (Cons (tail n) m)
The following `type function' makes sure that its argument is a valid list. That guarantee is established statically. We should note that the class List has no members. Therefore, the only terminating term with the signature `(List f) => f a -> f a' is the identity.
make_sure_it_is_a_list:: (List f) => f a -> f a make_sure_it_is_a_list = id
nil:: Nil Z a nil = Nil
We let the compiler write out the constraints for us:
consSig :: a -> f l a -> Cons (f l) (S l) a consSig = undefined cons h t | False = consSig h t cons h t = make_sure_it_is_a_list$ Cons h t
We can create a few lists:
testl1 = cons (3::Int) ( cons (2::Int) ( cons (1::Int) nil ) ) testl2 = ( cons (2::Int) ( cons (1::Int) nil ) )
The type of testl2 is reasonable: testl2 :: Cons (Cons (Nil Z) (S Z)) (S (S Z)) Int If we try to cheat and write consSig :: a -> f l a -> Cons (f l) (S (S l)) a the typechecker will point out that 'Z' is not equal to 'S Z' when typechecking testl1 and testl2. We can now handle Append:
class Append l1 l2 l3 | l1 l2 -> l3 where appnd :: l1 a -> l2 a -> l3 a
instance Append (Nil Z) l l where appnd _ l = l
instance (Append (t n) l (t' n'), List (t' n')) => Append (Cons (t n) (S n)) l (Cons (t' n') (S n')) where appnd (Cons h t) l = cons h (appnd t l)
We had to be explicit with types in the latter instance. The types must correspond to the term; the typechecker will tell us if they do not. We now attempt to verify the sum of lengths property. We attach the desired constraints using the partial signature trick. This saves us trouble enumerating all other constraints.
constraintAdd:: Add l1 l2 l3 => (f1 l1 a) -> (f2 l2 a) -> (f3 l3 a) constraintAdd = undefined
vapp l1 l2 | False = constraintAdd l1 l2 vapp l1 l2 = appnd l1 l2
Perhaps we should move to Cafe?
participants (5)
-
Bjorn Lisper -
Conor T McBride -
Martin Sulzmann -
oleg＠pobox.com -
wb＠arb-phys.uni-dortmund.de