[Haskell-cafe] Monad-control rant

[Edward Z. Yang]

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.

> > I think your simulation is incomplete. Let's make this concrete: suppose I'm
> > running one of these programs, and I type ^C (because I want to stop the
> > program and do something else.)  In normal 'run' operation, I would expect
> > the program to run some cleanup operations and then exit.  But there's
> > no way for the simulation to do that! We've lost something here.
> I'm not sure I would want to go ^C on a power plant controlling 
> software, but OK. We could accommodate external interruptions by:
> 
> 1. Adding `Finally ∷ Controller α → (Maybe α → Controller β) → Command 
> (α, β)` and a `MonadFinally Controller` instance (and modifying 
> interpreters to maintain finalizer stacks):
> 
> instance MonadFinally Controller where
>    finally' m = singleton . Finally m
> 
> 2. Writing more simulators with different interruption strategies (e.g. 
> using StdGen, or `interrupt ∷ PowerPlantState → Bool`, etc).

I think this scheme would work, because your interpreter slices up the actions
finely enough so that the interpreter always gets back control before some
action happens.

> > 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?

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?)

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

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

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?

> > 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!

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

> > 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?

Cheers,
Edward