The most important thing to understand as a programmer learning Lean is how evaluation works. Evaluation is the process of finding the value of an expression, just as one does in arithmetic. For instance, the value of 15 - 6 is 9 and the value of 2 × (3 + 1) is 8. To find the value of the latter expression, 3 + 1 is first replaced by 4, yielding 2 × 4, which itself can be reduced to 8. Sometimes, mathematical expressions contain variables: the value of x + 1 cannot be computed until we know what the value of x is. In Lean, programs are first and foremost expressions, and the primary way to think about computation is as evaluating expressions to find their values.
Most programming languages are imperative, where a program consists of a series of statements that should be carried out in order to find the program's result. Programs have access to mutable memory, so the value referred to by a variable can change over time. In addition to mutable state, programs may have other side effects, such as deleting files, making outgoing network connections, throwing or catching exceptions, and reading data from a database. "Side effects" is essentially a catch-all term for describing things that may happen in a program that don't follow the model of evaluating mathematical expressions.
In Lean, however, programs work the same way as mathematical
expressions. Once given a value, variables cannot be reassigned. Evaluating an expression cannot have side effects. If two
expressions have the same value, then replacing one with the other
will not cause the program to compute a different result. This does
not mean that Lean cannot be used to write
Hello, world! to the
console, but performing I/O is not a core part of the experience of
using Lean in the same way. Thus, this chapter focuses on how to
evaluate expressions interactively with Lean, while the next chapter
describes how to write, compile, and run the
Hello, world! program.
To ask Lean to evaluate an expression, write
#eval before it in your
editor, which will then report the result back. Typically, the result
is found by putting the cursor or mouse pointer over
#eval 1 + 2
yields the value
Lean obeys the ordinary rules of precedence and associativity for arithmetic operators. That is,
#eval 1 + 2 * 5
yields the value
11 rather than
While both ordinary mathematical notation and the majority of
programming languages use parentheses (e.g.
f(x)) to apply a function to its
arguments, Lean simply writes the function next to its
f x). Function application is one of the most common operations,
so it pays to keep it concise. Rather than writing
#eval String.append("Hello, ", "Lean!")
one would instead write
#eval String.append "Hello, " "Lean!"
where the function's two arguments are simply written next to it with spaces.
Just as the order-of-operations rules for arithmetic demand
parentheses in the expression
(1 + 2) * 5, parentheses are also
necessary when a function's argument is to be computed via another
function call. For instance, parentheses are required in
#eval String.append "great " (String.append "oak " "tree")
because otherwise the second
String.append would be interpreted as
an argument to the first, rather than as a function being passed
"oak " and
"tree" as arguments. The value of the inner
call must be found first, after which it can be appended to
yielding the final value
"great oak tree".
Imperative languages often have two kinds of conditional: a
conditional statement that determines which instructions to carry
out based on a Boolean value, and a conditional expression that
determines which of two expressions to evaluate based on a Boolean
value. For instance, in C and C++, the conditional statement is
else, while the conditional expression is
written with a ternary operator
:. In Python, the
conditional statement begins with
if, while the conditional
if in the middle.
Because Lean is an expression-oriented functional language, there are no conditional statements, only conditional expressions.
They are written using
String.append "it is " (if 1 > 2 then "yes" else "no")
String.append "it is " (if false then "yes" else "no")
which evaluates to
String.append "it is " "no"
which finally evaluates to
"it is no".
For the sake of brevity, a series of evaluation steps like this will sometimes be written with arrows between them:
String.append "it is " (if 1 > 2 then "yes" else "no") ===> String.append "it is " (if false then "yes" else "no") ===> String.append "it is " "no" ===> "it is no"
Messages You May Meet
Asking Lean to evaluate a function application that is missing an argument will lead to an error message. In particular, the example
#eval String.append "it is "
yields a quite long error message:
expression String.append "it is " has type String → String but instance Lean.MetaEval (String → String) failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
This message occurs because Lean functions that are applied to only some of their arguments return new functions that are waiting for the rest of the arguments. Lean cannot display functions to users, and thus returns an error when asked to do so.
What are the values of the following expressions? Work them out by hand, then enter them into Lean to check your work.
42 + 19
String.append "A" (String.append "B" "C")
String.append (String.append "A" "B") "C"
if 3 == 3 then 5 else 7
if 3 == 4 then "equal" else "not equal"