Reading a File

Stream: lean4

[Ian Riley]

How can I read a file with IO.FS.readFile? I currently have let input ← IO.FS.readFile ⟨fname⟩ but I expected the input to be a String or a EStateM.Result and instead it's just an EStateM. The type is EStateM IO.Error IO.RealWorld String.

[Reid Barton]

I'm pretty sure the type is just IO String.

[Reid Barton]

Maybe that unfolds to something with EStateM but why are you seeing that? We can only conjecture

[Ian Riley]

Reid Barton said:

I'm pretty sure the type is just IO String.

I figured it out. You have to include IO in the return type. The function's type was String, so I had to change it to IO String.

[Ian Riley]

Now, I need to figure out how to get out of IO hell. I'm having to change the return type of every function to include IO. It seems like I either have to exclude the IO and let a file not found go silent or I include the IO and can report the file not found, but then the next function up has to handle the case where EStateM.Result.error occurs even though that function can't report anything.

[Marc Huisinga]

Lean functions are pure, so IO bubbling up all the way to main is by design. All functions that interact with the outside world somewhere need to use IO.

[Ian Riley]

Marc Huisinga said:

Lean functions are pure, so IO bubbling up all the way to main is by design. All functions that interact with the outside world somewhere need to use IO.

Thanks. I do understand the reason for it. It seems like my best approach is to be happy with having a border between IO code and non-IO code. Everything that uses IO bubbles up to a function whose return type is Option String, so I'm just having this return none and ensuring that the other functions report.

[Marc Huisinga]

It has to bubble up all the way to main

[Reid Barton]

Ian Riley said:

but then the next function up has to handle the case where EStateM.Result.error occurs even though that function can't report anything.

You have no way to even get to the point of seeing EStateM.Result.error because you don't have an IO.RealWorld to run the IO action on.

[Ian Riley]

Reid Barton said:

Ian Riley said:

but then the next function up has to handle the case where EStateM.Result.error occurs even though that function can't report anything.

You have no way to even get to the point of seeing EStateM.Result.error because you don't have an IO.RealWorld to run the IO action on.

I learned that () counts as an IO.RealWorld.

[Reid Barton]

Uh oh!

[Ian Riley]

Last thing to figure out. How would you take IO (String × String) and turn it into IO String?

[Ian Riley]

Reid Barton said:

Uh oh!

def selectChallenge (year day : Nat) : Option (IO String) := do
  let solution := match year with
  | 2022 => Advent2022.selectDay day
  | _ => none
  match solution with
  | some result => match result () with
    | EStateM.Result.ok ⟨part1, part2⟩ _ => some (pure s!"year: {year}, day: {day} => ({part1}, {part2})")
    | EStateM.Result.error err _ => some (pure s!"{err}")
  | none => none

Note that result () is able to destructure the IO (String × String)

[Reid Barton]

I suggest you find an IO tutorial--there must be good ones for Haskell, and maybe already Lean too?

[Reid Barton]

This is pretty deeply wrong

[Reid Barton]

I suggest you stick to something like this

[Reid Barton]

def main (_args : List String) : IO UInt32 := do
  let input ← IO.FS.lines "input"
  let output := solve input
  IO.println output
  return 0

[Reid Barton]

where solve : String -> String

[Reid Barton]

or use IO.FS.readFile as appropriate

[Ian Riley]

Reid Barton said:

or use IO.FS.readFile as appropriate

I can't use IO.FS.readFile in main. My main is a CLI that takes a year and a day and directs those to a solver. The solver is responsible for knowing if a day has been solved, so it must return an Option. If the day has been solved, then it calls the solve to get the solution (String × String) because the challenges are divided into two parts. Solving a challenge requires reading an input file, so that gives us IO (String × String).

[Reid Barton]

The solver is responsible for knowing if a day has been solved, so it must return an Option... Solving a challenge requires reading an input file

Then the solver must return IO something; perhaps IO (Option something).

[Ian Riley]

Reid Barton said:

The solver is responsible for knowing if a day has been solved, so it must return an Option... Solving a challenge requires reading an input file

Then the solver must return IO something; perhaps IO (Option something).

I could probably do that. So is this because the outside IO is what's permitting Results to be captured and tossed back?

[Reid Barton]

You should never touch a Result, or unfold IO in any way

[Reid Barton]

