[Haskell-cafe] Monad-control rant
mikhail.vorozhtsov at gmail.com
Tue Jan 24 13:26:35 CET 2012
On 01/22/2012 02:47 AM, Edward Z. Yang wrote:
> 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.)
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).
>>> 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.
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).
>>>>> 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
> - 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 was
thinking about something like (no asynchronous exceptions for now):
-- ABORTS(μ) ⊆ RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ) ⊆ ZEROS(μ)
-- 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)
-- 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)
>>>>> For example, what happens in these cases:
>>>>> retry `recover` \e -> writeTVar t v
>>>>> 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. :^)
`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.
>>>>> 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.
So I won't be able to use `catch` with `ErrorT SomeException` or
interpreters that do not handle bottoms?
> 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?
> 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?
> 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.
More information about the Haskell-Cafe