MonadExcept in the ContT monad

Stream: mathlib4

[Eric Wieser]

@Kyle Miller spotted that something is wrong with the tryCatch in the ContT (continuation) monad:

def foo : ContT Bool (Except String) Bool := do
  let x ← try pure true catch _ => return false
  throw s!"oh no {x}"

#eval foo.run pure
-- `Except.ok false`, no error; should be `Except.error "oh no true"`

the github discussion has some ideas for how to fix this, but none of them fully work.

[Eric Wieser]

Kyle suggested

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

which looks correct, but doesn't work for a MonadExcept instance

[Kyle Miller]

ContT also seems like it just might not be suitable for a try/catch, at least if you expect a finally clause that always runs, since ContT lets you do an early return from anywhere. This ContT r m r type seems to be what you need to delimit a continuation. (Here's some Haskell)

[Eric Wieser]

Ah, I hadn't quite made the connection that try/catch enables finally

[Eric Wieser]

And https://www.yesodweb.com/blog/2014/05/exceptions-cont-monads suggests that finally can't exist in ContT

[James Gallicchio]

It is odd that we don't separate catch and mask into two classes. This isn't the first time I've found it awkward.