[Haskell-cafe] Haskell and the Software design process

[Kyle Murphy]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100504/23c66773/attachment.html