tag:blogger.com,1999:blog-6839602.post8391585046753089908..comments2008-01-10T04:38:05.761-08:00Jim Applehttp://www.blogger.com/profile/11080395413026172939noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-6839602.post-44093325150550198022008-01-10T04:38:00.000-08:002008-01-10T04:38:00.000-08:00The reasons for the implementations being different is that ESC did not support if or where at the time the paper was written. In addition, the ESC paper does not use a type class, but is restricted to Int in the type of risers. Catch does use a very identical to the one you present.<BR/><BR/>You also miss one way to remove the error. If you have a highly-optimising compiler, such as Supero http://www-users.cs.york.ac.uk/~ndm/supero/ it can actually optimise away the error case. If that happens, you can guarantee the original code is safe.<BR/><BR/>I also don't necessarily disagree that functions are hard to transform, in the most part. Occasionally you get a tricky one, but the majority are probably trivial. The problem is that as soon as you introduce a few hoops in front of someone, they tend to stop, and don't check their code is correct. Catch is partly about proving difficult functions, and partly about automating ones you could have done manually.<BR/><BR/>It's nice that you can use these techniques to enforce the invariant, but you would still need to add some kind of "did the user use these techniques everywhere" check afterwards. Just because you supply a safe list, the user is free to use the original list data type in other places, and it won't be immediately obvious.Neil Mitchellhttp://www.blogger.com/profile/13084722756124486154noreply@blogger.com