13.3. 函数🔗

可以通过由 Lean.Parser.Term.fun : termfun 关键字引入的抽象来创建函数类型的项。在不同社群中，函数抽象也称为 λ 抽象，源于 Alonzo Church 为其采用的记法；也称为匿名函数，因为不必在全局环境中用名称定义它们。核心类型论中的抽象只允许绑定单个变量，而 Lean 的高层语法中的函数项则相当灵活。

语法函数抽象

最基本的函数抽象引入一个变量来代表函数参数：

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

精译时，Lean 必须能够确定函数的定义域。类型标注是提供这一信息的一种方式：

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

用 Lean.Parser.Command.definition : commanddef 等关键字定义的函数定义会脱糖为 Lean.Parser.Term.fun : termfun。另一方面，归纳类型声明会引入具有函数类型的新值（构造器和类型构造器），它们本身无法只用 Lean.Parser.Term.fun : termfun 实现。

语法柯里化函数

Lean.Parser.Term.fun : termfun 后可接受多个参数名称：

term ::= ...
    | fun ident ident* => term

term ::= ...
    | fun ident ident* : term => term

多个参数使用不同类型标注时需要圆括号：

term ::= ...
    | fun (ident* : term) =>term

这些写法等价于书写嵌套的 Lean.Parser.Term.fun : termfun 项。

本节所述的所有语法中，Lean.Parser.Term.fun : term=> 都可以替换为 Lean.Parser.Term.fun : term↦。

函数抽象还可以在参数规格中使用模式匹配语法，从而不必引入一个随即就要解构的局部变量。此语法见模式匹配一节。

13.3.1. 隐式参数🔗

Lean 支持函数的隐式参数。这意味着 Lean 自身可以为函数提供实参，而不要求用户提供全部所需实参。隐式参数分为三类：

普通隐式参数: 普通隐式参数是应由 Lean 通过合一确定其值的函数参数。换言之，每个调用处都应恰好存在一个候选实参值，使整个函数调用良类型。每次函数出现时，Lean 精译器都会尝试为所有隐式实参寻找值。普通隐式参数写在花括号（{ 和 }）中。
严格隐式参数: 严格隐式参数与普通隐式参数相同，区别在于只有调用处提供了后续显式实参时，Lean 才会尝试寻找实参值。严格隐式参数写在双花括号（⦃ 和 ⦄，或 {{ 和 }}）中。
实例隐式参数: 实例隐式参数的实参通过类型类合成查找。实例隐式参数写在方括号（[ 和 ]）中。与其他种类的隐式参数不同，不带 : 书写的实例隐式参数指定的是参数类型，而不是提供名称。此外，只允许一个名称。大多数实例隐式参数会省略参数名称，因为作为函数参数合成的实例即使没有显式命名，也已经可以在函数体中使用。

普通隐式参数与严格隐式参数

函数 f 与 g 的区别在于，α 在 f 中是严格隐式的：

def f ⦃α : Type⦄ : α → α := fun x => x
def g {α : Type} : α → α := fun x => x

应用于具体实参时，这两个函数的精译结果相同：

example : f 2 = g 2 := rfl

然而，未提供显式实参时，使用 f 不要求求解隐式的 α：

example := f

但使用 g 的确要求求解它；若可用信息不足，精译就会失败：

Failed to infer type of exampleexample := don't know how to synthesize implicit argument `α`
  @g ?m.3
context:
⊢ Typeg

don't know how to synthesize implicit argument `α`
  @g ?m.3
context:
⊢ Type

在线查看 ↪

语法带不同绑定器的函数

Lean.Parser.Term.fun : termfun 最一般的语法接受一系列绑定器：

term ::= ...
    | fun funBinder funBinder* => term

语法函数绑定器

函数绑定器可以是标识符：

funBinder ::= ...
    | ident

带圆括号的标识符序列：

funBinder ::= ...
    | ([anonymous]ident ident*)

带类型标注的标识符序列：

funBinder ::= ...
    | ([anonymous]ident ident* : term)

带或不带类型标注的隐式参数：

funBinder ::= ...
    | {ident ident*}

funBinder ::= ...
    | {ident ident* : term}

匿名或具名的实例隐式参数：

funBinder ::= ...
    | [term]

funBinder ::= ...
    | [ident : term]

或者带或不带类型标注的严格隐式参数：

funBinder ::= ...
    | ⦃ident ident*⦄

funBinder ::= ...
    | ⦃ident* : term⦄

与往常一样，可以用 _ 代替标识符来创建匿名参数；⦃ 和 ⦄ 也可分别写成 {{ 和 }}。

Lean 的核心语言不区分隐式参数、实例参数和显式参数：各种函数及函数类型在定义上相等。这些区别只能在精译过程中观察到。

若函数的预期类型包含隐式参数，而其绑定器不包含，则所得函数最终的参数可能比代码中的绑定器所指明的更多。这是因为隐式参数会自动添加。

来自类型的隐式参数

恒等函数可以只用一个显式参数书写。只要其类型已知，隐式类型参数就会自动添加。

fun {α} x => x : {α : Type} → α → α#check (fun x => x : {α : Type} → α → α)

fun {α} x => x : {α : Type} → α → α

以下写法全都等价：

fun {α} x => x : {α : Type} → α → α#check (fun {α} x => x : {α : Type} → α → α)

fun {α} x => x : {α : Type} → α → α

fun {α} x => x : {α : Type} → α → α#check (fun {α} (x : α) => x : {α : Type} → α → α)

fun {α} x => x : {α : Type} → α → α

fun {α} x => x : {α : Type} → α → α#check (fun {α : Type} (x : α) => x : {α : Type} → α → α)

fun {α} x => x : {α : Type} → α → α

在线查看 ↪