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
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
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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
