[Haskell-cafe] Monad-control rant

[Edward Z. Yang]

Excerpts from Mikhail Vorozhtsov's message of Sat Jan 21 09:25:07 -0500 2012:
> > But I also believe that you can't use this as justification to stick your
> > head in the sand, and pretend bottoms don't exist (regardless of whether or
> > not we'rd talking about asynchronous exceptions.)  The reason is that
> > understanding how code behaves in the presence of bottoms tells you
> > some very important information about its strictness/laziness, and this
> > information is very important for managing the time and space usage of your code.
> I totally agree with you. My point is that things like `evaluate` and 
> `try undefined = return (Left (ErrorCall "Prelude.undefined"))` are 
> magic and should not be taken for granted. Bottoms are everywhere, but 
> the ability to distinguish them from normal values is special. We could 
> have a separate abstraction for this ability:
> 
> class MonadAbort SomeException μ ⇒ MonadUnbottom μ where
>    -- evaluate a = abort (toException e), if WHNF(a) = throw e
>    --              return WHNF(a), otherwise
>    -- join (evaluate m) = m, ensures that `undefined ∷ μ α = abort ...`
>    evaluate ∷ α → μ α
> 
> or something like that.

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

> > The identity monad for which error "FOO" is a left zero is a legitimate monad:
> > it's the strict identity monad (also known as the 'Eval' monad.)  Treatment
> > of bottom is a part of your abstraction!
> >
> > (I previously claimed that we could always use undefined :: m a as a left zero,
> > I now stand corrected: this statement only holds for 'strict' monads, a moniker which
> > describes IO, STM and ST, and any monads based on them. Indeed, I'll stick my neck
> > out and claim any monad which can witness bottoms must be strict.)
> Bottoms may be zeros in strict monads, but they are not necessarily 
> recoverable. `runX (recover (True <$ undefined) (const $ return False))` 
> may be equivalent to `undefined`, not to `runX (return False)`. See my 
> example of such "IO based" X below. I want to have options.

I think this touches on a key disagreement, which is that I think that in IO-like
monads you need to be able to recover from bottoms. See below.

> Let's consider the following X (using the `operational` library):
> 
> data Command α where
>    -- Note that we do not employ exceptions here. If command stream
>    -- transport fails, the interpreter is supposed to start the
>    -- appropriate emergency procedures (or switch to a backup channel).
>    -- Sending more commands wouldn't help anyway.
>    AdjustControlRods ∷ Height → Command Bool
>    AdjustCoolantFlow ∷ ...
>    AdjustSecondaryCoolantFlow ∷ ...
>    RingTheAlarm ∷ ...
>    -- We could even add an unrecoverable (/in the Controller monad/)
>    -- error and the corresponding "finally" command.
>    ...
>    ReadCoolantFlow ∷ ...
>    ...
> 
> type Controller = Program Command
> 
> -- Run a simulation
> simulate ∷ PowerPlantState → Controller α → (α, PowerPlantState)
> -- Run for real
> run ∷ Controller α → IO α
> 
> type X = ErrorT SomeException Controller
> 
> So the effects here are decoupled from control operations. Would you 
> still say that finalizers are useless here because exception handling is 
> implemented by pure means?

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.

> >>> You are free to create another interface that supports "unrecoverable"
> >>> exceptions, and to supply appropriate semantics for this more complicated
> >>> interface. However, I don't think it's appropriate to claim this interface
> >>> is appropriate for IO style exceptions, which are (and users expect) to always
> >>> be recoverable.
> >> Why exactly not? I think that everything useful written with this
> >> assumption in mind can be rewritten to use `finally`, just like I did
> >> with `withMVar` (the version in `base` actually uses `onException`).
> >
> > I think the argument here is similar to your argument: saying that all
> > IO exceptions are recoverable is more precise.  An interface that specifies
> > recoverable exceptions is more precise than an interface that specifies
> > recoverable *and* unrecoverable exceptions.
> There is a crucial difference here. In the MonadZero case, being more 
> precise means having a smaller language (only `mzero`, no `mplus`) and 
> less laws. Which means that the code you write is more general 
> (applicable to a greater number of monads). But in the 
> recoverable/unrecoverable case being more precise means having /more/ 
> laws (all zeros vs only some zeros are recoverable). Therefore the code 
> you write is less general (applicable to a lesser number of monads). 
> Having no unrecoverable errors is a special case of maybe having some.

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.

But the inclusion relation goes the wrong direction.  Perhaps this rephrasing
of your last sentence makes this clear:

> Having no side effects is a special case of maybe having some.

:-)

> >>> For example, what happens in these cases:
> >>>
> >>>       retry `recover` \e ->   writeTVar t v
> >> retry
> >>>       retry `finally` writeTVar t v
> >> instance MonadFinally STM where
> >>     finally' m f = do
> >>       r ← catchSTM (Right<$>  m) (return . Left)
> >>           `mplus` (f Nothing>>  retry)
> >>       either (\e → f Nothing>>  throwSTM e) (\a → (a, )<$>  f (Just a)) r
> >>
> >> ~>  writeTVar t v>>  retry ~>  retry
> >>
> >> retry+finally may actually not be quite as useless as it seems. The
> >> finalizer could contain IORef manipulations (collecting some statistics,
> >> implementing custom retry strategies, etc).
> >>
> >>>       error "foo" `mplus` return ()
> >> It depends. In STM and Maybe it would be `error "foo"`. In some
> >> right-biased monad it could be `return ()`. But that's OK, because
> >> `mplus` is required to have `mzero` as its zero, everything (other kinds
> >> of failures; and `error "foo"` is not necessarily a failure!) on top of
> >> that is implementation dependent. The same goes for `recover`:
> >> everything on top of handling `abort` is implementation dependent.
> >
> > Playing along with the recoverable/unrecoverable idea for a bit,
> > I think I agree with your assessments for the first two cases (the second
> > is a bit weird but I agree that it could be useful.)  But I'm very worried
> > about your refusal to give a law for the third case. In some ways, this
> > is exactly how we got into the MonadPlus mess in the first place.
> I'm not sure I understand. Neither of MonadOr/MonadPlus has laws about 
> `error`, so the behavior is implementation dependent for both `mplus` 
> and `morelse`.

Well, in that case, recover/finally are being awfully nosy sticking their
laws into non-bottom zeros. :^)

> >>> I think the distinction between recoverable and unrecoverable is reasonable,
> >>> and could be the basis for an interesting typeclass. But the notion needs
> >>> to be made a lot more precise.
> >> It is actually not about creating a new typeclass (what methods would it
> >> have anyway?), it is about relaxing rules for `recover`.
> >
> > MonadOr and MonadPlus have functions with the same type signatures, but they
> > are named differently to avoid confusion. I suggest something like that
> > would be useful here.
> The problem with MonadPlus and MonadOr is that their respective laws are 
> incomparable. As I already mentioned, "no unrecoverable errors" is a 
> special case of "maybe some unrecoverable errors", so we have a nice 
> inclusion relation. We could have a "marker" (no new methods, just laws) 
> typeclass for monads with no unrecoverable errors. But I suspect it 
> would be rarely used in the presence of `finally`.

I disagreed.

> So, to sum things up. I want a generic (works with weird interpreters 
> too), modular (several typeclasses) API for error handling. You want to 
> squash all the typeclasses into one, staying as close to IO exceptions 
> as possible and merging MonadPlus in (where applicable). Am I correct? 
> Hopefully I showed that there are some useful monads that do not fit 
> into this "one class to rule them all" approach.

That's close, although misses some subtleties I developed in this message.

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.

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.

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

Cheers,
Edward