13.10. 类型标注🔗

类型标注显式地以类型标注项。它们是向 Lean 提供项的预期类型的一种方式。该类型必须与根据项的上下文所预期的类型定义相等。类型标注不仅能用于记录程序，还可用于：

程序文本中可能没有足够的信息来推导某项的类型。标注是提供该类型的一种方式。
推断出的类型可能不是该项所需的类型。
项的预期类型用于驱动强制转换的插入，而标注是控制强制转换插入位置的一种方式。

语法后缀类型标注

类型标注必须由圆括号包围。它们表示第一个项的类型是第二个项。

term ::= ...
    | ([anonymous]term : term)

如果需要类型标注的项很长，例如策略证明或 Lean.Parser.Term.do : termdo 块，那么带有强制圆括号的后缀类型标注可能难以阅读。此外，无论是证明还是 Lean.Parser.Term.do : termdo 块，项的类型对其解释都至关重要。在这些情况下，前缀形式可能更易阅读。

语法前缀类型标注

term ::= ...
    | show term from term

当 Lean.Parser.Term.show : termshow 主体中的项是策略证明时，可以省略关键字 Lean.Parser.Term.show : termfrom。

term ::= ...
    | show term by tacticSeq

为证明标注命题

此示例无法执行策略证明，因为所需的命题未知。在运行前面的策略时，该命题会自动精化为策略能够证明的命题。然而，它们的默认分支错误地补全了该命题，导致证明失败。

example (n : Nat) := byn:Nat⊢ ?m.2 n
  induction nzero⊢ ?m.2 0succn✝:Nata✝:?m.2 n✝⊢ ?m.2 (n✝ + 1)
  next =>⊢ ?m.2 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:0 ≍ n'⊢ 0 ≍ n' + 1
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rewrite [Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'ihn':Natih:0 ≍ n'⊢ 0 ≍ n'.succ]n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rfl

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'

可以使用带 Lean.Parser.Term.show : termshow 的前缀类型标注来提供待证明的命题。在不方便把它添加为局部定义的语法上下文中，这很有用。

example (n : Nat) := show 0 + n = n byAll goals completed! 🐙
  induction nzero⊢ 0 + 0 = 0succn✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
  next =>⊢ 0 + 0 = 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:Nat.add 0 n' = n'⊢ (Nat.add 0 n').succ = n'.succ
    rewrite [ihn':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ]n':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ
    rflAll goals completed! 🐙

在线查看 ↪

为 Lean.Parser.Term.do : termdo 块标注类型

此示例缺少足够的类型信息来合成 Pure 实例。

example := do
  typeclass instance problem is stuck
  Pure ?m.8

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.return 5

typeclass instance problem is stuck
  Pure ?m.8

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

带 Lean.Parser.Term.show : termshow 的前缀类型标注与空洞结合，可以用来指出单子。默认的 OfNat _ 5 实例提供了足够的类型信息，可用 Nat 填充空洞。

example := show StateM String _ from do
  return 5

在线查看 ↪

后缀类型标注与 Lean.Parser.Term.show : termshow 之间有一项重要区别。普通后缀类型标注会改变项的预期类型，从而可能改变项的精译方式。然而，精译之后，Lean 会推断所得项的类型，并将该推断类型用于后续精译任务。另一方面，Lean.Parser.Term.show : termshow 会精译为一个推断类型就是所标注类型的项。使用广义字段表示法时可以观察到这一区别：只有使用 Lean.Parser.Term.show : termshow，才能保证以所标注类型解析字段。

后缀标注与 show

此定义为 List String 建立了一个别名：

def Colors := List String

后缀类型标注提供了确定 List.nil 的隐式实参 String 所需的类型信息，但所得类型仍然是 List String：

[] : List String#check ([] : Colors)

[] : List String

另一方面，使用 Lean.Parser.Term.show : termshow 时，精译后的项会以一种使其推断类型为 Colors 的方式构造：

have this := [];
this : Colors#check (show Colors from [])

have this := [];
this : Colors

此函数设计为通过广义字段表示法调用：

def Colors.hasYellow (cs : Colors) : Bool :=
  cs.any (·.toLower == "yellow")

由于推断类型不同，它可以与 Lean.Parser.Term.show : termshow 一起使用，却不能与后缀类型标注一起使用：

#eval ([] : Colors).Invalid field `hasYellow`: The environment does not contain `List.hasYellow`, so it is not possible to project the field `hasYellow` from an expression
  []
of type `List String`hasYellow

Invalid field `hasYellow`: The environment does not contain `List.hasYellow`, so it is not possible to project the field `hasYellow` from an expression
  []
of type `List String`

false#eval (show Colors from []).hasYellow

false