[Haskell-cafe] Monad-control rant

[Mikhail Vorozhtsov]

On 01/18/2012 02:45 AM, Edward Z. Yang wrote:
> 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 
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.