[Haskell-cafe] Monad-control rant

[Edward Z. Yang]

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.

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.)

> 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.

Point conceded. (Though, I probably would have used 'error' for 'contract',
since violation of pre/post-conditions is almost certainly due to developer
error.)

> >      - 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 
> too.

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
collected.)

> > 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.

> > 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 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.

> `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.)

Edward