[Haskell-cafe] Monad-control rant

[Edward Z. Yang]

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.

I like to think of this another way: because in Haskell actually contains pure code,
we should take advantage of this fact, and unceremoniously terminate pure code
when we like: while also having a nice semantics for what this means, to boot.

Hiding the constructor of your exception is clever, and means this argument is
nullified if your exception system (or at least bits of it: more on this later0
doesn't handle all exceptions.

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

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

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

> > 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.  For example, what happens in these cases:

    retry `recover` \e -> writeTVar t v
    retry `finally` writeTVar t v
    error "foo" `mplus` return ()

Tread carefully.

> Not thirteen:
>    1. MonadRecover covers catch# and catchSTM#
>    2. MonadAbort covers raiseIO#
>    3. MonadMask covers maskAsyncExceptions# + maskUninterruptible# + 
> unmaskAsyncException#
>    4. MonadPlus covers catchRetry#
>    5. Some class for fork# and forkOn# (capability type can be 
> abstracted the same way the mask type is abstracted in MonadMask)
> 
> Lifting atomically# is simple:
> 
> atomically ∷ MonadBase IO μ ⇒ STM α → μ α
> atomically = liftBase . STM.atomically
> 
> check# and finalizeWeak# cannot be fully generalized because of their 
> semantics. Suppose we want to lift `mkWeak` to `StateT s IO` manually, 
> without relying on some generic mechanism. I just don't see any coherent 
> meaning of accessing/modifying state in the finalizer. I would start 
> with a partial generalization (leaving finalizer `IO ()`) and see if 
> someone comes up with a not-trivial (a trivial one would be ReaderT) 
> monad that actually properly implements the fully generalized version in 
> a meaningful way.

Thanks for doing that legwork. I didn't do very much except go look at
the primops list. :-)

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

> Notice that copy-pasting is only needed for control operations, which 
> are clearly a minority of the functions exported by `base`. All other 
> functions could be lifted the same way lifted-base does it, with liftBase.

I think the number is nontrivial, despite being a minority. But I haven't
run the numbers.

> I think it would be wiser to invest time into improving GHC 
> specializer/optimizer than to try to sidestep the issue by choosing 
> poor-but-already-optimizable abstractions.

Worth thinking about.

> I wouldn't be too optimistic about convincing GHC HQ. Even making 
> Applicative a superclass of Monad can make Haskell98 nazis come after 
> you in ninja suits.

Heh, Functor/Applicative/Monad is something of a mess.

> Regarding orthogonal features. What exactly do you have in mind?

Essentially, every time the GHC team throws a new feature into the IO sin
bin, they have to figure out how it interacts with all of the other features
currently living in the IO sin bin. This is kind of tricky.  A variant of this
problem is why STM is really hard to implement in traditional languages.

I think we're converging on agreement. Hooray!

Cheers,
Edward