Excerpts from Mikhail Vorozhtsov's message of Sun Jan 29 05:34:17 -0500 2012:
You are trying to make bottoms a new null pointers. Sometimes it just doesn't worth the effort (or depends on the interpreter you use). I want to have the option to say: sorry, in this particular case (monad) I don't distinguish `error` from non-termination, so `catch ⊥ h = ⊥`.
This is a longstanding complaint that Robert Harper has with lazy languages (the "paucity of types" complaint.) http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/ There's not much I can say here, except that: - There really is no difference: GHC can sometimes detect nontermination and will throw an exception (for example, the deadlocked exception), and - The user will sometimes act as a termination checker, and ^C a program that is taking too long.
I think it is one of the simplest layouts one can some up with. I'll try to explain the motivation behind each inclusion.
ABORTS(μ) ⊆ RECOVERABLE_ZEROS(μ)
I'm sorry, I cannot understand the discussion below because you haven't defined precisely what ABORTS means. (See also below; I think it's time to write something up.)
Why are they not equal? After all we can always write `recover weird $ \e → abort e`, right? But zeros from `RECOVERABLE_ZEROES \ ABORTS` may have additional effects. For example, recoverable interruptions could permanently disable blocking operations (you can close a socket but you can't read/write from it). Why the inclusion is not the other way around? Well, I find the possibility of `abort e1` and `abort e2` having different semantics (vs `recover` or `finally`) terrifying. If you can throw unrecoverable exceptions, you should have a different function for that.
RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ)
If a zero is recoverable, we can always "finalize" it (by catch-and-rethrow).
FINALIZABLE_ZEROS(μ) ⊆ ZEROS(μ)
This one is pretty obvious. One example of non-finalizable zeros is bottoms in a non-MonadUnbottom monad (e.g. my X monad). Another would be `System.Posix.Process.exitImmediately`.
Ugh, don't talk to me about the exit() syscall ;-)
If we can unify the semantics in a sensible way, I have no objection (the choice of exceptions or pure values is merely an implementation detail.) But it's not obvious that this is the case, especially when you want to vary the semantics in interesting ways. That's why I'm trying to make things like MonadUnbottom optional.
Well, I haven't actually checked if this works or not!
- If the semantics are different, OK, now you need to write two catch functions, but you are handling each type of exception separately already, right?
You have to handle IO exceptions only if you "leak" them from your implementation. For transformer stacks it is always so, for some interpreters it is not. The `ErrorT e IO` problem is related to another can of worms: operation lifting through transformers.
OK.
IO has effects, so if I have mplus (effect>> mzero) a, this equals effect>> a, not a. Same applies for MaybeT IO. I have to be very careful to preserve the monoid property. STM, on the other hand, by definition has the ability to rollback. This is what makes it so nice! Should STM/`MaybeT IO` have MonadException instances? How `catch` and `finally` will interact with `retry`/`MaybeT (return Nothing)`?
I don't see why not, as long as they obey the semantics. But someone should do the legwork here.
I also think that unrecoverable/recoverable exceptions is a legitimate idea. I think it could get its own typeclass, let's call it MonadUnrecoverableException. I don't think any MonadException is automatically a MonadUnrecoverableException, by appealing to the laws of MonadException. I'm confused. What methods/laws would MonadUnrecoverableException contain?
They'd be very simple! Unrecoverable exceptions always cause program execution to "get stuck." There are no contexts (like catch) which affect them. So you are suggesting something like
class MonadUnrecoverableException μ where throwUnrecoverable ∷ Exception e ⇒ e → μ α
But I'm not interested in throwing such exceptions! It may not even be possible (allowed) to do that from within the monad itself (e.g. external interruptions in my X monad). All I care about is that unrecoverable zeros (not necessarily tied with Exception) exist, which means that I cannot implement `finally` on top of `catch`.
Yes, but in that case, your semantics would have to change to add a case for finally; you'd need to unwind the stack, etc etc. You're talking about finalizable, but unrecoverable exceptions.
Yes, I think for some this is the crux of the issue. Indeed, it is why monad-control is so appealing, it dangles in front of us the hope that we do, in fact, only need one API.
But, if some functions in fact do need to be different between the two cases, there's not much we can do, is there? Yes, but on the other hand I don't want to reimplement ones that are the same. I want to have a modular solution precisely because it allows both sharing and extensibility.
The cardinal sin of object oriented programming is building abstractions in deference of code reuse, not the other way around. Stepping back a moment, I think the most useful step for you is to write up a description of your system, incorporating the information from this discussion, and once we have the actual article in hand we can iterate from there. Edward