Error translating FPIL IO example from do to bind

Stream: new members

[mars0i]

I'm at a stage (with Lean, Haskell, Idris, etc.) where I find it helpful to translate do blocks into code that uses only >>=. I want to see what the do code reduces to. FPIL section 2.4 includes this example:

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

This type checks with my configuration, as expected, but my translation of it doesn't:

def myFileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) :=
  filename.pathExists >=
  λ fileExists => if not fileExists then
                    IO.getStderr >>=
                    λ stderr => stderr.putStrLn s!"File not found: {filename}"
                  else
                    IO.FS.Handle.mk filename IO.FS.Mode.read >>=
                    λ handle => pure (some (IO.FS.Stream.ofHandle handle))

There are two errors. On stderr.putStrLn s!"File not found: {filename}":

▶ 62:33-62:79: error:
type mismatch
  IO.FS.Stream.putStrLn stderr (toString "File not found: " ++ toString filename ++ toString "")
has type
  IO Unit : Type
but is expected to have type
  BaseIO ?m.1830 : Type

On IO.FS.Handle.mk filename IO.FS.Mode.read:

▶ 64:21-64:61: error:
application type mismatch
  bind (IO.FS.Handle.mk filename IO.FS.Mode.read)
argument
  IO.FS.Handle.mk filename IO.FS.Mode.read
has type
  IO IO.FS.Handle : Type
but is expected to have type
  BaseIO ?m.2145 : Type

It seems relevant that in the original FPIL version with do, the types of IO.getStderr and IO.FS.Handle.mk are preceded by "IO" and a space. In my version, the types of the same functions are preceded by "BaseIO" and a space. Is therew some special Lean do magic going on here, or am I making a silly mistake (not unlikely)?

I'm not sure what a keyword + space before a type means, but it seems as if without do, BaseIO is needed, but with do, IO is needed.

(Feel free to answer by pointing me to an online text or another thread! I tried searching here without success--not sure what search string to use.)

[Timo Carlin-Burns]

This might not be the problem, but why did the pure none disappear in your translation?

[Yaël Dillies]

Do you know you can #print fileStream to see what the do block reduces to?

[mars0i]

Yeah, just noticed the missing pure none. Hold on ....

[mars0i]

With pure none the first error changes, but seems similar.

def myFileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) :=
  filename.pathExists >=
  λ fileExists => if not fileExists then
                    IO.getStderr >>=
                    λ stderr => stderr.putStrLn s!"File not found: {filename}" >>=
                    λ _ => pure none
                  else
                    IO.FS.Handle.mk filename IO.FS.Mode.read >>=
                    λ handle => pure (some (IO.FS.Stream.ofHandle handle))

Here's the new error:

▶ 62:33-62:79: error:
application type mismatch
  bind (IO.FS.Stream.putStrLn stderr (toString "File not found: " ++ toString filename ++ toString ""))
argument
  IO.FS.Stream.putStrLn stderr (toString "File not found: " ++ toString filename ++ toString "")
has type
  IO Unit : Type
but is expected to have type
  BaseIO ?m.1867 : Type

[mars0i]

@Yaël Dillies , no! Didn't know.

[mars0i]

There are added liftMs:

▶ 57:1-57:7: information:
def fileStream : System.FilePath → IO (Option IO.FS.Stream) :=
fun filename => do
  let fileExists ← liftM (System.FilePath.pathExists filename)
  if (!fileExists) = true then do
      let stderr ← liftM IO.getStderr
      IO.FS.Stream.putStrLn stderr (toString "File not found: " ++ toString filename ++ toString "")
      pure none
    else do
      let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
      pure (some (IO.FS.Stream.ofHandle handle))

which converts from one monad to another (as I would put it) according to liftM's documentation. But still, not sure I understand what's going on.

[Timo Carlin-Burns]

BaseIO is another monad which is like IO without exceptions. Maybe one of the API functions returns a value in BaseIO and the do notation was automatically inserting coercions using MonadLift?

[mars0i]

That sounds reasonable @Timo Carlin-Burns. Thanks. I'll look at it more later, then. (I might not like it. I know I'm in a minority, but in Haskell, I think do hides what is really happening from novices. I was very confused by do at first. As I said, it's a minority perspective. But packing more syntactic sugar into do means it's harder to understand what it's doing. Oh well. Realistic, flexible IO is always going to be somewhat messy.)

