One example is Except.tryCatch:
Except.tryCatch.{u, v} {ε : Type u} {α : Type v}
(ma : Except ε α) (handle : ε → Except ε α) :
Except ε α
Both of its parameters are in Except ε.
MonadLift can lift the entire application of the handler.
The function getBytes, which extracts the single bytes from an array of Nats using state and exceptions, is written without Lean.Parser.Term.do : termdo-notation or automatic lifting in order to make its structure explicit.
set_option autoLift false
def getByte (n : Nat) : Except String UInt8 :=
if n < 256 then
pure n.toUInt8
else throw s!"Out of range: {n}"
def getBytes (input : Array Nat) : StateT (Array UInt8) (Except String) Unit := do
input.forM fun i =>
liftM (Except.tryCatch (some <$> getByte i) fun _ => pure none) >>=
fun
| some b => modify (·.push b)
| none => pure ()
Except.ok #[1, 58, 255, 2]#eval getBytes #[1, 58, 255, 300, 2, 1000000] |>.run #[] |>.map (·.2)
getBytes uses an Option returned from the lifted action to signal the desired state updates.
This quickly becomes unwieldy if there is more than one way to react to the inner action, such as saving handled exceptions.
Ideally, state updates would be performed within the tryCatch call directly.
Attempting to save bytes and handled exceptions does not work, however, because the arguments to Except.tryCatch have type Except String Unit:
def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do
input.forM fun i =>
liftM
(Except.tryCatch
(getByte i >>= fun b =>
failed to synthesize
MonadStateOf (Array UInt8) (Except String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array UInt8) (·.push b))
fun e =>
failed to synthesize
MonadStateOf (Array String) (Except String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array String) (·.push e))
failed to synthesize
MonadStateOf (Array String) (Except String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
Because StateT has a MonadControl instance, control can be used instead of liftM.
It provides the inner action with an interpreter for the outer monad.
In the case of StateT, this interpreter expects that the inner monad returns a tuple that includes the updated state, and takes care of providing the initial state and extracting the updated state from the tuple.
def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do
input.forM fun i =>
control fun run =>
(Except.tryCatch
(getByte i >>= fun b =>
run (modifyThe (Array UInt8) (·.push b))))
fun e =>
run (modifyThe (Array String) (·.push e))
Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])#eval
getBytes' #[1, 58, 255, 300, 2, 1000000]
|>.run #[] |>.run #[]
|>.map (fun (((), bytes), errs) => (bytes, errs))
