5.4. Function Application🔗

Ordinarily, function application is written using juxtaposition: the argument is placed after the function, with at least one space between them. In Lean's type theory, all functions take exactly one argument and produce exactly one value. All function applications combine a single function with a single argument. Multiple arguments are represented via currying.

The high-level term language treats a function together with one or more arguments as a single unit, and supports additional features such as implicit, optional, and by-name arguments along with ordinary positional arguments. The elaborator converts these to the simpler model of the core type theory.

syntax

A function application consists of a term followed by one or more arguments, or by zero or more arguments and a final ellipsis.

term ::= ...
    | term argument+
    | term argument* ..

syntaxArguments

Function arguments are either terms or named arguments.

argument ::= ...
    | term
    | ((ident  | ident ):=term)

The function's core-language type determines the placement of the arguments in the final expression. Function types include names for their expected parameters. In Lean's core language, non-dependent function types are encoded as dependent function types in which the parameter name does not occur in the body. Furthermore, they are chosen internally such that they cannot be written as the name of a named argument; this is important to prevent accidental capture.

Each parameter expected by the function has a name. Recurring over the function's argument types, arguments are selected from the sequence of arguments as follows:

If the parameter's name matches the name provided for a named argument, then that argument is selected.
If the parameter is implicit, a fresh metavariable is created with the parameter's type and selected.
If the parameter is instance implicit, a fresh instance metavariable is created with the parameter's type and inserted. Instance metavariables are scheduled for later synthesis.
If the parameter is a strict implicit parameter and there are any named or positional arguments that have not yet been selected, a fresh metavariable is created with the parameter's type and selected.
If the parameter is explicit, then the next positional argument is selected and elaborated. If there are no positional arguments:
- If the parameter is declared as an optional parameter, then its default value is selected as the argument.
- If the parameter is an automatic parameter then its associated tactic script is executed to construct the argument.
- If the parameter is neither optional nor automatic, and no ellipsis is present, then a fresh variable is selected as the argument. If there is an ellipsis, a fresh metavariable is selected as if the argument were implicit.

As a special case, when the function application occurs in a pattern and there is an ellipsis, optional and automatic arguments become universal patterns (_) instead of being inserted.

It is an error if the type is not a function type and arguments remain. After all arguments have been inserted and there is an ellipsis, then the missing arguments are all set to fresh metavariables, just as if they were implicit arguments. If any fresh variables were created for missing explicit positional arguments, the entire application is wrapped in a Lean.Parser.Term.fun : termfun term that binds them. Finally, instance synthesis is invoked and as many metavariables as possible are solved:

A type is inferred for the entire function application. This may cause some metavariables to be solved due to unification that occurs during type inference.
The instance metavariables are synthesized. Default instances are only used if the inferred type is a metavariable that is the output parameter of one of the instances.
If there is an expected type, it is unified with the inferred type; however, errors resulting from this unification are discarded. If the expected and inferred types can be equal, unification can solve leftover implicit argument metavariables. If they can't be equal, an error is not thrown because a surrounding elaborator may be able to insert coercions or monad lifts.

Named Arguments

The Lean.Parser.Command.check : command#check command can be used to inspect the arguments that were inserted for a function call.

The function sum3 takes three explicit Nat parameters, named x, y, and z.

def sum3 (x y z : Nat) : Nat := x + y + z

All three arguments can be provided positionally.

sum3 1 3 8 : Nat#check sum3 1 3 8

sum3 1 3 8 : Nat

They can also be provided by name.

sum3 1 3 8 : Nat#check sum3 (x := 1) (y := 3) (z := 8)

sum3 1 3 8 : Nat

When arguments are provided by name, it can be in any order.

sum3 1 3 8 : Nat#check sum3 (y := 3) (z := 8) (x := 1)

sum3 1 3 8 : Nat

Named and positional arguments may be freely intermixed.

sum3 1 3 8 : Nat#check sum3 1 (z := 8) (y := 3)

sum3 1 3 8 : Nat

Named and positional arguments may be freely intermixed. If an argument is provided by name, it is used, even if it occurs after a positional argument that could have been used.

sum3 8 3 1 : Nat#check sum3 1 (x := 8) (y := 3)

sum3 8 3 1 : Nat

If a named argument is to be inserted after arguments that aren't provided, a function is created in which the provided argument is filled out.

fun x y => sum3 x y 8 : Nat → Nat → Nat#check sum3 (z := 8)

fun x y => sum3 x y 8 : Nat → Nat → Nat

Behind the scenes, the names of the arguments are preserved in the function type. This means that the remaining arguments can again be passed by name.

fun x => (fun x y => sum3 x y 8) x 1 : Nat → Nat#check (sum3 (z := 8)) (y := 1)

fun x => (fun x y => sum3 x y 8) x 1 : Nat → Nat

Optional and automatic parameters are not part of Lean's core type theory. They are encoded using the optParam and autoParam gadgets.

def

optParam.{u} (α : Sort u) (default : α) : Sort u

Gadget for optional parameter support.

A binder like (x : α := default) in a declaration is syntax sugar for x : optParam α default, and triggers the elaborator to attempt to use default to supply the argument if it is not supplied.

def

autoParam.{u} (α : Sort u)
    (tactic : Lean.Syntax) : Sort u

Gadget for automatic parameter support. This is similar to the optParam gadget, but it uses the given tactic. Like optParam, this gadget only affects elaboration. For example, the tactic will not be invoked during type class resolution.

