lifting transformers

Stream: lean4

[Chris Lovett]

Trying to understand transformers and port https://mmhaskell.com/monads/transformers to lean, there is something I don't quite yet follow in the following code. I find validUserName is of type Except String String and not just String.

def readUserName : ExceptT String IO String := do
  IO.println "Please enter your username:"
  let stdin ← IO.getStdin
  let str ← stdin.getLine
  if str.length > 5 then
    return str.trim
  else throw "Username must be more than 5 characters"

def main : IO Unit := do
  try
    let validUserName ← readUserName
    IO.println s!"Hello, {validUserName}!"
  catch e =>
    IO.println s!"Error: {e}"

I tried also readUserName .run but it doesn't help. So it seems I needs some sort of extra lift here to force the try/catch to do something useful here. I was able to fix it with my liftIO function, but why is this necessary, and is there some easier way to do this?

open EStateM

def liftIO (t : Except String α) : IO α := do
  match t with
  | .ok r => Result.ok r
  | .error s => Result.error s

def main : IO Unit := do
  try
    let validUserName ← readUserName >>= liftIO
    IO.println s!"Hello, {validUserName}!"
  catch e =>
    IO.println s!"Error: {e}"

The liftIO now cases the error case to go to the catch block which is what I wanted?

[Mario Carneiro]

try ... catch desugars to tryCatch, which does not change the type in the body of the try block. So it can't be used to eliminate an Except ... wrapper around the type

[Chris Lovett]

Ok, I figured it had something to do with my main type of IO String not matching so I moved the code to a new function and now it works fine:

def login : ExceptT String IO String:= do
  try
    let username ← readUserName
    let email ← readEmail
    let password ← readPassword
    return s!"Hello, {username}, we are logging you in...!"
  catch e =>
    throw e

def main : IO Unit := do
  IO.println (← login)

[Mario Carneiro]

The simplest fix to your code is to remove the ExceptT like so:

def readUserName : IO String := do
  IO.println "Please enter your username:"
  let stdin ← IO.getStdin
  let str ← stdin.getLine
  if str.length > 5 then
    return str.trim
  else throw ↑"Username must be more than 5 characters"

[Chris Lovett]

Woah, what? IO is not "Except" as far as I know so where did that throw come from, something to do with that tricky up arrow ↑ ?

[Mario Carneiro]

IO is a MonadExcept

[Chris Lovett]

So demonstrating monad transformers with ExceptT String IO String is a bad idea then?

[Mario Carneiro]

but the error type is IO.Error so you need to coerce it from String

[Mario Carneiro]

How about using a simple monad as the base, like StateM Nat?

[Chris Lovett]

So ↑ is a notation for coercion? Where is it defined?

[Mario Carneiro]

https://leanprover-community.github.io/mathlib4_docs///Init/Coe.html

[Chris Lovett]

Found it, thanks: syntax:1024 (name := coeNotation) "↑" term:1024 : term

[Chris Lovett]

Hmmm, ok, the haskell chapter uses OptionT IO String which I also found a bit contrived, given IO can already return errors. So I'll switch to something more like what I wrote in https://github.com/leanprover/lean4-samples/tree/main/SimpleMonads#monad-composition like functions of type StateT Nat (ExceptT String Id) Float.

[Mario Carneiro]

@Leonardo de Moura In this code:

example : IO Unit := throw "hello"
-- failed to synthesize instance
--   MonadExcept String IO

Is this expected / intended behavior? throw has the type

throw [MonadExcept ε m] : ε → m α

where ε is an outParam of MonadExcept, so there is a competition between using the ε from the argument (which is String) and the ε inferred from the MonadExcept instance (which is IO.Error).

[Mario Carneiro]

I think that simple monads like StateT and ExceptT are easier to understand if you are building things from scratch

[Chris Lovett]

I notice mmhaskell uses this:

class MonadTrans t where
  lift :: (Monad m) => m a -> t m a

And the book has these lift commands to access functions on inner monads, but I'm not finding the need for that in Lean? For example, here I'm able to access throw without any lift keywords:

abbrev Arguments := List String

def hasSwitch (name: String) : ReaderT Arguments (Except String) Bool := do
  let args ← read
  if args.contains s!"--{name}" then
    return true
  else
    throw s!"Command line argument --{name} not found"

I assume lifting works differently in lean with MonadLift and all that - which seems to operate more on return values - lifting them to match some larger monad at the call site?

[Sebastian Ullrich]

Yes, automatic monad lifting is described in https://leanprover.github.io/papers/do.pdf#page=18

[Leonardo de Moura]

Mario Carneiro said:

Leonardo de Moura In this code:

example : IO Unit := throw "hello"
-- failed to synthesize instance
--   MonadExcept String IO

Is this expected / intended behavior? throw has the type

throw [MonadExcept ε m] : ε → m α

where ε is an outParam of MonadExcept, so there is a competition between using the ε from the argument (which is String) and the ε inferred from the MonadExcept instance (which is IO.Error).

The type class resolution procedure failed when trying to check whether the synthesized value type had the expected type. Here:
https://github.com/leanprover/lean4/blob/766afdd0bc6c6480113b6dd91033fea871028fcd/src/Lean/Meta/SynthInstance.lean#L695
I agree this is a different kind of failure. Moreover, it does not give the caller the opportunity to do something about it (e.g., adding a coercion).
We can get more information using set_option trace.Meta.synthInstance true. BTW, the new tracing infrastructure that @Gabriel Ebner implemented looks great. We get:
image.png
Then, we can expand the trace and get
image.png