13.4. 函数应用🔗

通常，函数应用以并置方式书写：实参放在函数之后，二者之间至少有一个空格。在 Lean 的类型论中，所有函数都恰好接受一个实参并产生一个值。每个函数应用都将一个函数与一个实参组合起来。多个实参通过柯里化表示。

高层项语言将函数及其一个或多个实参视为一个整体，除普通位置实参外，还支持隐式实参、可选实参和具名实参等附加功能。精译器会将这些转换为核心类型论中更简单的模型。

语法函数应用

函数应用由一个项后接一个或多个实参组成；也可以后接零个或多个实参，并以省略号结尾。

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

语法实参

函数实参可以是项，也可以是具名实参。

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

函数的核心语言类型决定实参在最终表达式中的位置。函数类型包含其预期参数的名称。在 Lean 的核心语言中，非依赖函数类型编码为参数名称不出现在类型体中的依赖函数类型。此外，这些名称由内部选取，无法写作具名实参的名称；这对于防止意外捕获十分重要。

函数预期的每个参数都有名称。递归遍历函数的实参类型时，按以下方式从实参序列中选择实参：

若参数名称与某个具名实参提供的名称匹配，则选择该实参。
若参数是隐式参数，则创建并选择一个具有该参数类型的新元变量。
若参数是实例隐式参数，则创建并插入一个具有该参数类型的新实例元变量。实例元变量会被安排稍后合成。
若参数是严格隐式参数，且仍有尚未选择的具名或位置实参，则创建并选择一个具有该参数类型的新元变量。
若参数是显式参数，则选择并精译下一个位置实参。若没有位置实参：
- 若参数声明为可选参数，则选择其默认值作为实参。
- 若参数是自动参数，则执行其关联的策略脚本来构造实参。
- 若参数既非可选也非自动，且没有省略号，则选择一个新变量作为实参。若有省略号，则像实参为隐式的一样选择一个新元变量。

有一种特殊情况：当函数应用出现在模式中且存在省略号时，可选实参和自动实参会变为通配模式（_），而不是被插入。

若类型不是函数类型但仍有实参剩余，则会报错。插入所有实参后，若存在省略号，则所有缺失的实参都会设为新元变量，如同它们是隐式实参一样。若为缺失的显式位置实参创建了新变量，则整个应用会包裹在绑定这些变量的 Lean.Parser.Term.fun : termfun 项中。最后调用实例合成，并尽可能求解更多元变量：

推断整个函数应用的类型。类型推断期间发生的合一可能会求解某些元变量。
合成实例元变量。仅当推断类型是某个实例的输出参数元变量时，才使用默认实例。
若存在预期类型，则将其与推断类型合一；但会丢弃此次合一产生的错误。若预期类型与推断类型可能相等，合一就能求解剩余的隐式实参元变量。若二者不可能相等，也不会抛出错误，因为外围精译器或许能插入强制转换或单子提升。

具名实参

可以使用 Lean.Parser.Command.check : command#check 命令查看为函数调用插入了哪些实参。

函数 sum3 接受三个显式的 Nat 参数，名称分别为 x、y 和 z。

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

三个实参都可以按位置提供。

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

sum3 1 3 8 : Nat

它们也可以按名称提供。

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

sum3 1 3 8 : Nat

按名称提供实参时，可以采用任意顺序。

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

sum3 1 3 8 : Nat

具名实参与位置实参可以自由混用。

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

sum3 1 3 8 : Nat

具名实参与位置实参可以自由混用。若按名称提供了实参，就会使用该实参，即使它出现在本可使用的位置实参之后。

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

sum3 8 3 1 : Nat

若要在尚未提供的实参之后插入具名实参，则会创建一个已填入所提供实参的函数。

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

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

在幕后，实参名称会保留在函数类型中。这意味着其余实参仍可再次按名称传递。

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

参数名称取自函数的类型，函数参数所用名称不必与类型中使用的名称匹配。这意味着，与参数名称冲突的局部绑定不会妨碍具名参数的使用，因为 Lean 会重命名函数参数以避免冲突，同时保持类型中的名称不变。

let x := 15;
fun x_1 y => sum3 x_1 y x : Nat → Nat → Nat#check let x := 15; sum3 (z := x)

这里，用于命名 sum3 第一个实参的 x 已被替换，以免与外围的 Parser.Term.letlet 冲突：

let x := 15;
fun x_1 y => sum3 x_1 y x : Nat → Nat → Nat

尽管 x 已被重命名，仍可按名称传递它：

(let x := 15;
  fun x_1 y => sum3 x_1 y x)
  4 : Nat → Nat#check (let x := 15; sum3 (z := x)) (x := 4)

(let x := 15;
  fun x_1 y => sum3 x_1 y x)
  4 : Nat → Nat

这是因为类型中仍使用名称 x。启用选项 pp.piBinderNames 可显示类型中的参数名称：

set_option pp.piBinderNames true in
let x := 15;
fun x_1 y => sum3 x_1 y x : (x y : Nat) → Nat#check let x := 15; sum3 (z := x)

let x := 15;
fun x_1 y => sum3 x_1 y x : (x y : Nat) → Nat

在线查看 ↪

可选参数和自动参数并非 Lean 核心类型论的一部分。它们使用 optParam 和 autoParam 辅助机制进行编码。

定义

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

