Additional Conveniences

Nested Actions

Many of the functions in feline exhibit a repetitive pattern in which an IO action's result is given a name, and then used immediately and only once. For instance, in dump:

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

the pattern occurs for stdout:

    let stdout ← IO.getStdout
    stdout.write buf

Similarly, fileStream contains the following snippet:

  let fileExists ← filename.pathExists
  if not fileExists then

When Lean is compiling a do block, expressions that consist of a left arrow immediately under parentheses are lifted to the nearest enclosing do, and their results are bound to a unique name. This unique name replaces the origin of the expression. This means that dump can also be written as follows:

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    (← IO.getStdout).write buf
    dump stream

This version of dump avoids introducing names that are used only once, which can greatly simplify a program. IO actions that Lean lifts from a nested expression context are called nested actions.

fileStream can be simplified using the same technique:

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  if not (← filename.pathExists) then
    (← IO.getStderr).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))

In this case, the local name of handle could also have been eliminated using nested actions, but the resulting expression would have been long and complicated. Even though it's often good style to use nested actions, it can still sometimes be helpful to name intermediate results.

It is important to remember, however, that nested actions are only a shorter notation for IO actions that occur in a surrounding do block. The side effects that are involved in executing them still occur in the same order, and execution of side effects is not interspersed with the evaluation of expressions. For an example of where this might be confusing, consider the following helper definitions that return data after announcing to the world that they have been executed:

def getNumA : IO Nat := do
  (← IO.getStdout).putStrLn "A"
  pure 5

def getNumB : IO Nat := do
  (← IO.getStdout).putStrLn "B"
  pure 7

These definitions are intended to stand in for more complicated IO code that might validate user input, read a database, or open a file.

A program that prints 0 when number A is five, or number B otherwise, can be written as follows:

def test : IO Unit := do
  let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
  (← IO.getStdout).putStrLn s!"The answer is {a}"

However, this program probably has more side effects (such as prompting for user input or reading a database) than was intended. The definition of getNumA makes it clear that it will always return 5, and thus the program should not read number B. However, running the program results in the following output:

A
B
The answer is 0

getNumB was executed because test is equivalent to this definition:

def test : IO Unit := do
  let x ← getNumA
  let y ← getNumB
  let a : Nat := if x == 5 then 0 else y
  (← IO.getStdout).putStrLn s!"The answer is {a}"

This is due to the rule that nested actions are lifted to the closest enclosing do block. The branches of the if were not implicitly wrapped in do blocks because the if is not itself a statement in the do block—the statement is the let that defines a. Indeed, they could not be wrapped this way, because the type of the conditional expression is Nat, not IO Nat.

Flexible Layouts for do

In Lean, do expressions are whitespace-sensitive. Each IO action or local binding in the do is expected to start on its own line, and they should all have the same indentation. Almost all uses of do should be written this way. In some rare contexts, however, manual control over whitespace and indentation may be necessary, or it may be convenient to have multiple small actions on a single line. In these cases, newlines can be replaced with a semicolon and indentation can be replaced with curly braces.

For instance, all of the following programs are equivalent:

-- This version uses only whitespace-sensitive layout
def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let name := (← stdin.getLine).trim
  stdout.putStrLn s!"Hello, {name}!"

-- This version is as explicit as possible
def main : IO Unit := do {
  let stdin ← IO.getStdin;
  let stdout ← IO.getStdout;

  stdout.putStrLn "How would you like to be addressed?";
  let name := (← stdin.getLine).trim;
  stdout.putStrLn s!"Hello, {name}!"
}

-- This version uses a semicolon to put two actions on the same line
def main : IO Unit := do
  let stdin ← IO.getStdin; let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let name := (← stdin.getLine).trim
  stdout.putStrLn s!"Hello, {name}!"

Idiomatic Lean code uses curly braces with do very rarely.

Running IO Actions With #eval

Lean's #eval command can be used to execute IO actions, rather than just evaluating them. Normally, adding a #eval command to a Lean file causes Lean to evaluate the provided expression, convert the resulting value to a string, and provide that string as a tooltip and in the info window. Rather than failing because IO actions can't be converted to strings, #eval executes them, carrying out their side effects. If the result of execution is the Unit value (), then no result string is shown, but if it is a type that can be converted to a string, then Lean displays the resulting value.

This means that, given the prior definitions of countdown and runActions,

#eval runActions (countdown 3)

displays

3
2
1
Blast off!

This is the output produced by running the IO action, rather than some opaque representation of the action itself. In other words, for IO actions, #eval both evaluates the provided expression and executes the resulting action value.

Quickly testing IO actions with #eval can be much more convenient that compiling and running whole programs. However, there are some limitations. For instance, reading from standard input simply returns empty input. Additionally, the IO action is re-executed whenever Lean needs to update the diagnostic information that it provides to users, and this can happen at unpredictable times. An action that reads and writes files, for instance, may do so at inconvenient times.