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.