Uncaught Exception with List.foldlM ?

Stream: new members

[iwooden]

Hi all, learning Lean 4 with the "Functional Programming in Lean" book, been great fun so far!

I tried modifying the doug utility introduced in chapter 7.1 to handle parsing multiple config arguments using ExceptT. However, I get an uncaught exception error when trying this that I don't understand - the minimally viable code I can find to reproduce this is, in Main.lean:

abbrev ExceptStack := ExceptT String IO Nat

def argToConfig (n : Nat) : String → ExceptStack
  | "--ok" => do
    IO.println "valid arg processed"
    .ok <| pure <| n+1
  | _ => .error "invalid arg"

def buildConfig (xs : List String) : ExceptStack := do
  xs.foldlM argToConfig 0

def main (args : List String) : IO Unit := do
  match (← buildConfig args) with
  | .ok n => IO.println s!"valid: {n}"
  | .error err => IO.println err

Trying to run it gives me:

iwooden@mbp lean-except-bug % lake build
[0/2] Building Main
[1/2] Compiling Main
[2/2] Linking lean-except-bug
iwooden@mbp lean-except-bug % .lake/build/bin/lean-except-bug
valid: 0
iwooden@mbp lean-except-bug % .lake/build/bin/lean-except-bug --ok
valid arg processed
valid: 1
iwooden@mbp lean-except-bug % .lake/build/bin/lean-except-bug --notok
uncaught exception: invalid arg

The idea here is that I have some default object (in chapter 7.1 this would be the Config), use something like List.foldlM to make changes in that object for valid arguments, with "short-circuiting" for invalid arguments. Note that if I use Except String Nat here instead of ExceptT String IO Nat it works, but I'd like the IO context available so I can do e.g. filesystem checks as part of the validation.

I have two questions:

1. Why does this typecheck/compile? I would've hoped to avoid things like uncaught exceptions.
2. What should I use instead of List.foldlM here? I can, of course, manually write a recursive function to traverse the list in this context, but I was hoping there's something in the standard library that would work.

Again, thanks so much for putting work into Lean and the great accompanying books! I'm having a great time, just this one issue has me scratching my head. Thanks!

[iwooden]

Ahhh, got it. After lots of trial and error, that .error inside of argToConfig is (for some reason) an EStateM.Result.error instead of an Except.error. Explicitly using the latter solves this issue and no longer results in an uncaught exception.

Fairly confusing bug for a newcomer, but I guess being more explicit is one of the first things I should have tried.

[iwooden]

(although looking at it a bit more, EStateM should work as well here? Looks like it's supposed to be equivalent to ExceptT ε (StateM σ), not sure why you'd get an uncaught exception from it)

[Mario Carneiro]

The issue is that .error is not resolving the way you might hope/expect: it is EStateM.error, which is the constructor for the exception state of the IO monad, rather than the additional exception path you have added via ExceptT. The String you passed to it is coerced to a IO.Exception and so since you didn't use the tryCatch implementation of the IO monad it propagated a userError "invalid arg" out of main and the runtime caught it.

What you should do instead is use throw, which is the generic function provided by the MonadExcept instance for ExceptT (or even more precisely, throwThe which allows you to specify which type you expect if the monad simultaneously supports throwing more than one type, in your case String and IO.Exception).