io fustration

Stream: lean4

[Joseph O]

how do people use io in lean?
lets say i read a file. the type is IO String, so i cant pass that into a function that takes string. how can I come across that? also getting a random item of a list is super annoying

[Arthur Paulino]

I think what you're experiencing is not exactly IO frustration, but monadic programming frustration.

If you have a : M α where M is some monad, say IO, and you're inside a do block, then you can do let a' : α ← a.

[Joseph O]

hmm. I can try

[Arthur Paulino]

Or if you have a function f : α → τ for some type τ, then you can do let t : τ := f (← a)

[Joseph O]

but in this function, i have to return an io monad

def getRandomSentence' (filename : FilePath) : Array String := do
  let fconts : String ← FS.readFile filename
  fconts.split (·='\n')

[Joseph O]

this gives an error

[Arthur Paulino]

You need to be inside IO in order to call readFile:

def getRandomSentence' (filename : FilePath) : IO (List String) := do
  let fconts : String ← FS.readFile filename
  pure $ fconts.split (·='\n')

Also, split returns a List, not an Array

[Joseph O]

Ok, but I dont want to return an IO (List String)

[Arthur Paulino]

What type do you want?

[Joseph O]

Just List String

[Arthur Paulino]

Yeah, I'm getting flashbacks of my own frustrations from two months ago

[Mauricio Collares]

https://www.cis.upenn.edu/~cis194/spring13/lectures/08-IO.html

[Jakub Kądziołka]

That is not possible, as such a value would break basically everything

[Jakub Kądziołka]

if a function needs to do IO, its return type will be wrapped in IO

[Jakub Kądziołka]

you can unwrap that with do-notation, but your other function will also have its type wrapped with IO, as it (transitively) needs to do IO

[Joseph O]

this is insane

[Joseph O]

well, sorta

[Xubai Wang]

Well, although it's a very bad practice, you can use unsafeIO.

It seems that you are using an external file to produce random sentences in Lean, so you can also read the file at compile time to ensure that it exists (see this for example).

[Joseph O]

I have no idea what you are doing there lol

[Xubai Wang]

It creates a new term include_str% which functions the same as include_str! macro in Rust (you seem to have a rust background?)

So for your case you can use:

def sentences := include_str% "<path to your file>"

def getRandomSentence : Array String := do
  sentences.splitOn '\n'

[Arthur Paulino]

Different monads can give you access to different computational resources. The IO monad gives you access to file reading and writing (and other cool things). But once you start a computation that relies on being in a certain monad, everything that depends on it will need to be in that monad too (or in a higher level monad, but don't worry about it for now)

[Arthur Paulino]

Defining the return type of a function as IO foo is how you say in Lean "this computation happens inside IO"

[Arthur Paulino]

And requiring such type is how Lean chains monadic computations

[Joseph O]

Xubai Wang said:

It creates a new term include_str% which functions the same as include_str! macro in Rust (you seem to have a rust background?)

So for your case you can use:

def sentences : String := include_str% "<path to your file>"

def getRandomSentence : Array String := do
  sentences.splitOn '\n'

I honestly don't know what include_str macro does, but it sounds like what I need

[Joseph O]

Ah yes, it is

[Mario Carneiro]

Xubai Wang said:

Well, although it's a very bad practice, you can use unsafeIO.

It's not just bad practice: keep in mind that if you use unsafeIO then the compiler will frequently miscompile your code, because it relies on the assumption that pure functions are pure

[Jakub Kądziołka]

Joseph O said:

this is insane

If you think that, you're probably misunderstanding how this approach works. It's really not that different from marking functions as pure or impure with a special keyword. Note that, outside of higher order functions, you'll never want to take IO _ as an argument.

[Joseph O]

What type of function is include_str% in lean?

[Jakub Kądziołka]

It isn't a function. It is a macro that gets expanded to the contents of a file at compile-time.

[Xubai Wang]

It expands into a string literal.

[Joseph O]

Oh that’s cool. Where can I find such other macros?

[Xubai Wang]

Unfortunately, there is no such a place, but actually it's almost everywhere, and many parts of Lean itself is implemented with it (namespace, section, etc...) Just search for builtinCommandElab in lean4 source code (and the whole Lean.Elab module).

If you want to find some other examples, this GH search may be useful https://github.com/search?q=language%3ALean+termelab&type=code.

There is also a youtube video on Lean4 metaprogramming. But it's not a comprehensive guide. You may look at some Lean 3 meta programming tutorials to get inspiration.

[Joseph O]

I would say I’m actually quite a bit familiar with the macros

[Joseph O]

But also, how did you find out about the macro?

[Joseph O]

also, @Xubai Wang image.png image.png

[Jakub Kądziołka]

looks like it's not built into Lean, check the link posted earlier

[Henrik Böving]

Joseph O said:

But also, how did you find out about the macro?

I wrote it for doc-gen4 and it was copied to xubai's project for his purposes, as explained in the github link

[Patrick Stevens]

The frustration you are experiencing is because Lean knows that "if f calls g, and g talks to the outside world, then f talks to the outside world". Many other languages do not know this, which makes their happy-paths simpler and easier to write, usually at the cost of having bizarre runtime errors when anything goes wrong. If the filesystem flakes out, for example, most languages will just throw an exception or something; Lean forces you to indicate that you know your function is vulnerable to filesystem flakiness, and propagate that knowledge to all your callers, by using the IO monad.

[Yuri de Wit]

And there are best practices on how to structure code with and without IO in that you want to try and keep IO in the "outer" shell of your application and the pure part inside it. Well, otherwise your whole app will be in IO. But I am no help here.

I think the whole assumption here is that the upside of this outweighs the difficulties.

[Henrik Böving]

For example doc-gen4 performs its analysis step inside the MetaM monad (which is quite a beefed up version of IO for meta programming) and does every little bit it of meta analysis there, then it spits out some result type and hands that over to the HTML generator which works in another much weaker monad (a Reader one) and simply presents the results of the analysis so the application has one part that can actually interact with the real world and another half that just presents the data