[Haskell-cafe] Monad-control rant
Edward Z. Yang
ezyang at MIT.EDU
Sun Jan 29 17:55:24 CET 2012
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.)
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
> RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ)
> If a zero is recoverable, we can always "finalize" it (by
> 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
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.
> > 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.
More information about the Haskell-Cafe