[Haskell-cafe] Haskell and the Software design process

[aditya siram]

This is awesome! GHC-devs , please mainline the CONTRACT pragma.
-deech

On 5/4/10, Edward Kmett <ekmett at 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 <
> gcross at 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 <jwlato at gmail.com> wrote:
>>
>>> On Tue, May 4, 2010 at 5:31 PM, Gregory Crosswhite
>>> <gcross at 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>