RFC: better UX around `throw`?

[JamesGallicchio]

Proposal

Currently, throw "error" : IO A does not typecheck. I would like it to typecheck.

Reasoning:

• As a seasoned Lean programmer it is still hard for me to remember .userError when trying to throw in IO. I suspect this is deeply unfriendly to beginners.
• There is a canonical coercion from String to IO.Error, via .userError.
• User code in IO almost always wants to throw via this canonical coercion, rather than the more internal-to-IO errors.

I have no ideas for how to do this without some major changes to MonadExcept. Suggestions appreciated.

One (bad) option would be to add a MonadExceptOf instance:

instance (priority := low) : MonadExceptOf String IO where
  throw e := throw (.userError e)
  tryCatch x f := tryCatch x (fun
    | .userError e => f e
    | e => throw e)

#check show IO Unit from throwThe String "hi"
#check show IO Unit from throw (.userError "hi")

but this requires throwThe String rather than throw, which I find no better than the status quo.

Community Feedback

Small bit of discussion here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Map.20of.20Lean's.20monads

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[tydeu]

One potential type-class-based solution that eliminates the need for throwThe at the cost of losing support for implicit-type . constructors (e.g., throw (.userError "hi") would have to be written as throw (IO.userError "hi")):

namespace Issue3128

#check show IO Unit from throw "hi" -- fails
#check show IO Unit from throw (IO.userError "hi") -- works
#check show IO Unit from throw (.userError "hi") -- works

class MonadThrow (ε : semiOutParam $ Type u) (m : Type v → Type w) where
  throw : ε → m α

export MonadThrow (throw)

abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadThrow ε m] {α : Type v} (e : ε) : m α :=
  throw e

instance [MonadExceptOf ε m] : MonadThrow ε m where
  throw := MonadExceptOf.throw

instance [MonadThrow α m] [Coe β α] : MonadThrow β m where
  throw e := throwThe α ↑e

#check show IO Unit from throw "hi" -- works
#check show IO Unit from throw (IO.userError "hi") -- works
#check show IO Unit from throw (.userError "hi") -- fails

[kim-em]

@tydeu's suggestion looks like a net positive to me.

[Kha]

It would be good to first look at whether support for the combination of out-params and coercions cannot be improved in general. There already is special handling for out-params in the app result type, but not yet in arguments.

[tydeu]

Revisiting this, I have since discovered that @[default_instance] can be used to get the best of both worlds:

namespace Issue3128

#check show IO Unit from throw "hi" -- fails
#check show IO Unit from throw (IO.userError "hi") -- works
#check show IO Unit from throw (.userError "hi") -- works

class MonadThrow (ε : semiOutParam $ Type u) (m : Type v → Type w) where
  throw : ε → m α

export MonadThrow (throw)

abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadThrow ε m] {α : Type v} (e : ε) : m α :=
  throw e

@[default_instance] instance [MonadExcept ε m] : MonadThrow ε m where
  throw := MonadExcept.throw

instance [MonadThrow α m] [Coe β α] : MonadThrow β m where
  throw e := throwThe α ↑e

#check show IO Unit from throw "hi" -- works
#check show IO Unit from throw (IO.userError "hi") -- works
#check show IO Unit from throw (.userError "hi") -- works

Also, if the use of coercions in synthesis is a concern, we can avoid them altogether with instances like:

instance [MonadThrow IO.Error m] : MonadThrow String m where
  throw e := throwThe IO.Error e