[Haskell-cafe] Monad-control rant
mikhail.vorozhtsov at gmail.com
Sat Jan 21 15:25:07 CET 2012
On 01/18/2012 10:43 PM, Edward Z. Yang wrote:
> Excerpts from Mikhail Vorozhtsov's message of Wed Jan 18 08:47:37 -0500 2012:
>>> 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
>> 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.
> I can't argue with "error should be used sparingly, and usually in cases
> where there is an indication of developer error, rather than user error."
> It's good, sound advice.
> 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.
> 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.
>>> - 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?
> The distinction I'm trying to make is between code that is pure (and cannot
> witness bottoms), and code that is impure, and *can* witness bottoms.
> It is true that I need language/RTS support to do the latter, but I'm
> in no way tying myself to a particular implementation of an RTS: the semantics
> are independent (and indeed are implemented in all of the other Haskell implementations.)
>>> - 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
> Claim: such a mysterious monad would have to be backed by IO/ST. (In the
> case of a pure State monad, once we exit the monad all of that gets garbage
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?
>>> 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.
I think that in general we should prefer a more widely applicable API,
going into specifics only when we actually need them.
>>> 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`
>>> 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`.
>> `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
> I think my previous comments apply here.
>> catches (...) [Handler \MZeroException -> mzero,
>> Handler \(e ∷ SomeException) -> ...]
>> is just ugly.
> I agree that this is ugly. (But, I admit, it does have a sort of theoretical
> unity about it.)
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.
More information about the Haskell-Cafe