Excerpts from Mikhail Vorozhtsov's message of Tue Jan 17 06:29:12 -0500 2012:
The vehicle of implementation here is kind of important. If they are implemented as asynchronous exceptions, I can in fact still throw in this universe: I just attempt to execute the equivalent of 'undefined :: m a'. Since asynchronous exceptions can always be thrown from pure code, I can /always/ do this, no matter how you lock down the types. Indeed, I think implementing this functionality on asynchronous exceptions is a good idea, because it lets you handle nonterminating pure code nicely, and allows you to bail out even when you're not doing monadic execution. I don't like there this is going. Arguments like this destroy the whole point of having abstract interfaces. I took liftBase from you and now you are picking lock on my back door with raise#. I can deny this by hiding the constructor of the asynchronous exception I use for passing `lavel` in my implementation. But seriously. Next thing I know you will be sneaking down my chimney with `unsafePerformIO` in your hands. It is no question that the type system cannot protect us from all the tricks RTS provides, but we still can rely on conventions of use.
Personally I'm not a fan of exceptions in pure code. If something can fail it should be reflected in its type, otherwise I consider it a bug. The only scenario I'm comfortable with is using asynchronous exceptions to interrupt some number crunching.
Well, that's the kind of language we live in. The denotation of our language always permits for bottom values, and it's not a terribly far jump from there to undefined and error "foo". I don't consider the use of these facilities to be a trap door. Non-termination is a bug (when termination is expected) and I wish that `undefined` and `error` would be interpreted as bugs too (when a value is expected). Putting asynchronous exceptions aside, in some situations it might be useful to recover from bugs, but they should not be treated
On 01/18/2012 02:45 AM, Edward Z. Yang wrote: like /errors/, something that is expected to happen. At least I like to think this way when `error`s meet monads. For example, what is the meaning of `error` in this piece: nasty ∷ Monad μ ⇒ μ () nasty = error "FOO" >> return () runIdentity nasty ~> () -- error is not necessarily a left zero! runIdentity $ runMaybeT nasty ~> error It's just slipping through abstraction and doing what it wants.
Hm, are you against splitting MonadPlus too?
The problem with MonadPlus is not the fact that it has mplus/mzero, but that there are in fact multiple disjoint sets of laws that instances obey. The only other point of order is that MonadZero is a useful abstraction by itself, and that's the point of debate. What is the "usefulness" here? Is being precise not enough?
contract ∷ MonadZero μ ⇒ (α → Bool) → (β → Bool) → (α → μ β) → α → μ β contract pre post body x = do unless (pre x) mzero y ← body x unless (post y) mzero return y Why would I drag `mplus` here? `contract` is useful regardless of whether you have a choice operation or not.
You are forgetting about `ST`. For example, in `ErrorT SomeException ST` finalizers /do/ make sense. It's not about having IO, it is about having some sort of state(fulness).
Conceded. Although there are several responses:
- We only have three magical base monads: IO, ST and STM. In ST we do not have any appreciable control over traditional IO exceptions, so the discussion there is strictly limited to pure mechanisms of failure.
Why is this distinction necessary? Why are you trying to tie exception handling idioms to the particular implementation in RTS?
- Finalizing "mutable state" is a very limited use-case; unlike C++ we can't deallocate the state, unlike IO there are no external scarce resources, so the only thing you really might see is rolling back the state to some previous version, in which case you really ought not to be using ST for that purpose.
Maybe. But you can. And who said that we should consider only IO, ST and STM? Maybe it is a mysterious stateful monad X keeping tabs on god-knows-what. Also, even though we do not deallocate memory directly, having a reference to some gigantic data structure by mistake could hurt too.
I think that's incoherent. To draw out your MaybeT IO example to its logical conclusion, you've just created two types of zeros, only one of which interacts with 'recover' but both of which interact with 'finally'. Down this inconsistency lies madness! Really, we'd like 'recover' to handle Nothing's: and actually we can: introduce a distinguished SomeException value that corresponds to nothings, and setup abort to transform that not into an IO exception but a pure Nothing value. Then 'finally' as written works. I see no inconsistency here. I just give implementers an opportunity to decide which failures are recoverable (with `recover`) and which are not, without sacrificing proper resource/state management. You approach rejects unrecoverable failures completely. Back to this particular case. I implemented `MonadRecover e (MaybeT μ)` this way because that's how I usually use `MaybeT IO`: `catch` for exceptions, `mplus` for `mzero`s. BTW that is also how STM works: `catchSTM` for exceptions, `orElse` for `retry`s. Ideally we should have different ways of recovering from different kinds of failures (and some kinds should not be allowed to be "thrown" by client code) in our abstract setting too. But I don't think that's easily expressible in the type system we have today (at least without confusing type inference). Injecting failures into exception hierarchy is too value-level for me.
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`).
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. [snip]
Regarding `finally`. I was certainly aware that it is not a primop, that's why I wrote "induced /mainly/ by primops". The generalization of `finally` is somewhat natural if you think about it. We start with IO, there the set of reasons why control can escape is fixed, then we proceed to MaybeT and a new "zero" pops up. Then we ask ourselves a question "what if we had more, possibly unrecoverable, failures/zeros?". In the end it boils down to changing `finally` documentation from "computation to run afterward (even if an exception was raised)" to "computation to run when control escapes".
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`.
`recover` is interdefinable with `eval`: eval m = recover (Right <$> m) (return . Left) recover m f = eval m >>= either (\e → f e >> abort e) return We would probably both agree that eval (abort e) = return (Left e) and (if we forget about asynchronous exceptions) eval (return a) = return (Right a) eval (m >>= f) = eval m >>= either (return . Left) (eval . f) What about `eval (error "FOO")`? Sometimes it is `error "FOO"`, sometimes `return $ Left (ErrorCall "FOO")`, sometimes it is a pure nonsense (interpreter goes bananas). What about `eval mzero`? My answer is "I want precision, so I will leave it as implementation dependent". Otherwise I would be forced to use `catchSTM`/`Control.Exception.catch` instead of the generic `catch` when I work with STM/`MaybeT IO`. Writing catches (...) [Handler \MZeroException -> mzero, Handler \(e ∷ SomeException) -> ...] is just ugly.