5.4.1. Generalized Field Notation

The section on structure fields describes the notation for projecting a field from a term whose type is a structure. Generalized field notation consists of a term followed by a dot (.) and an identifier, not separated by spaces.

syntaxField Notation

term ::= ...
    | The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
More precisely,
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
  where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
  `e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type,
  the above is repeated for every base type of the structure.

The field index notation `e.i`, where `i` is a positive number,
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. term.ident

If a term's type is a constant applied to zero or more arguments, then field notation can be used to apply a function to it, regardless of whether the term is a structure or type class instance that has fields. The use of field notation to apply other functions is called generalized field notation.

The identifier after the dot is looked up in the namespace of the term's type, which is the constant's name. If the type is not an application of a constant (e.g., a function, a metavariable, or a universe) then it doesn't have a namespace and generalized field notation cannot be used. If the field is not found, but the constant can be unfolded to yield a further type which is a constant or application of a constant, then the process is repeated with the new constant.

When a function is found, the term before the dot becomes an argument to the function. Specifically, it becomes the first explicit argument that would not be a type error. Aside from that, the application is elaborated as usual.

Generalized Field Notation

The type Username is a constant, so functions in the Username namespace can be applied to terms with type Username with generalized field notation.

def Username := String

One such function is Username.validate, which checks that a username contains no leading whitespace and that only a small set of acceptable characters are used. In its definition, generalized field notation is used to call the functions String.isPrefixOf, String.any, Char.isAlpha, and Char.isDigit. In the case of String.isPrefixOf, which takes two String arguments, " " is used as the first because it's the term before the dot. String.any can be called on name using generalized field notation even though it has type Username because Username.any is not defined and Username unfolds to String.

def Username.validate (name : Username) : Except String Unit := do
  if " ".isPrefixOf name then
    throw "Unexpected leading whitespace"
  if name.any notOk then
    throw "Unexpected character"
  return ()
where
  notOk (c : Char) : Bool :=
    !c.isAlpha &&
    !c.isDigit &&
    !c ∈ ['_', ' ']

def root : Username := "root"

However, Username.validate can't be called on "root" using field notation, because String does not unfold to Username.

#eval invalid field 'validate', the environment does not contain 'String.validate'
  "root"
has type
  String"root".validate

invalid field 'validate', the environment does not contain 'String.validate'
  "root"
has type
  String

root, on the other hand, has type Username:

Except.ok ()#eval root.validate

Except.ok ()

option

pp.fieldNotation

Default value: true

(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied

syntaxControlling Field Notation

The pp_nodot attribute causes Lean's pretty printer to not use field notation when printing a function.

attr ::= ...
    | pp_nodot

Turning Off Field Notation

Nat.half is printed using field notation by default.

def Nat.half : Nat → Nat
  | 0 | 1 => 0
  | n + 2 => n.half + 1

Nat.zero.half : Nat#check Nat.half Nat.zero

Nat.zero.half : Nat

Adding pp_nodot to Nat.half causes ordinary function application syntax to be used instead when displaying the term.

attribute [pp_nodot] Nat.half

Nat.half Nat.zero : Nat#check Nat.half Nat.zero

Nat.half Nat.zero : Nat

5.4.2. Pipeline Syntax

Pipeline syntax provides alternative ways to write function applications. Repeated pipelines use parsing precedence instead of nested parentheses to nest applications of functions to positional arguments.

syntaxPipelines

Right pipe notation applies the term to the right of the pipe to the one on its left.

term ::= ...
    | Haskell-like pipe operator `|>`. `x |> f` means the same as the same as `f x`,
and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
e |> e

Left pipe notation applies the term on the left of the pipe to the one on its right.

term ::= ...
    | Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`,
except that it parses `x` with lower precedence, which means that `f <| g <| x`
is interpreted as `f (g x)` rather than `(f g) x`.
e <| e

The intuition behind right pipeline notation is that the values on the left are being fed to the first function, its results are fed to the second one, and so forth. In left pipeline notation, values on the right are fed leftwards.

Right pipeline notation

Right pipelines can be used to call a series of functions on a term. For readers, they tend to emphasize the data that's being transformed.

'!'#eval "Hello!" |> String.toList |> List.reverse |> List.head!

'!'

Left pipeline notation

Left pipelines can be used to call a series of functions on a term. They tend to emphasize the functions over the data.

'!'#eval List.head! <| List.reverse <| String.toList <| "Hello!"

'!'

syntaxPipeline Fields

There is a version of pipeline notation that's used for generalized field notation.

term ::= ...
    | `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
term |>.ident

term ::= ...
    | `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
term |>.fieldIdx

e |>.f arg is an alternative syntax for (e).f arg.

Pipeline Fields

Some functions are inconvenient to use with pipelines because their argument order is not conducive. For example, Array.push takes an array as its first argument, not a Nat, leading to this error:

#eval #[1, 2, 3] |> Array.push failed to synthesize
  OfNat (Array ?m.4) 4
numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
  Array ?m.4
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.4

failed to synthesize
  OfNat (Array ?m.4) 4
numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
  Array ?m.4
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Using pipeline field notation causes the array to be inserted at the first type-correct position:

#[1, 2, 3, 4]#eval #[1, 2, 3] |>.push 4

#[1, 2, 3, 4]

This process can be iterated:

#[0, 1, 2, 3, 4]#eval #[1, 2, 3] |>.push 4 |>.reverse |>.push 0 |>.reverse

#[0, 1, 2, 3, 4]