Functions and Definitions

In Lean, definitions are introduced using the def keyword. For instance, to define the name hello to refer to the string "Hello", write:

def hello := "Hello"

In Lean, new names are defined using the colon-equal operator:= rather than =. This is because = is used to describe equalities between existing expressions, and using two different operators helps prevent confusion.

In the definition of hello, the expression "Hello" is simple enough that Lean is able to determine the definition's type automatically. However, most definitions are not so simple, so it will usually be necessary to add a type. This is done using a colon after the name being defined.

def lean : String := "Lean"

Now that the names have been defined, they can be used, so

#eval String.append hello (String.append " " lean)

outputs

"Hello Lean"

In Lean, defined names may only be used after their definitions.

In many languages, definitions of functions use a different syntax than definitions of other values. For instance, Python function definitions begin with the def keyword, while other definitions are defined with an equals sign. In Lean, functions are defined using the same def keyword as other values. Nonetheless, definitions such as hello introduce names that refer directly to their values, rather than to zero-argument functions that return equivalent results each time they are called.

Defining Functions

There are a variety of ways to define functions in Lean. The simplest is to place the function's arguments before the definition's type, separated by spaces. For instance, a function that adds one to its argument can be written:

def add1 (n : Nat) : Nat := n + 1

Testing this function with #eval gives 8, as expected:

#eval add1 7

Just as functions are applied to multiple arguments by writing spaces between each argument, functions that accept multiple arguments are defined with spaces between the arguments' names and types. The function maximum, whose result is equal to the greatest of its two arguments, takes two Nat arguments n and k and returns a Nat.

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

When a defined function like maximum has been provided with its arguments, the result is determined by first replacing the argument names with the provided values in the body, and then evaluating the resulting body. For example:

maximum (5 + 8) (2 * 7)
===>
maximum 13 14
===>
if 13 < 14 then 14 else 13
===>
14

Expressions that evaluate to natural numbers, integers, and strings have types that say this (Nat, Int, and String, respectively). This is also true of functions. A function that accepts a Nat and returns a Bool has type Nat → Bool, and a function that accepts two Nats and returns a Nat has type Nat → Nat → Nat.

As a special case, Lean returns a function's signature when its name is used directly with #check. Entering #check add1 yields add1 (n : Nat) : Nat. However, Lean can be "tricked" into showing the function's type by writing the function's name in parentheses, which causes the function to be treated as an ordinary expression, so #check (add1) yields add1 : Nat → Nat and #check (maximum) yields maximum : Nat → Nat → Nat. This arrow can also be written with an ASCII alternative arrow ->, so the preceding function types can be written Nat -> Nat and Nat -> Nat -> Nat, respectively.

Behind the scenes, all functions actually expect precisely one argument. Functions like maximum that seem to take more than one argument are in fact functions that take one argument and then return a new function. This new function takes the next argument, and the process continues until no more arguments are expected. This can be seen by providing one argument to a multiple-argument function: #check maximum 3 yields maximum 3 : Nat → Nat and #check String.append "Hello " yields String.append "Hello " : String → String. Using a function that returns a function to implement multiple-argument functions is called currying after the mathematician Haskell Curry. Function arrows associate to the right, which means that Nat → Nat → Nat should be parenthesized Nat → (Nat → Nat).

Exercises

• Define the function joinStringsWith with type String -> String -> String -> String that creates a new string by placing its first argument between its second and third arguments. joinStringsWith ", " "one" "and another" should evaluate to "one, and another".
• What is the type of joinStringsWith ": "? Check your answer with Lean.
• Define a function volume with type Nat → Nat → Nat → Nat that computes the volume of a rectangular prism with the given height, width, and depth.

Defining Types

Most typed programming languages have some means of defining aliases for types, such as C's typedef. In Lean, however, types are a first-class part of the language - they are expressions like any other. This means that definitions can refer to types just as well as they can refer to other values.

For instance, if String is too much to type, a shorter abbreviation Str can be defined:

def Str : Type := String

It is then possible to use Str as a definition's type instead of String:

def aStr : Str := "This is a string."

The reason this works is that types follow the same rules as the rest of Lean. Types are expressions, and in an expression, a defined name can be replaced with its definition. Because Str has been defined to mean String, the definition of aStr makes sense.

Messages You May Meet

Experimenting with using definitions for types is made more complicated by the way that Lean supports overloaded integer literals. If Nat is too short, a longer name NaturalNumber can be defined:

def NaturalNumber : Type := Nat

However, using NaturalNumber as a definition's type instead of Nat does not have the expected effect. In particular, the definition:

def thirtyEight : NaturalNumber := 38

results in the following error:

failed to synthesize instance
  OfNat NaturalNumber 38

This error occurs because Lean allows number literals to be overloaded. When it makes sense to do so, natural number literals can be used for new types, just as if those types were built in to the system. This is part of Lean's mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes. The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above.

One way to work around this limitation is by providing the type Nat on the right-hand side of the definition, causing Nat's overloading rules to be used for 38:

def thirtyEight : NaturalNumber := (38 : Nat)

The definition is still type-correct because NaturalNumber is the same type as Nat—by definition!

Another solution is to define an overloading for NaturalNumber that works equivalently to the one for Nat. This requires more advanced features of Lean, however.

Finally, defining the new name for Nat using abbrev instead of def allows overloading resolution to replace the defined name with its definition. Definitions written using abbrev are always unfolded. For instance,

abbrev N : Type := Nat

and

def thirtyNine : N := 39

are accepted without issue.

Behind the scenes, some definitions are internally marked as being unfoldable during overload resolution, while others are not. Definitions that are to be unfolded are called reducible. Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand. Definitions produced with abbrev are marked as reducible.