missing `IO String` function

Stream: lean4

[Asei Inoue]

Why is it that there is IO.print, a function of type IO Unit that prints a string to the terminal, but there is no function of type IO String that receives keyboard input characters?

[Asei Inoue]

As far as I know, the only function in the standard library that accepts keyboard input is one that takes FS.Stream as an argument.

[Asei Inoue]

Why are the following function of type IO String not provided in the standard library? Would it be a good idea to add them?

def IO.getln : IO String := do
  let input ← (← IO.getStdin).getLine
  return input.trim

[Asei Inoue]

As for me, I would like to have such a function, because it is a hassle to prepare a Stream every time....

[Eric Wieser]

I don't think it should be calling trim

[Chris Bailey]

Rust communities pretty frequently get "why is this python code faster than this rust code" type questions from users reaching for conveniently packaged fire and forget IO functions, but under the hood end up reacquiring locks/handles needlessly or allocating a bunch of stuff that doesn't need to be allocated when they're put under a heavy work load.

I don't know how the codegen/compilation works for IO in Lean so this is totally speculative, but maybe something to think about.

[Asei Inoue]

@Eric Wieser

You're right. Indeed, I shouldn't call trim. How about this?

/-- Accepts a string input from the keyboard, removing newline characters. -/
def IO.getInput : IO String := do
  let mut input ← (← IO.getStdin).getLine
  input := input.replace "\n" "" |>.replace "\r" ""
  return input

/-- Accepts a string input from the keyboard, including the trailing newline as-is. -/
def IO.getInputln : IO String := do
  let input ← (← IO.getStdin).getLine
  return input

/-  example usage -/

/-- Reads a string from the keyboard and displays its length. -/
def main : IO Unit := do
  IO.print "Enter a string: "
  let input ← IO.getInput
  IO.println s!"The entered string is '{input}'."
  IO.println s!"The string has {input.trim.length} characters."

[Eric Wieser]

If nothing else I would at least avoid duplication there

/-- Accepts a string input from the keyboard, including the trailing newline as-is. -/
def IO.getInputln : IO String := return (← IO.getStdin).getLine

/-- Accepts a string input from the keyboard, removing newline characters. -/
def IO.getInput : IO String := return (← IO.getInputln).replace "\n" "" |>.replace "\r" ""

but I think you need to be careful about the line-stripping logic; on Linux, I don't think stripping \r is expected behavior

[Asei Inoue]

@Eric Wieser

You are right. how about this?

/-- Accepts a string input from the keyboard, removing newline characters. -/
def IO.getInput : IO String := do
  let input ← (← IO.getStdin).getLine
  return removeBr input
where
  removeBr : String → String :=
    if System.Platform.isWindows then
      (String.replace · "\r" "") ∘ (String.replace · "\n" "")
    else
      (String.replace · "\n" "")

/-- Accepts a string input from the keyboard, including the trailing newline as-is. -/
def IO.getInputln : IO String := do
  (← IO.getStdin).getLine

[Eric Wieser]

You should write those in the other order so that one can use the other

[Eric Wieser]

I still think that trying to emulate python's "universal newlines" feature is a bad idea without a larger design for how it is expected to work

[Asei Inoue]

@Eric Wieser

how about this?

/-- Accepts a string input from the keyboard, including the trailing newline as-is. -/
def IO.getInputln : IO String := do
  (← IO.getStdin).getLine

/-- Accepts a string input from the keyboard, removing newline characters. -/
def IO.getInput : IO String := do
  return removeBr (← getInputln)
where
  removeBr : String → String :=
    if System.Platform.isWindows then
      (String.replace · "\r" "") ∘ (String.replace · "\n" "")
    else
      (String.replace · "\n" "")

[Asei Inoue]

What exactly do you mean by "larger design for how it is expected to work"?

[Eric Wieser]

I mean questions like:

• What if I want to read a text file with windows newlines? Should getLine do the right thing for me?
• What if I read the whole file / stdin at once; should I see \r\n or just \n?|
• Should the user be able to opt in / out, in case they're reading a windows file on linux?

[Asei Inoue]

The file was not supposed to be read. I assumed only keyboard input from the user.

[Eric Wieser]

I can always write cat some_file.txt | lake exe your_program though

[Asei Inoue]

Perhaps only the line breaks at the end should be removed. hmm. I understand the problem, but I don't know how to solve it.

[Asei Inoue]

@Eric Wieser

How about just adding this function only?

def IO.getInputln : IO String := do
  (← IO.getStdin).getLine

[Eric Wieser]

For what it's worth, Rust does not have such a function

[Asei Inoue]

Interesting. Why is there no such function in Rust?

[François G. Dorais]

String.replace will scan the entire string but in this case it is known exactly where the final newline is.

[François G. Dorais]

FWIW, it's better to just let the user deal with newlines.

[Eric Wieser]

I think python's TextIOWrapper that wraps a stream object and tidies newlines is a nice way to design the feature

[François G. Dorais]

I've used that idea in UnicodeBasic: https://github.com/fgdorais/lean4-unicode-basic/blob/main/UnicodeBasic/CharacterDatabase.lean

The line parsing version is simpler since it doesn't have to delete comments and split into fields.

[Asei Inoue]

hmm... request for IO.getInputln is not accepted?

[François G. Dorais]

How about implementing something more generic like this:

def ByLine (σ) [Stream σ Char] : Type _ := ...

instance [Stream σ Char] : Stream (ByLine σ) String := ...