Unfortunately, the Lean 4 core library is not yet set up in a way to prevent you from doing it

[Ian Riley]

Reid Barton said:

You should never touch a Result, or unfold IO in any way

Why not? It's done several times throughout the source code of lean4.

[Reid Barton]

Yes, but you didn't write lean 4.

[Reid Barton]

https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean#L22

[Reid Barton]

& line 25

[Ian Riley]

Reid Barton said:

Yes, but you didn't write lean 4.

I don't see what that has to do with anything. Destructuring results is a natural part of error handling. Are you saying that we should never write lean code that looks at whether a file access resulted in an ok or an err?

[Reid Barton]

What you are doing is not the way to do that

[Reid Barton]

I see there is already some explanation of IO here:
https://leanprover.github.io/functional_programming_in_lean/hello-world.html

[Ian Riley]

Reid Barton said:

What you are doing is not the way to do that

I don't disagree. The use of () as an IO.RealWorld seems like a total hack. Thanks for the link. I have read through that example. I just still have a lot of questions after, so I've been looking at the type information in InfoView and the lean4 source code to figure them out.

[Reid Barton]

Unfortunately it's not really possible to understand IO by looking at its source. It would be better to look at some programs that use it.

[Reid Barton]

And it's especially easy to go wrong given that IO is not yet opaque

[Ian Riley]

Reid Barton said:

And it's especially easy to go wrong given that IO is not yet opaque

So if something returns an IO Option String, do I not have a way to get access to Option String with a match?

[Reid Barton]

I suggest reading an IO tutorial!

[Reid Barton]

Since you said "with a match", the answer is no.

[Ian Riley]

Reid Barton said:

Since you said "with a match", the answer is no.

I figured it out. I just need to use the ← arrow and it works with match.

Thanks for the help though. I think I've got everything I needed. I think my main problem was that I was thinking of IO strictly as a Result wrapper and not something that needed to be evaluated.

[Tomas Skrivan]

One way to think about IO α is as a type RealWorld -> α where RealWorld is just some hypothetical type with one and only one element, the actual real world i.e. state of your file system, network etc.

[Mauricio Collares]

Just leaving this here: https://www.seas.upenn.edu/~cis1940/fall16/lectures/06-io-and-monads.html

[Mario Carneiro]

Tomas Skrivan said:

One way to think about IO α is as a type RealWorld -> α where RealWorld is just some hypothetical type with one and only one element, the actual real world i.e. state of your file system, network etc.

The hypothetical RealWorld type doesn't have only one element, it has an element for every possible state of the real world. Where this model breaks down is when you start treating it like a StateM and attempt to persist old values of the real world, because the computer can't do literal time travel

[Mario Carneiro]

Well this is fun...

@[noinline] def bar := @id

def foo (x : IO.Ref Nat) : Nat :=
  match (show IO Nat from x.modifyGet (fun x => (x, x+1))) () with
  | .ok n _ => n
  | .error .. => 0

#eval do
  let r ← IO.mkRef 1
  pure (foo r, foo (bar r))
-- segfaults lean

[Trebor Huang]

GHC Haskell also has this magical RealWorld type which can do limited time travelling. But of course you can't rely on the analogy too much because a computer can't (and hopefully can never) reach into your mind and delete the memory of what it just displayed.

[Trebor Huang]

I suggest adding more docs to the IO source code to prevent people getting confused over the magic? Last time I saw someone get confused about outParam which looks like it does nothing in the source code.

[David Thrane Christiansen]

@Ian Riley You may also be interested in the new chapter on monads: https://leanprover.github.io/functional_programming_in_lean/monads.html

[David Thrane Christiansen]

Tomas Skrivan said:

One way to think about IO α is as a type RealWorld -> α where RealWorld is just some hypothetical type with one and only one element, the actual real world i.e. state of your file system, network etc.

I think that a better mental model is that IO α is like RealWorld → (α × RealWorld) - that is, an IO action takes the world as input, returning a value plus a potentially-modified world. That is, it's a more like a state monad than it is like a reader monad. But it should clearly not support get and set operations - the primitives need to be structured to ensure that there's always precisely one world at any given time :-)

[Sebastian Ullrich]

Yes, world state threading is important for preserving the order of IO operations. RealWorld effectively is a linear type. There is an interesting correspondence to control edges in the sea of nodes SSA representation, for anyone who stumbled over that one before.