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:
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. OK, what MonadUnrecoverableException exactly do you have in mind? I was
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). 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) -- 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)
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. :^) `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.