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