What I think to be the hard part to do is to put this on the type system, e.g.:
intDiv x y = if y > x then 0 else 1 + (intDiv (x - y) y) Should not compile. Otherwise you will need the bottom value. Am I missing something? Thiago. 2011/12/20 Jesse Schalken <jesseschal...@gmail.com>: > On Tue, Dec 20, 2011 at 10:43 PM, Gregory Crosswhite <gcrosswh...@gmail.com> > wrote: >> >> >> On Dec 20, 2011, at 9:18 PM, Jesse Schalken wrote: >> >> Why do you have to solve the halting problem? >> >> >> You have to solve the halting problem if you want to replace every place >> where _|_ could occur with an Error monad (or something similar), because >> _|_ includes occasions when functions will never terminate. > > > I think we're talking about different things. By "bottom" I mean the > function explicitly returns "error ..." or "undefined". In those cases, it > should go in an error monad instead. In cases where there is an infinite > loop, the function doesn't return anything because it never finishes, and > indeed this separate problem will never be solved while remaining Turing > complete because it is the halting problem. > >> >> >> Consider integer division by 0. [...] >> This is all I was talking about. >> >> >> But imagine there was an occasion where you *knew* that the divisor was >> never zero --- say, because the divisor was constructed to be a natural >> number. > > > Then use a separate type for natural numbers excluding 0. Then you can > define a total integer division function on it (although the return value > may be zero and so needs a different type). > >> >> Now there is no point in running in the Error monad because there will >> never such a runtime error; in fact, it is not clear what you would even >> *do* with a Left value anyway, short of terminating the program and printing >> and error, which is what would have happened anyway. > > > What you do with a Left value is up to you - that's the point, you now have > a choice. In fact, the value might not even be being handled by you, in > which case someone else now has a choice. Handling of the error is done in > the same place as handling of the result, no IO needed. > >> >> Furthermore, it is easy to imagine circumstances where you have now forced >> your entire program to run in the Error monad, which makes everything >> incredibly inconvenient with no benefit at all. > > > This "inconvenience" I imagine is the extra code required to compose > functions which return values in a monad as opposed to straight values. To > me this is a small price to pay for knowing my code won't randomly crash, > and I would rather this be handled syntactically to make composing monadic > values more concise. > > The point is your program shouldn't be able to make assumptions about values > without proving them with types. It's often easier not to make the > assumption and propagate some error in an error monad instead, but that's > better than getting away with the assumption and having the program crash or > behave erratically because the assumption turned out false. > >> This is the problem with arguments against partial functions; they don't >> solve any problems at all except in the case where you have untrusted data >> in which case you should be using a different function or manually checking >> it anyway, and they add a lot of wasted overhead. > > > The whole term "untrusted data" baffles me. How often can you actually > "trust" your data? When you send your software out into the wild, what > assumptions can you make about its input? What assumptions can you make > about the input to a small part of a larger program which is millions of > lines? You can often deduce that certain values do/do not occur in small > parts of code, but the difficulty of such deductions increases exponentially > with the size of the codebase, and is a job done much better by a type > system. > > Also I would like to think this "wasted overhead" can be optimised away at > some stage of compilation, or somehow removed without the programmer needing > to think about it. Maybe I'm just dreaming on those fronts, however. > >> Cheers, >> Greg > > > > _______________________________________________ > 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