Additional Conveniences
Pipe Operators
Functions are normally written before their arguments. When reading a program from left to right, this promotes a view in which the function's output is paramount—the function has a goal to achieve (that is, a value to compute), and it receives arguments to support it in this process. But some programs are easier to understand in terms of an input that is successively refined to produce the output. For these situations, Lean provides a pipeline operator which is similar to the that provided by F#. Pipeline operators are useful in the same situations as Clojure's threading macros.
The pipeline E1 |> E2
is short for E2 E1
.
For example, evaluating:
#eval some 5 |> toString
results in:
"(some 5)"
While this change of emphasis can make some programs more convenient to read, pipelines really come into their own when they contain many components.
With the definition:
def times3 (n : Nat) : Nat := n * 3
the following pipeline:
#eval 5 |> times3 |> toString |> ("It is " ++ ·)
yields:
"It is 15"
More generally, a series of pipelines E1 |> E2 |> E3 |> E4
is short for nested function applications E4 (E3 (E2 E1))
.
Pipelines may also be written in reverse. In this case, they do not place the subject of data transformation first; however, in cases where many nested parentheses pose a challenge for readers, they can clarify the steps of application. The prior example could be equivalently written as:
#eval ("It is " ++ ·) <| toString <| times3 <| 5
which is short for:
#eval ("It is " ++ ·) (toString (times3 5))
Lean's method dot notation that uses the name of the type before the dot to resolve the namespace of the operator after the dot serves a similar purpose to pipelines.
Even without the pipeline operator, it is possible to write [1, 2, 3].reverse
instead of List.reverse [1, 2, 3]
.
However, the pipeline operator is also useful for dotted functions when using many of them.
([1, 2, 3].reverse.drop 1).reverse
can also be written as [1, 2, 3] |> List.reverse |> List.drop 1 |> List.reverse
.
This version avoids having to parenthesize expressions simply because they accept arguments, and it recovers the convenience of a chain of method calls in languages like Kotlin or C#.
However, it still requires the namespace to be provided by hand.
As a final convenience, Lean provides the "pipeline dot" operator, which groups functions like the pipeline but uses the name of the type to resolve namespaces.
With "pipeline dot", the example can be rewritten to [1, 2, 3] |>.reverse |>.drop 1 |>.reverse
.
Infinite Loops
Within a do
-block, the repeat
keyword introduces an infinite loop.
For example, a program that spams the string "Spam!"
can use it:
def spam : IO Unit := do
repeat IO.println "Spam!"
A repeat
loop supports break
and continue
, just like for
loops.
The dump
function from the implementation of feline
uses a recursive function to run forever:
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
This function can be greatly shortened using repeat
:
def dump (stream : IO.FS.Stream) : IO Unit := do
let stdout ← IO.getStdout
repeat do
let buf ← stream.read bufsize
if buf.isEmpty then break
stdout.write buf
Neither spam
nor dump
need to be declared as partial
because they are not themselves infinitely recursive.
Instead, repeat
makes use of a type whose ForM
instance is partial
.
Partiality does not "infect" calling functions.
While Loops
When programming with local mutability, while
loops can be a convenient alternative to repeat
with an if
-guarded break
:
def dump (stream : IO.FS.Stream) : IO Unit := do
let stdout ← IO.getStdout
let mut buf ← stream.read bufsize
while not buf.isEmpty do
stdout.write buf
buf ← stream.read bufsize
Behind the scenes, while
is just a simpler notation for repeat
.