[Haskell-cafe] Monad-control rant

[Mikhail Vorozhtsov]

On 01/24/2012 10:56 PM, Edward Z. Yang wrote:
> Excerpts from Mikhail Vorozhtsov's message of Tue Jan 24 07:26:35 -0500 2012:
>>> Sure, but note that evaluate for IO is implemented with seq# under the hood,
>>> so as long as you actually get ordering in your monad it's fairly straightforward
>>> to implement evaluate.  (Remember that the ability to /catch/ an error
>>> thrown by evaluate is separate from the ability to /evaluate/ a thunk which
>>> might throw an error.)
>> Yes, of course. The purpose of MonadUnbottom is to guarantee that
>> `Control.Exception.throw e ∷ μ α = abort (toException e)`. The choice of
>> a class method is somewhat arbitrary here (one could go with 'α → μ
>> (Either SomeException α)` or with no methods at all).
>
> I want to highlight the strangeness of "exception-like" monads that don't have
> a MonadUnbottom instance (for concreteness, let's assume that there are no
> methods associated with it.  What would you expect this code to do?
>
>      catch (throw (UserError "Foo")) (putStrLn "caught")>>  putStrLn "ignored result"
>
> If we don't have ordering, the monad is permitted to entirely ignore the thrown
> exception. (In fact, you can see this with the lazy state monad, so long as you
> don't force the state value.) Just like in lazy IO, exceptions can move around
> to places you don't expect them.
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 = ⊥`.

[snip]
>>> Stepping back for a moment, I think the conversation here would be helped if we
>>> dropped loaded terms like "general" and "precise" and talked about concrete
>>> properties:
>>>
>>>       - A typeclass has more/less laws (equivalently, the typeclass constrains
>>>         what else an object can do, outside of an instance),
>>>       - A typeclass requires an instance to support more/less operations,
>>>       - A typeclass can be implemented for more/less objects
>>>
>>> One important point is that "general" is not necessarily "good".  For example,
>>> imagine I have a monad typeclass that has the "referential transparency" law
>>> (why are you using a monad?! Well, never mind that for now.)  Obviously, the IO
>>> monad cannot be validly be an instance of this typeclass. But despite only
>>> admitting instances for a subset of monads, being "less general", I think most
>>> people who've bought into Haskell agree, referentially transparent code
>>> is good code!  This is the essential tension of generality and specificity:
>>> if it's too general, "anything goes", but if it's too specific, it lacks elegance.
>>>
>>> So, there is a definitive and tangible difference between "all bottoms are recoverable"
>>> and "some bottoms are recoverable."  The former corresponds to an extra law
>>> along the lines of "I can always catch exceptions."  This makes reduces the
>>> number of objects the typeclass can be implemented for (or, if you may,
>>> it reduces the number of admissible implementations for the typeclass), but
>>> I would like to defend this as good, much like referential transparency
>>> is a good restriction.
>> OK, what MonadUnrecoverableException exactly do you have in mind?
>
> I don't know, I've never needed one! :^)
>
>> I was thinking about something like (no asynchronous exceptions for now):
>>
>> -- ABORTS(μ) ⊆ RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ) ⊆ ZEROS(μ)
>
> Do you have a motivation behind this division?  Are there non-finalizable
> but recoverable zeros? Why can't I use aborts to throw non-recoverable
> or non-finalizable zeros? Maybe there should be a hierarchy of recoverability,
> since I might have a top-level controller which can "kill and spawn" processes?
> Maybe we actually want a lattice structure?
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(μ)

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`.

> Someone has put a term for this problem before: it is an "embarassment of riches".
> There is so much latitude of choice here that it's hard to know what the right
> thing to do is.
>
>> -- RECOVERABLE_ZEROS = zeros recoverable /by `recover`/.
>> -- e.g. `mzero` may not be in RECOVERABLE_ZEROS, even though it is
>> -- recoverable by `mplus`.
>> class MonadAbort e μ ⇒ MonadRecover e μ | μ → e where
>>     -- let eval m = recover (Right<$>  m) (return . Left)
>>     -- LAWS:
>>     -- eval (return a) = return $ Right a
>>     -- eval (abort e) = return $ Left e
>>     -- eval (m>>= f) = eval m>>= either (return . Left) (eval . f)
>>     recover ∷ μ α → (e → μ α) → μ α
>>
>> -- RECOVERABLE_ZEROS(μ) = ZEROS(μ)
>> class MonadRecover e μ ⇒ MonadRecoverAll e μ | μ → e where
>>     -- EXTRA LAW:
>>     -- ∀ z ∷ μ α . (∀ f ∷ α → μ β . z>>= f = z)
>>     --             =>  eval z = return $ Left ERROR(z)
>>     -- No new methods.
>>
>> finallyDefault ∷ MonadRecoverAll e μ ⇒ μ α → (Maybe α → μ β) → μ (α, β)
>> finallyDefault m f = do
>>     a ← m `recover` \e → f Nothing>>  abort e
>>     (a, )<$>  f (Just a)
>
> I must admit, I have some difficulty seeing what is going on here.  Does
> the instance of a type class indicates there /exist/ zeros of some type
> (zeros that would otherwise be untouchable?)
A MonadRecoverAll instance indicates that /all/ (can be relaxed to "all 
finalizable") left zeros are recoverable by `recover`. The 
implementation dependent meta-function `ERROR` maps zeros to the error 
type `e` (but `ERROR (abort e) = e` always holds).

>>> Well, in that case, recover/finally are being awfully nosy sticking their
>>> laws into non-bottom zeros. :^)
>> `recover` should be tied to `abort` in the same manner as `mplus` is
>> tied to `mzero`. But I admit that MonadFinally is wacky, I can't even
>> give laws for it.
>
> It would be cool if we could figure this out.
The "no error" and "recoverable error" scenarios are simple. But when an 
unrecoverable error occurs, the finalizer may well be executed in a 
different environment altogether (e.g. something like C `atexit`).

>>> I want to squash all the typeclasses into one, staying as close to IO
>>> exceptions as possible.  This is because bottom is special, and I think
>>> it's worth giving a typeclass for handling it specially.  Let's call
>>> this typeclass MonadException.
>> So I won't be able to use `catch` with `ErrorT SomeException` or
>> interpreters that do not handle bottoms?
>
> 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.

> Some other points here:
>
>      - Why not use exceptions? I've always thought ErrorT was not such a good
>        idea, if you are in an IO based monad stack. If you're in a
>        left-associated stack of binds, exceptions are more efficient. (The
>        obvious answer is: you want the semantics to be different. But then...)
>
>      - 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.

>>> MonadPlus is a fine typeclass and can be left as is.  I don't think
>>> MonadException should interact with MonadPlus zeros. In fact, I don't
>>> even think IO should really be MonadPlus.
>> What about `MaybeT IO` and STM?
>
> 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 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`.

>>> I make no claim about whether or not a modular API would make sense for
>>> the unrecoverable/recoverable exception idea.  Maybe it does, I haven't
>>> thought hard enough about it. However, I definitely object to such an API
>>> being used in a generic fashion, for ordinary IO as well.
>> Then we'll need two different APIs for error handling. One for "exactly
>> like IO" and one for "not exactly like IO". And all the common idioms
>> (starting with the contents of `Control.Exception`) will need to be
>> implemented twice. I just want to be able to write
>>
>> -- Assuming the ConstraintKinds extension is enabled.
>> type MonadException μ = (MonadAbort SomeException μ, ...)
>>
>> and get all the utilities for free.
>
> 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.