[Haskell-cafe] Monad-control rant

[Edward Z. Yang]

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