RFC: MonadFail

Stream: lean4 dev

[Henrik Böving]

Another suggestion from @Siddharth Bhat and my experiences^^

While writing an abstraction that allows users to construct LLVM for a declaration themselves we
ended up trying to write the library on a general transformer instead of a concrete monad, in case the
user wants to use a custom monad to generate their LLVM. As a simplified example consider:

abbrev MyT (m : Type → Type) (a : Type) := ReaderT Context (StateT State m) a

While implementing the API based on this however there are of course cases where the user can provide malformed input (for example referring to a non existing function), so we want to throw an error. However just based on [Monad m] this is not possible. And we did also not want to force the user to have a [MonadExcept String m] instance because for example IO does not have this since it deals with IO.Errors (which do happen to have the case userError : String -> IO.Error though). So basically we ended up reimplementing Haskells MonadFail and declaring an instance for IO.

Would it be reasonable to have this API in general in core? That is a typeclass like MonadFail that allows us to throw a string as an error? And possibly on top of that also an instance [MonadExcept String m] : MonadFail m to make it play nicely with the existing abstractions.

[Mario Carneiro]

Don't we already have MonadExcept, MonadExceptOf, Alternative, and MonadError? I'm really not a fan of having five different typeclasses for "you can throw errors"

[Mario Carneiro]

I think MonadError is the most sensible thing to build on for LLVM errors. In particular it gives you the throwError macro, which lets you interpolate various kinds of structured objects sensibly into the error message. Using strings will lead to a low quality experience by default

[Henrik Böving]

Oh we didn't see monad error, thanks a lot! We'll just use that instead then ^^

[Mac Malone]

Mario Carneiro said:

Don't we already have MonadExcept, MonadExceptOf, Alternative, and MonadError? I'm really not a fan of having five different typeclasses for "you can throw errors"

Which MonadError? :stuck_out_tongue: Both Lake and Lean have one (I named it that before realizing there was already a different one in the Lean core). I would say Lake's is more appropriate for @Henrik Böving 's request. The Lean MonadError does a whole lot more. For example, it stores structured Lean-specific MessageData (and thus imports Lean.Environment, hence making it not very appropriate for non-meta code). However, if this is just to be used within Lean for Lean monads, then it may be sufficient.