[mars0i]

I'm trying to fix my do-less function by using what I am finding using #print on the original FPIL do-based definition. This is making me hate Lean's do. It causes what appears to be the same function appear to have different types when surrounded by do from the type it appears to have outside of do. How is that a good thing? It inserts additional calls in ways that I can't figure out how to reproduce in my code. Granted, I'm a beginner, but I'm looking at the #print output and I can't figure out what it is doing. It's easy to translate Haskell's do into what it is syntactic sugar for, but it's not easy to do that with Lean's do. So what it is actually doing becomes confusing and mysterious. If it works, great, but if it ever doesn't, it may be difficult to diagnose. Functional programming is supposed to free us from side-effects that are not apparently on the face of the code. Lean's do is doing something analogous to producing non-apparent side-effects, by rewriting code in ways that are not obvious. Saying this won't change anything.

[Mauricio Collares]

Did you take a look at https://lean-lang.org/papers/do.pdf?

[mars0i]

No, didn't know about that. Thanks @Mauricio Collares . I'll look at it.

[mars0i]

I apologize for being so rant-ey in my earlier post. I do appreciate the link to the article that Maurcio provided.

(I've skimmed the PDF, and feel it's not obvious that it clarifies what bothered me, but also that it wouldn't be worth my trouble at this stage to try to figure out whether the answer is there. It's OK. I can use do in the ways suggested in teaching materials without trying to understand it. I didn't decide to learn Lean for the sake of do. :smile: )

[mars0i]

I will say that copying do boilerplate for the sake of building up intuitive pattern intuitions is going to have to be part of my strategy with do. That's OK. (do's semantics in Haskell weren't clear to me until I learned how to translate away do. I know many people think that do is easy to understand because "it's just like imperative languages", but I never felt that way, despite having more experience with imperative than functional languages--like most people. Everyone's different.)

[mars0i]

And it is good that I went through this experience with Lean's do.

[Henrik Böving]

mars0i said:

I apologize for being so rant-ey in my earlier post. I do appreciate the link to the article that Maurcio provided.

(I've skimmed the PDF, and feel it's not obvious that it clarifies what bothered me, but also that it wouldn't be worth my trouble at this stage to try to figure out whether the answer is there. It's OK. I can use do in the ways suggested in teaching materials without trying to understand it. I didn't decide to learn Lean for the sake of do. :smile: )

The point of the automated insertion of functions (namely the only automated insertion that is happening is lifting of monads) is that you don't want users to think about it. For example when I am doing meta programming I'm in MetaM which is a StateT + ReaderT + CoreM. When I call a function that operates just in CoreM I don't want to have to think about why I'm suddenly getting a type error and that I have to remember inserting a liftM. It should just work as its obvious that I can do this.

[Henrik Böving]

mars0i said:

That sounds reasonable Timo Carlin-Burns. Thanks. I'll look at it more later, then. (I might not like it. I know I'm in a minority, but in Haskell, I think do hides what is really happening from novices. I was very confused by do at first. As I said, it's a minority perspective. But packing more syntactic sugar into do means it's harder to understand what it's doing. Oh well. Realistic, flexible IO is always going to be somewhat messy.)

I also think that its fine for do to hide what's going on. With the <- arrow you do not need to know at all that it is about some bind operation that is defined in some funky way. Instead the mental model of <- can just be "this performs some additional thing specific to the monad" In IO thats running an IO action, in State that's accessing and potentially modifying the state etc. A user does not really need to know how to desugar into bind sequences in order for this to work out.

[mars0i]

Thanks @Henrik Böving. That makes sense, and it's helpful to have that context. I kind of prefer to take a different approach, but this just isn't the best situation for my preferred strategy. It won't be a big deal to go along with the standard Lean do procedure when I need IO, state, etc. I could say more about what I prefer and why, but it's not very interesting. There's no point to me going on about it.

[Patrick Massot]

Note that nobody forces you to use do.

[Kyle Miller]

set_option pp.notation false causes the pretty printer to stop using do notation (among other notations)

[mars0i]

Thanks @Kyle Miller. That's extremely useful for what I was trying to understand.