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