用于支持可选参数的辅助类型。

声明中的绑定器 (x : α := default) 是 x : optParam α default 的语法糖；若调用处没有提供该参数，精译器会尝试使用 default 作为实参。

定义

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

用于支持自动参数的辅助类型。它与 optParam 类似，但使用给定的策略构造默认实参。与 optParam 一样，它只影响精译过程；例如，类型类合成不会运行这里给出的策略。

13.4.1. 广义字段表示法🔗

关于结构字段的小节介绍了从类型为结构的项中投影字段的表示法。广义字段表示法由一个项、一个点号（.）和一个标识符依次组成，三者之间不能有空格。

语法字段表示法

term ::= ...
    | term.ident

如果一个项的类型是应用于零个或多个参数的常量，那么无论该项是不是拥有字段的结构或类型类实例，都可以用字段表示法将一个函数应用于它。使用字段表示法应用其他函数称为广义字段表示法。

点号后的标识符会在该项类型的命名空间中查找，也就是在这个常量名称所对应的命名空间中查找。如果类型不是常量的应用（例如，它是一个元变量或宇宙），那么它就没有命名空间，因而不能使用广义字段表示法。特别地，如果表达式是函数，广义字段表示法会在 Function 命名空间中查找。因此，Nat.add.uncurry 是广义字段表示法的一种用法，它等价于 Function.uncurry Nat.add。

如果找不到该字段，但可以展开这个常量，得到另一个常量或常量应用类型，那么就用新的常量重复这一过程。

找到函数后，点号前的项会成为该函数的一个参数。具体而言，它会成为第一个不会导致类型错误的显式参数。除此之外，该应用会照常精译。

广义字段表示法

类型 Username 是常量，因此可以用广义字段表示法，将 Username 命名空间中的函数应用于类型为 Username 的项。

def Username := String

Username.validate 就是这样的函数之一，它检查用户名是否没有前导空白，且是否只使用了少量允许的字符。在其定义中，广义字段表示法用于调用函数 String.isPrefixOf、String.any、Char.isAlpha 和 Char.isDigit。 String.isPrefixOf 接受两个 String 参数；在这里，" " 用作第一个参数，因为它是点号前的项。虽然 name 的类型是 Username，但仍可用广义字段表示法对它调用 String.any，这是因为 Username.any 没有定义，而 Username 可展开为 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 adminUser : Username := "admin"

然而，不能用字段表示法对 "admin" 调用 Username.validate，因为 String 不会展开为 Username。

#eval "admin".Invalid field `validate`: The environment does not contain `String.validate`, so it is not possible to project the field `validate` from an expression
  "admin"
of type `String`validate

Invalid field `validate`: The environment does not contain `String.validate`, so it is not possible to project the field `validate` from an expression
  "admin"
of type `String`

另一方面，adminUser 的类型是 Username，因此可以用广义字段表示法调用 Username.validate 函数：

Except.ok ()#eval adminUser.validate

Except.ok ()

反过来，确实可以用广义字段表示法对 Username 值 adminUser 调用 String.any，因为类型 Username 可展开为 String。

true#eval adminUser.any (· == 'm')

true

在线查看 ↪

选项

pp.fieldNotation

默认值：true

控制美化打印时是否使用字段表示法，包括结构体投影；若声明带有 @[pp_nodot] 属性，则不使用字段表示法。

属性控制字段表示法

pp_nodot 属性使 Lean 的美化打印器在打印函数时不使用字段表示法。

attr ::= ...
    | pp_nodot

关闭字段表示法

默认情况下，Nat.half 使用字段表示法打印。

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

为 Nat.half 添加 pp_nodot 后，显示该项时会改用普通的函数应用语法。

attribute [pp_nodot] Nat.half

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

Nat.half Nat.zero : Nat

在线查看 ↪

13.4.2. 管道语法🔗

管道语法提供了函数应用的其他写法。重复使用管道时，可借助解析优先级把函数依次应用于位置参数，而不必使用嵌套括号。

语法管道

右管道表示法把管道右侧的项应用于左侧的项。

term ::= ...
    | term |> term

左管道表示法把管道左侧的项应用于右侧的项。

term ::= ...
    | term <| term

右管道表示法背后的直观理解是：左侧的值被送入第一个函数，其结果再送入第二个函数，以此类推。在左管道表示法中，右侧的值向左传递。

右管道表示法

右管道可以在一个项上依次调用一系列函数。对读者而言，它往往更强调正在变换的数据。

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

'!'

在线查看 ↪

左管道表示法

左管道可以在一个项上依次调用一系列函数。它往往更强调函数而非数据。

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

'!'

在线查看 ↪

语法管道字段

管道表示法还有一个用于广义字段表示法的版本。

term ::= ...
    | term |>.ident

term ::= ...
    | term |>.fieldIdx

e |>.f arg 是 (e).f arg 的另一种语法。

管道字段

有些函数的参数顺序不便于使用管道。例如，Array.push 的第一个参数是数组，而不是 Nat，因而会产生以下错误：

#eval #[1, 2, 3] |> Array.push failed to synthesize instance of type class
  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

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.4

failed to synthesize instance of type class
  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

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

使用管道字段表示法会把数组插入第一个类型正确的位置：

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

#[1, 2, 3, 4]

这一过程可以反复进行：

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

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

在线查看 ↪