User Error
Gah. I’m trying to write some straightforward combinatorial code in Haskell, and I finally got to the point where I had to start using nontrivial algorithms to make it acceptably fast. When I run those algorithms the first time, I get the following gem:
*Main> drops 100 2
*** Exception: divide by zero
The “drops” function is now 15 lines of mutually recursive Haskell, and the interactive interpreter conveniently informs me that there was a division by zero. No hint as to where it might be, of course. Come to think of it, this was probably the reason I dropped back to Python after my last Haskell stint.
This came up all the time in OCaml compiler work too. Deep in the middle of an optimization pass, I’d mess up a symbol context. The compiler would conveniently inform me that
NotFound
OCaml exceptions are monomorphic, so the default exception thrown by map classes couldn’t even include the key, much less something like a stack trace.
The conclusion: any language that claims to be high level should be able to give the exact context in which errors occurred. This means either some form of trace reporting and/or the ability to rule out the possibility of certain errors (dependent types). Yes, both Haskell and OCaml have debuggers for this purpose, but that isn’t good enough; in my case the history function in the Haskell prints out gobs and gobs of tail recursion frames before it ever gets to the real source of the problem. Debugging in high level languages should be easy, not just possible.
Update: the problem turns out to be integer overflow, which means I’m hitting the same language flaw Guido van Rossum described here. Converting my code from Int to Integer requires adding a slew of conversion calls and type annotations because I’m using integers as both container indices and as the results of large combinatorial values. Hopefully Tim Sweeney’s idea will work out and this dichotomy can go away.
Update (16mar2009): Possible hope for the future:
http://ghcmutterings.wordpress.com/2008/12/04/explicit-stack-traces.
March 14th, 2009 at 11:07 pm
Sweeny’s presentation was very rewarding to flip through! I only don’t understand what “partiality” is. When talking about “Effects Model,” Sweeny says “purely functional is the right default,” but, “imperative constructs are vital.” He then says, “Why not go one step further and define partiality as an effect, thus creating a foundational language subset suitable for proofs?”
March 15th, 2009 at 7:09 am
A function is partial if it fails to return on some inputs, either because it loops forever or hits an exceptional case (and presumably throws an exception). It’s easy to infer “throws an exception” as part of the type system. Checking for nontermination is more difficult: for Turing complete languages it is impossible without full dependent typing, where programs are required to include a proof that all computations are total.
Agda and Epigram are examples of total dependent typed languages, and Disciple is an example of an effect typed language.