help with do notation

Stream: lean4

[Chris Lovett]

How do I switch this function to use do notation?

def divideWithArgs (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float :=
  if y == 0 then
    throw "can't divide by zero"
  else
    bind (modify fun s => s + 1) fun _ =>
      bind (get) fun s =>
        bind (read) fun args =>
          if (s > 10 && args.contains "--limit") then
            throw "too many divides"
          else
            pure (x / y)

I tried this but I get a compile error:

def divideWithArgsDo (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float := do
  if y == 0 then
    throw "can't divide by zero"
  else
    modify fun s => s + 1
    get fun s =>
      read fun args =>
        if (s > 10 && args.contains "--limit") then
          throw "too many divides"
        else  pure (x / y)

saying:

function expected at
  get
term has type
  ?m.5037 ?m.5036

This simpler version works fine:

def divideDo (x:Float) (y:Float) : (StateT Nat (ExceptT String Id)) Float := do
  if y == 0 then
    throw "can't divide by zero"
  else
    modify fun s => s + 1
    pure (x / y)

problem seems to be with get, so how do I use get and do notation?

[Henrik Böving]

def divideWithArgs (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float :=
  if y == 0 then
    throw "can't divide by zero"
  else
    bind (modify fun s => s + 1) fun _ =>
      bind (get) fun s =>
        bind (read) fun args =>
          if (s > 10 && args.contains "--limit") then
            throw "too many divides"
          else
            pure (x / y)


def divideWithArgsDo (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float := do
  if y == 0 then
    throw "can't divide by zero"
  else
    modify fun s => s + 1
    let s ← get
    let args ← read
    if (s > 10 && args.contains "--limit") then
      throw "too many divides"
    else
      pure (x / y)


example : divideWithArgs x y = divideWithArgsDo x y := by
  simp[divideWithArgs, divideWithArgsDo]

with an extra equivalence proof on top^^

[Henrik Böving]

I'm a little surprised you are trying to work this way around (this way being, from written out binds to do notation) especially due to the very ergonomic way that the Lean do notation is implemented it is usually much easier to go do notation -> written out binds understanding wise.

Because what is get really, just a function that has type get : m σ where m is some state monad and σ is the state. and what do we want to do in do notatino if we want to access a value that is wrapped within a monad? We <- it, hence we end up with let s <- get

[Chris Lovett]

Oh, I'm just trying to learn monads, and understanding bind and all the heavy lifting do notation does for me... so thanks again for the quick unblock, and I love that you threw in the proof to boot, you rock!

[Chris Lovett]

Monad lifting is cool. But why can't I do this simple test in main below:

def divide (x: Float ) (y: Float): ExceptT String Id Float :=
  if y == 0 then
    throw "can't divide by zero"
  else
    pure (x / y)

def divideRefactored (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float := do
  modify fun s => s + 1
  let s ← get
  let args ← read
  if (s > 10 && args.contains "--limit") then
    throw "too many divides"
  else
    divide x y

def main : IO Unit := do
  let x ← (divideRefactored 5 0 [] 0)
  IO.println "hello"

type mismatch
  divideRefactored 5 0 [] 0
has type
  ExceptT String Id (Float × Nat) : Type
but is expected to have type
  IO ?m.246 : Type

Looks like it's complaining that IO is missing? Does this mean 'IO' cannot be lifted?
Looks like I can't even discard (divideRefactored 5 0 [] 0).
I can do the following instead, but I was trying to be lazy and avoid the big match statement...

def main : IO Unit := do
  IO.println (match (divideRefactored 5 0 [] 0) with
  | Except.error s => s
  | Except.ok r => toString r)

[Henrik Böving]

If we have an instance MonadLiftT m n that means there is a way on how to turn a computation that happens inside of m into one that happens inside of n and (this is the key part) usually without the instance itself creating any additional data that feeds into the computation. To answer your first question, this means you can in principle declare lifting instances from any monad to any other monad, it does not however mean that you should do this as we will see.

Also as a little side note, the question "Does this mean 'IO' cannot be lifted" is not the question you want to ask here, the monad you want to be lifted is ExceptT String Id into IO. Not the other way around. After all you have a computation in that ExceptT String Id monad and want to execute it (i.e. lift it into) into a computation that is happening within IO.

IO is an EIO IO.Error where EIO is basically a mix of a state + an except monad but without monad transfomers instead done inside of a single monad. Now if we look at your type the ExceptT transformer has String as its error type but it is not obvious how we can go from String to IO.Error, yes there is IO.Error.userError which operates on String but maybe the user intended something different (there are more than a dozen IO.Error variants after all) hence it is not obvious how to go from ExceptT String m a to IO (m a) or even IO a in this case since m is Id. Yes the MonadLift instance could make a guess here and say "well surely they want IO.Error.userError but maybe they also wanted to use another variant that takes a string and suddenly you end up with a certain error variant where you didnt know where it came from.

MonadLift instances that we do want to have on the other side are the ones where it is more or less "obvious" what to do, for example if you have a monad stack ReaderT Context (StateT State IO) it is obvious how one might lift a computation from IO into this monad, we simply let the computation ignore the ReaderT Context and the StateT State and just use the IO part of this stack. What is not obvious on the other side is how we can go the other way, if i want to execute a ReaderT Context (StateT State IO) inside of IO what should the Context and the State I am giving to this computation be? Hence lifting this way around does not work.

Finally a little style thing. While it is a nice thing that many monads can be represented as just regular functions you usually do not want to give the arguments to these hidden functions directly like you are doing here. This has two reasons mostly

1. It looks confusing because if you look at the documentation of the function this monad might be hidden behind an abbrev, for example in Lean compiler code we often observe:

abbrev M := ReaderT (List String) (StateT Nat (ExceptT String Id))

def  divideRefactored (x:Float) (y:Float) : M Float := ...

If you now go to the definition of divideRefactored based on the call site here: divideRefactored 5 0 [] 0 you would expect there to be 4 parameters but there are only 2, this is confusing at first if you do not know about what M is

2. It might make your code brittle to changes in case you add a new parameter after the case

What we do instead is use the run functions that are provided on most monads and monad transformers: docs4#StateT.run docs4#ReaderT.run etc. so your call site would usually look more like this: divideRefactored 5 0 |>.run [] |>.run 0 This way the type checker will always ensure for you that the result of divideRefactored 5 0 is a type that has some run method and so on, if this is not the case it will highlight the right section of your code instead of giving a confusing big error on your entire application that contains some weird monad stack mess.

Furthermore we would usually also split your match statement up:

def main : IO Unit := do
  let ret := divideRefactored 5 0 |>.run [] |>.run 0
  let final := match ret with
  | .ok s => toString s
  | .error e => e
  IO.println s!"{final}"

Also as you will already have observed both docs4#StateT.run and the regular application as a function will give you both the result of your computation as fell as the final state at the time of return as a tuple, a way to avoid this is is to use the StateT.run' function which will only give you the result and drop the state

[Henrik Böving]

Now I'm off to bed though so more monad support tomorrow :P

[Chris Lovett]

Can I steal all this great stuff and include it in my new sample: https://github.com/leanprover/lean4-samples/tree/clovett/monads/SimpleMonads ?

[Chris Lovett]

I'm also curious why this let statement requires any conversion? Doesn't the IO.println (toString ret) make everything a nice IO return type or does every statement of the try block have to match the return type IO Unit?

def main (args: List String): IO Unit := do
  try
    let ret ← (divideRefactored 5 0 args 10)
    IO.println (toString ret)
  catch e =>
    IO.println e

I was able to make this compile by adding the following conversion writing let ret ← liftIO (divideRefactored 5 0 args 10) where:

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

but I'm not sure I can explain how this works, seems like some automatic lifting is happening here also, and I couldn't figure out how to package this as a proper MonadLift transform so that it could be automatically inserted...

[Henrik Böving]

Sure you can take whatever of my examples and put it thetr ^^

In this case its not a lifting going on its a coercion from String to IO.userError in the Except.error case most likely. There are options to disable automatic lifts (I have seen that in the supplement for the do unchained paper though I do not recall the name sadly) and most likely also coercions though I don't know the name for that either from the top of my head

The way to go to make it a proper Monad lift should be something along the lines of

instance : MonadLift (Except String) IO where
  monadLift := liftIO

though I'm writing this code on mobile and am sadly not yet able to type check Lean code in my head so there might be slight mistakes here

[Chris Lovett]

thanks, unfortunately that MonadLift didn't work, the instance compiles, but doesn't get applied. How does one debug why a monadLift is not getting picked up?

[Henrik Böving]

To add to my note from earlier today the correct option is set_option autoLift false.

Since automatic lifting is exclusively focused on synthesizing an instance MonadLiftT m n (notice the T here which is for "Transitive closure of MonadLift instances" i.e. it can take multiple steps of lifting) you can in fact use the tracing of type class synthesis here

set_option trace.Meta.synthInstance true in
def mainLift : IO Unit := do
  let ret := divideRefactored 5 0 |>.run [] |>.run 0
  let final ← ret
  IO.println s!"{final}"

This will print out a whole lot more than we actually want because there is much more TC stuff going on here so we can reduce to:

set_option trace.Meta.synthInstance true in
#synth MonadLiftT (ExceptT String Id) IO

The trace is quite huge and the details are definitely quite confusing if we dont know what TC synthesis is doing internally, however in this case the solution is quite easy, we can apply a trick and name our instance:

instance myFunkyName : MonadLift (Except String) IO where
  monadLift := liftIO

and search for this name in the trace. As we will see the name does indeed appear in the trace so the type class synthesis is very much aware of it, it just cannot solve the problem with it. However it can solve a sub problem with it:

  [Meta.synthInstance.generate] instance myFunkyName

    [Meta.synthInstance.tryResolve] MonadLift ?m.1649 ?m.1650 =?= MonadLift (Except String) IO
    [Meta.synthInstance.tryResolve] success

and then ends up at the problem:

  [Meta.synthInstance.newSubgoal] MonadLiftT (ExceptT String Id) (Except String)

Which it will fail to resolve. Now while we know that ExceptT String Id is equivalent to Except String TC synthesis is not aware of this fact (otherwise it wouldn't have ended up at this goal anyways because it should have noticed it is done already). This is the case because ExceptT is not an abbrev or marked as @[reducible] so TC synthesis will not attempt to look through the definition and thus hang on this goal.

So what we want to do instead is declare the proper ExceptT instance:

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

instance myFunkyName : MonadLift (ExceptT String Id) IO where
  monadLift := liftIO

and tada:

def mainLift : IO Unit := do
  let ret := divideRefactored 5 0 |>.run [] |>.run 0
  let final ← ret
  IO.println s!"{final}"

works.

[Chris Lovett]

Hey, you got it working, very awesome. I think I originally played with using ExceptT but couldn't get it to work. Quick question about your recommendation of always using <|.run to execute a monad. Is that the right language, or is it executing the action the monad is producing? and why isn't run defines in the Monad base class? I notice most monads provide this run method, so why isn't it promoted to the interface kind of thing? or am I thinking about this the wrong way?

[Henrik Böving]

1. Its |>.run (the arrow is the other way)

2.The majority of monads are not runnable and the signature is not at all uniform.

For ReaderT run takes a context, an m a and produces an a

For StateT run takes a state, an m a and produces an (a x state)

These types and signatures are already not compatible but it gets worse. We do not want to "run" IO in the sense that we desire to unwrap values from it fully since this defeats the point of IO. There is also no way to unwrap values from the Option or List monad since they might be empty etc. (Without providing a default that is)

So while a few monads do have some notion of "running" them this notion is

1. Not uniform across monads

2. Non existing in many of them

The reason it appears to you as if many monads support this idea is because the majority of monads that we have in Lean right now (speaking of the ones in the compiler and meta stack) are ones that are based on reader and state stacks so naturally a run operation arises for them because the respective parts of the stack have one.

[Henrik Böving]

And regarding the run terminology I'd say that it executes the monadic action by giving some additional input such as initial state, context etc. In general I don't really say that monads produce an action if I have something of type m a I'd say its a monadic action or value that you can operate on. But opinions on precise terminology might differ.

[Mario Carneiro]

I would say that almost all monads have a "run" operation, because this basically means "unfold the definition of the monad and deliver the results in terms of more primitive notions". For ReaderT, that means unfolding the fact that ReaderT R m A is defined to be R -> m A so you can apply it to R to get an element of m A. For Option there isn't anything to unfold because it's not wrapping anything, but back when we had OptionM, OptionM.run would have the type OptionM A -> Option A. So Option.run doesn't exist only because it's the identity function (but morally we think of it as translating from Option-the-monad to Option-the-inductive-type).

Even IO has a "run" operation, that would give you the exceptions in terms of BaseIO. And BaseIO.run would allow you to apply the monad value to a RealWorld token.

[Chris Lovett]

Here's a fun one, playing with your proof :

example : divideWithArgs x y = divideWithArgsDo x y := by
  simp[divideWithArgs, divideWithArgsDo]    -- Goals accomplished 🎉

I modified to this divideWithArgsDo:

def divideWithArgsDo (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float := do
  modify fun s => s + 1
  let s ← get
  let args ← read
  if (s > 10 && args.contains "--limit") then
    throw "too many divides"
  else if y == 0 then
    throw "can't divide by zero"
  else
    pure (x / y)

and then refactored it into this smaller function:

def divide (x: Float ) (y: Float): ExceptT String Id Float :=
  if y == 0 then
    throw "can't divide by zero"
  else
    pure (x / y)

so I could write:

def divideRefactored (x:Float) (y:Float) : ReaderT (List String) (StateT Nat (ExceptT String Id)) Float := do
  modify fun s => s + 1
  let s ← get
  let args ← read
  if (s > 10 && args.contains "--limit") then
    throw "too many divides"
  else
    divide x y

But now these are no longer equivalent:

example : divideWithArgs x y = divideRefactored x y := by
  simp[divideWithArgs, divideRefactored]

fails, looks like the prover refuses to look inside my divide function? It stops with liftM (divide x y) ? Is there a way to get it to try?

[Mario Carneiro]

The two aren't equivalent. Here's a partial proof:

example : divideWithArgs x y = divideRefactored x y := by
  by_cases h : y == 0 <;>
    simp [divideWithArgs, divideRefactored, divide, h]
  · sorry
  · rfl

[Mario Carneiro]

the state at the sorry is:

⊢ throw "can't divide by zero" = do
  modify fun s => s + 1
  let s ← get
  let args ← read
  if s > 10 ∧ List.contains args "--limit" = true then throw "too many divides"
    else liftM (throw "can't divide by zero")

So we would have to show that the thing on the right always evaluates to throw "can't divide by zero". But this is false, since if s > 10 and you have a limit arg then you get throw "too many divides" instead

[Chris Lovett]

I've incorporated most of these comments and awesome additional information into my new sample, CR comments are welcome:
https://github.com/leanprover/lean4-samples/pull/6
See the readme

[Mario Carneiro]

Ironically, I also can't prove that they are not equal, because y == 0 is an opaque Float equality test and for all lean knows it's always false

[Mario Carneiro]

these equality proofs are not really something you can do in haskell, or at least, not beyond handwavy arguments about referential transparency

[Mario Carneiro]

I wouldn't say that lean is really optimized for doing proofs about do notation functions. It's possible, but it's not a major focus

[Mario Carneiro]

actually here's a proof anyway, modulo a little cheat to prove y == 0 is not always false:

example : ¬ ∀ x y, divideWithArgs x y = divideRefactored x y := by
  have ⟨y, h⟩ : ∃ y : Float, y == 0 := ⟨0, by native_decide⟩
  intro H
  have := congrFun (congrFun (H 0 y) ["--limit"]) 10
  simp [divideWithArgs, divideRefactored, h] at this
  injection this with h
  revert h; decide

[Eric Wieser]

Henrik Böving said:

The way to go to make it a proper Monad lift should be something along the lines of

instance : MonadLift (Except String) IO where
  monadLift := liftIO

Does something like this now exist? What's the preferred way to run an Except monad inside IO?

[Kyle Miller]

I think it's docs#IO.ofExcept