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)
Except.ok #[1, 58, 255, 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 instance of type class
MonadStateOf (Array UInt8) (Except String)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.modifyThe (Array UInt8) (·.push b))
fun e =>
failed to synthesize instance of type class
MonadStateOf (Array String) (Except String)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.modifyThe (Array String) (·.push e))
failed to synthesize instance of type class
MonadStateOf (Array String) (Except String)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance 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))
Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])
