This is awesome! GHC-devs , please mainline the CONTRACT pragma. -deech
On 5/4/10, Edward Kmett <ekm...@gmail.com> wrote: > The papers are available here: http://gallium.inria.fr/~naxu/pub.html > > But in general you can say things like the following: > > (Dana Xu uses a slightly different notation that I can never remember). > > sorted :: Ord a => [a] -> Bool >> sorted [] = True >> sorted [x] = True >> sorted (x:xs) = x < head xs && sorted xs >> >> sort :: Ord a => [a] -> { xs : [a] | sorted xs } >> sort [] = [] >> sort (x:xs) = insert x (sort xs) >> >> insert :: Ord a => a -> { xs : [a] | sorted xs } -> { ys : [a] | sorted xs >> } >> -- insert :: Ord a => a -> { xs : [a] } -> { ys : [a] | sorted xs ==> >> sorted ys } >> insert x [] = [x] >> insert x yys@(y:ys) >> | x < y = x:yys >> | otherwise = y:insert x ys >> > > > > And with that an abstract interpreter runs checking the partial correctness > of the code. The predicates can be specified in Haskell itself, > non-termination (even in the predicate) is covered by the fact that you only > check partial correctness. > > In the above, the abstract interpretation for sort can use the fact that > insert returns a sorted list. In fact the only non-trivial clause to prove > in the whole thing is the second branch of insert, which may rely on the > transitivity of (<=), and so may have to be handed off to an external > theorem prover. > > Static contract checking/ESC yields either success, a warning that it can't > prove something, with a stack trace to the condition it can't prove, or an > error with a counter example and a stack trace of what goes wrong. > Unannotated code is effectively inlined rather than assumed to be total, so > you can mix and match this style with traditional code. > > The fact that you get compile time stack traces is what made me fall in love > with the approach. Dana used to have (most of) a port of ghc to support SCC > on darcs.haskell.org, but I don't know what happened to it. > > -Edward Kmett > > > > On Tue, May 4, 2010 at 2:43 PM, Gregory Crosswhite < > gcr...@phys.washington.edu> wrote: > >> I definitely like that idea. :-) Is this similar to the notion of >> dependent types? >> >> Cheers, >> Greg >> >> >> >> On May 4, 2010, at 11:21 AM, Kyle Murphy wrote: >> >> This whole thing seems to be touching on something I saw recently and was >> quite interested in. I found a site talking about static contract checking >> in Haskell, unfortunately I can't seem to find it now, but this paper ( >> http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/haskellcontract.ps) >> by Simon Peyton Jones among others seems to be about the same thing the >> site I found was talking about. The idea is to provide enough extra >> information to the type system to actually be able to verify that for >> instance, secondElement is always called with at least two items. If there >> exists in your code any situation in which the contract of a function >> could >> be violated (and therefore the possibility of blowing up at runtime), it >> no >> longer passes static type checking. The paper doesn't go much into the >> impact something like that would have on for instance GHCi, but if it was >> smart enough to inherit contracts from functions used and display these >> derived contracts this would be a very simple way to find all the edge >> cases >> of your code. >> >> -R. Kyle Murphy >> -- >> Curiosity was framed, Ignorance killed the cat. >> >> >> On Tue, May 4, 2010 at 12:56, John Lato <jwl...@gmail.com> wrote: >> >>> On Tue, May 4, 2010 at 5:31 PM, Gregory Crosswhite >>> <gcr...@phys.washington.edu> wrote: >>> > >>> > Yes, but I think that it is also important to distinguish between cases >>> where an error is expected to be able to occur at runtime, and cases >>> where >>> an error could only occur at runtime *if the programmer screwed up*. If >>> you >>> structure your code to preserve and rely on the invariant that a given >>> list >>> has at least two elements, then it makes sense to call secondElement >>> because >>> if the list doesn't have two elements then you screwed up. Furthermore, >>> there is no way to recover from such an error because you don't >>> necessarily >>> know where the invariant was broken because if you did you would have >>> expected the possibility and already fixed it. >>> > >>> > But hypothetically, suppose that you decided to use safeSecondElement >>> anyway; now you have to deal with a Nothing in your code. Since, again, >>> you don't know how to recover from this (as if you did, you wouldn't have >>> gotten a Nothing in the first place), the only thing you can do is >>> propagate >>> it through the calculation, until it reaches someone who can recover from >>> it, which means that now your whole calculation has to be muddled up with >>> Maybe types wrapping every result purely to capture the possibility of a >>> bug >>> (or hardware fault, I suppose). If your program relied on this >>> calculation, >>> then it *still* has no choice but to terminate, and it *still* doesn't >>> know >>> where the error occurred --- although if you use something like ErrorT, >>> you >>> might at least know what the nature of the error was. So basically, you >>> still end up with having to terminate your program and printing out an >>> error >>> message reporting the existence of a bug, but now you had to add >>> error-propagating infrastructure to your entire program to do this that >>> makes every function more complicated, rather than relying on the >>> built-in >>> infrastructure supplied by Haskell in the form of undefined, error, and >>> throwing exceptions from pure code. >>> > >>> > If you want to make your program fault tolerant against bugs --- which >>> is reasonable in programs such as, say, a text editor, where inability to >>> complete one task doesn't necessarily mean that the whole program has to >>> stop --- then you are probably working in the IO monad and so have access >>> to >>> means of catching exceptions, which means that you might as well use >>> them. >>> > >>> > Thus, if you are dealing with invariants which only fail if you, the >>> programmer, screwed something up, I don't really see the benefit of using >>> functions like safeSecondElement over secondElement. Of course, >>> situations >>> in which you are *expecting* subcomputations to be able to fail at >>> runtime >>> if, say, the input is ill-formed, are a different matter. >>> >>> I agree completely, although I'm not the first to point out that >>> catching exceptions thrown from pure code can be tricky because they >>> might not appear where you expect them to. Of course this can also >>> indicate your architecture needs help. >>> >>> John >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> Haskell-Cafe@haskell.org >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >> >> >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
