Step By Step
A do
block can be executed one line at a time.
Start with the program from the prior section:
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
Standard IO
The first line is let stdin ← IO.getStdin
, while the remainder is:
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
To execute a let
statement that uses a ←
, start by evaluating the expression to the right of the arrow (in this case, IO.getStdIn
).
Because this expression is just a variable, its value is looked up.
The resulting value is a built-in primitive IO
action.
The next step is to execute this IO
action, resulting in a value that represents the standard input stream, which has type IO.FS.Stream
.
Standard input is then associated with the name to the left of the arrow (here stdin
) for the remainder of the do
block.
Executing the second line, let stdout ← IO.getStdout
, proceeds similarly.
First, the expression IO.getStdout
is evaluated, yielding an IO
action that will return the standard output.
Next, this action is executed, actually returning the standard output.
Finally, this value is associated with the name stdout
for the remainder of the do
block.
Asking a Question
Now that stdin
and stdout
have been found, the remainder of the block consists of a question and an answer:
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
The first statement in the block, stdout.putStrLn "How would you like to be addressed?"
, consists of an expression.
To execute an expression, it is first evaluated.
In this case, IO.FS.Stream.putStrLn
has type IO.FS.Stream → String → IO Unit
.
This means that it is a function that accepts a stream and a string, returning an IO
action.
The expression uses accessor notation for a function call.
This function is applied to two arguments: the standard output stream and a string.
The value of the expression is an IO
action that will write the string and a newline character to the output stream.
Having found this value, the next step is to execute it, which causes the string and newline to actually be written to stdout
.
Statements that consist only of expressions do not introduce any new variables.
The next statement in the block is let input ← stdin.getLine
.
IO.FS.Stream.getLine
has type IO.FS.Stream → IO String
, which means that it is a function from a stream to an IO
action that will return a string.
Once again, this is an example of accessor notation.
This IO
action is executed, and the program waits until the user has typed a complete line of input.
Assume the user writes "David
".
The resulting line ("David\n"
) is associated with input
, where the escape sequence \n
denotes the newline character.
let name := input.dropRightWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"
The next line, let name := input.dropRightWhile Char.isWhitespace
, is a let
statement.
Unlike the other let
statements in this program, it uses :=
instead of ←
.
This means that the expression will be evaluated, but the resulting value need not be an IO
action and will not be executed.
In this case, String.dropRightWhile
takes a string and a predicate over characters and returns a new string from which all the characters at the end of the string that satisfy the predicate have been removed.
For example,
#eval "Hello!!!".dropRightWhile (· == '!')
yields
"Hello"
and
#eval "Hello... ".dropRightWhile (fun c => not (c.isAlphanum))
yields
"Hello"
in which all non-alphanumeric characters have been removed from the right side of the string.
In the current line of the program, whitespace characters (including the newline) are removed from the right side of the input string, resulting in "David"
, which is associated with name
for the remainder of the block.
Greeting the User
All that remains to be executed in the do
block is a single statement:
stdout.putStrLn s!"Hello, {name}!"
The string argument to putStrLn
is constructed via string interpolation, yielding the string "Hello, David!"
.
Because this statement is an expression, it is evaluated to yield an IO
action that will print this string with a newline to standard output.
Once the expression has been evaluated, the resulting IO
action is executed, resulting in the greeting.
IO
Actions as Values
In the above description, it can be difficult to see why the distinction between evaluating expressions and executing IO
actions is necessary.
After all, each action is executed immediately after it is produced.
Why not simply carry out the effects during evaluation, as is done in other languages?
The answer is twofold.
First off, separating evaluation from execution means that programs must be explicit about which functions can have side effects.
Because the parts of the program that do not have effects are much more amenable to mathematical reasoning, whether in the heads of programmers or using Lean's facilities for formal proof, this separation can make it easier to avoid bugs.
Secondly, not all IO
actions need be executed at the time that they come into existence.
The ability to mention an action without carrying it out allows ordinary functions to be used as control structures.
For instance, the function twice
takes an IO
action as its argument, returning a new action that will execute the first one twice.
def twice (action : IO Unit) : IO Unit := do
action
action
For instance, executing
twice (IO.println "shy")
results in
shy
shy
being printed. This can be generalized to a version that runs the underlying action any number of times:
def nTimes (action : IO Unit) : Nat → IO Unit
| 0 => pure ()
| n + 1 => do
action
nTimes action n
In the base case for Nat.zero
, the result is pure ()
.
The function pure
creates an IO
action that has no side effects, but returns pure
's argument, which in this case is the constructor for Unit
.
As an action that does nothing and returns nothing interesting, pure ()
is at the same time utterly boring and very useful.
In the recursive step, a do
block is used to create an action that first executes action
and then executes the result of the recursive call.
Executing nTimes (IO.println "Hello") 3
causes the following output:
Hello
Hello
Hello
In addition to using functions as control structures, the fact that IO
actions are first-class values means that they can be saved in data structures for later execution.
For instance, the function countdown
takes a Nat
and returns a list of unexecuted IO
actions, one for each Nat
:
def countdown : Nat → List (IO Unit)
| 0 => [IO.println "Blast off!"]
| n + 1 => IO.println s!"{n + 1}" :: countdown n
This function has no side effects, and does not print anything. For example, it can be applied to an argument, and the length of the resulting list of actions can be checked:
def from5 : List (IO Unit) := countdown 5
This list contains six elements (one for each number, plus a "Blast off!"
action for zero):
#eval from5.length
6
The function runActions
takes a list of actions and constructs a single action that runs them all in order:
def runActions : List (IO Unit) → IO Unit
| [] => pure ()
| act :: actions => do
act
runActions actions
Its structure is essentially the same as that of nTimes
, except instead of having one action that is executed for each Nat.succ
, the action under each List.cons
is to be executed.
Similarly, runActions
does not itself run the actions.
It creates a new action that will run them, and that action must be placed in a position where it will be executed as a part of main
:
def main : IO Unit := runActions from5
Running this program results in the following output:
5
4
3
2
1
Blast off!
What happens when this program is run?
The first step is to evaluate main
. That occurs as follows:
main
===>
runActions from5
===>
runActions (countdown 5)
===>
runActions
[IO.println "5",
IO.println "4",
IO.println "3",
IO.println "2",
IO.println "1",
IO.println "Blast off!"]
===>
do IO.println "5"
IO.println "4"
IO.println "3"
IO.println "2"
IO.println "1"
IO.println "Blast off!"
pure ()
The resulting IO
action is a do
block.
Each step of the do
block is then executed, one at a time, yielding the expected output.
The final step, pure ()
, does not have any effects, and it is only present because the definition of runActions
needs a base case.
Exercise
Step through the execution of the following program on a piece of paper:
def main : IO Unit := do
let englishGreeting := IO.println "Hello!"
IO.println "Bonjour!"
englishGreeting
While stepping through the program's execution, identify when an expression is being evaluated and when an IO
action is being executed.
When executing an IO
action results in a side effect, write it down.
After doing this, run the program with Lean and double-check that your predictions about the side effects were correct.