feat: add a MonadError instance for ContT

[eric-wieser]

We already have a MonadExcept instance; this promotes it to MonadError.

This also documents an issue with the existing MonadExcept instance, but doesn't attempt to fix it.

---

[kmill]

Hmm, I know this was the pre-existing implementation of MonadExcept, but it's not good:

def foo : ContT Bool Lean.MetaM Bool := do
  let x ← try pure true catch _ => return false
  throwError "oh no {x}"

#eval foo.run pure
-- false

The exception from the continuation is able to throw back into the try/catch. I'll check the haskell library this module is based on to see if they have a solution.

[kmill]

I don't think this is salvageable. The issue is that act needs to be constrained to ContT r m r so that we can delimit the continuation.

def ContT.tryCatch [Monad m] [MonadExceptOf ε m] (act : ContT r m r) (h : ε → ContT r m α) :
    ContT r m α := fun c =>
  MonadExceptOf.tryCatch (act pure) (fun e => h e c)

Edit: That code is not right. I don't have act pure being fed into the continuation c...

[kmill]

By the way, we should add https://hub.darcs.net/ross/transformers/browse/Control/Monad/Trans/Cont.hs to the module docs since mtl imports transformers. There are still some definitions this library has that we don't have. (evalContT is what I called ContT.delimit elsewhere.)

[kmill]

Maybe this is it? Notice that ε has to be in the same universe as r, and everything has to be constrained to ContT r m r.

def ContT.tryCatch (ε : Type u) [Monad m] [MonadExceptOf ε m]
    (act : ContT r m r) (h : ε → ContT r m r) :
    ContT r m r := fun c => do
  match ← try Sum.inr <$> act pure catch e => pure (Sum.inl e) with
    | Sum.inr v => c v
    | Sum.inl e => h e c

[eric-wieser]

Hmm, I know this was the pre-existing implementation of MonadExcept

I've changed it to call the other implementation, so that we only have the incorrect code in one place rather than two!

[kmill]

Maybe we should add my nonlocal throwError example into the docstring for MonadExcept as a warning?

[eric-wieser]

I was hoping something like this might work, but I guess there's nowhere to pass through b:

  tryCatch act h f := do
    let mut b : Bool := true
    try
      act (fun a => do
        try
          f a
        catch e2 =>
          b := false -- not legal
          throw e2
      )
    catch e =>
      if b then h e f else throw e

[kmill]

Yeah, I was thinking about wrapping the continuation in a try/catch too and came to the same conclusion.

In a way, try/catch for ContT isn't a good idea because you can't force a finally to actually run. You can always do an early exit from anywhere. In Scheme, they've worked out all this business with dynamic-wind to detect when you're calling a continuation and leaving a dynamic scope, so you can have continuation-safe finallys. It seems the only way to do this is to delimit continuations and chain them together (which is my vague understanding of how dynamic-wind works).

[eric-wieser]

Maybe we should add my nonlocal throwError example into the docstring for MonadExcept as a warning?

Done.

[eric-wieser]

I made a Zulip thread

[kmill]

Could you add

<https://hub.darcs.net/ross/transformers/browse/Control/Monad/Trans/Cont.hs>

to right after line 20? The mts library doesn't actually implement the ContT transformer itself, so it'd be good to link to the relevant part of the transformers library too.

[eric-wieser]

Done

[YaelDillies]

Can you merge master to fix the build?

[eric-wieser]

Done. Since this doesn't make the MonadExcept instance any worse, are we happy to put this in as is?

[YaelDillies]

I agree that it isn't worse.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[Vierkantor]

What is the interaction between getRef and continuations? If I capture a getRef in the current continuation and call it twice, do I get the same reference twice or two different ones?

[Vierkantor]

I agree this doesn't make the exception situation much worse, but does it actually work well with refs?