Daniel Fischer wrote:
Distinguish between findable and unfindable bottoms? The difference in practice is clear, but is there also a theoretical difference?
That depends on the theory you choose. If you're only interested in non-bottom results anyway, you can choose to use a simple theory (that is: a simple formal semantic) which doesn't distinguish between non-termination and other errors. If you're interested in modeling error-handling, you should probably use a semantic which does distinguish different kinds of errors. A denotational semantics which takes errors into account could use the error monad similar to how you use it in Haskell for explicit error handling. In fact, monads in CS where first introduced for denotational semantics, before they where applied to functional programming. That means that you have a choice: Avoid findable bottoms by using explicit error handling with error monads in your program, so that you can use a simpler semantics to understand your code. Or use findable bottoms to encode errors, and use an error monad to upgrade your semantics to cope with them. I prefer to use the monads in my Haskell code, and not in my head (where the semantics is processed in the code understanding cycles of my programming process). Tillmann