On Tue, May 4, 2010 at 2:09 PM, Limestraël wrote:

2010/5/4 John Lato

...

"Crashing at the point of the error" isn't necessarily useful in Haskell due to lazy evaluation.  The code will crash when the result of the partial function is evaluated, which may be quite far away (in terms of function calls) from where the programmer would expect.

Is that why Haskell can't provide a traceback when exceptions are raised?

I'm not really the right person to answer this, but I believe this is roughly true.

Are there other methods than Maybe or exceptions to handle the errors in Haskell? Is the monad Error(T) useful?

There are many other ways of handling errors/exceptional conditions. Maybe, Either, ErrorT, abuse of monad fail, explicit-exception [1] and attempt [2] are some of them; there are others. Which is appropriate depends upon the use case. The difficulty is gluing together libraries that use different mechanisms (attempt addresses this to some extent). And of course exceptions, which are unavoidable but often neglected because they're invisible at the type level. [1] http://hackage.haskell.org/package/explicit-exception [2] http://hackage.haskell.org/package/attempt John

On Tue, May 4, 2010 at 5:31 PM, Gregory Crosswhite 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

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/haskellc... ) 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 wrote: On Tue, May 4, 2010 at 5:31 PM, Gregory Crosswhite 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

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@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/haskellc...) 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 wrote:

...

On Tue, May 4, 2010 at 5:31 PM, Gregory Crosswhite 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

...

...

...

...

"aditya" == aditya siram writes:

aditya> This is awesome! GHC-devs , please mainline the CONTRACT aditya> pragma. I think it needs a LOT more work before it is usable. (I hope I'm wrong, but Dana reckoned it needed about 7 more man-years of work.) Dana sent me a copy of her ghc 6.8 repository (which didn't compile), and I updated (by hand) a 6.11 repository. I was able to get a few test programs to be rejected as not fulfilling their contracts (due to type classes), and a few others to loop at compile time, but I couldn't find any that passed. I was supposed to have a go at debugging the loops, but never got round to it. -- Colin Adams Preston Lancashire () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments

Gregory Crosswhite 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*.

Well sure, but how can you demonstrate that you (the programmer) haven't screwed up? That's the point that I'm most interested in. Certainly there is a difference between exceptional behavior at runtime (e.g., due to malformed inputs) vs programming errors. We can't stop the former without broadening the scope of the typesystem to include runtime inputs; but we can, at least idealistically, stop the latter. While complex invariants require full dependent types to capture, there are a surprising number of invariants that Haskell's type system can already capture (even without GADTs!).

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.

If you're structuring your code with that invariant, then why aren't you using the correct type? data AtLeastTwo a = ALT a a [a] If your response is that you use too many of the standard list functions, then write a module with ALT versions (because evidently you need one). If your response is that you convert between lists and ALT too often, then you probably need to restructure the code. At the very least you should be using a newtype and smart constructors, so that you can actually prove your invariant whenever necessary: newtype AtLeastTwo a = Hidden_ALT [a] altEnd :: a -> a -> AtLeastTwo a altCons :: a -> AtLeastTwo a -> AtLeastTwo a altList :: a -> a -> [a] -> AtLeastTwo a fromList :: [a] -> Maybe (AtLeastTwo a) toList :: AtLeastTwo a -> [a] Without smart constructors or an ADT to enforce your invariants, why should you be convinced that you (the programmer) haven't messed up? The cheap and easy access to ADTs is one of the greatest benefits of Haskell over mainstream languages, don't fear them. -- Live well, ~wren