11. 强制转换🔗

当 Lean 精译器期望某种类型，却产生了另一类型的项时，它会尝试自动插入强制转换。强制转换是从该项的类型到期望类型的特别指定函数。强制转换使得我们可以用具体类型表示数据，同时与那些期望信息较少类型的 API 交互。它们也让数学形式化能够沿用通常的“一符多义”惯例：同一个符号既可表示代数结构，也可表示其载体集合，确切含义由上下文决定。

Lean 的标准库和元编程 API 定义了许多强制转换。例如：

可在期望 Int 之处使用 Nat。
可在期望 Nat 之处使用 Fin。
可在期望 Option α 之处使用 α。该强制转换用 some 包装此值。
可在期望 Thunk α 之处使用 α。该强制转换将此项包装在函数中，以延迟其求值。
当语法类别 c1 嵌入另一类别 c2 时，从 TSyntax c1 到 TSyntax c2 的强制转换会执行构造有效语法树所需的包装。

强制转换通过类型类合成来查找。可以为适当的类型类添加更多实例，从而扩展强制转换集合。

强制转换

以下示例全都依赖强制转换：

example (n : Nat) : Int := n
example (n : Fin k) : Nat := n
example (x : α) : Option α := x

def th (f : Int → String) (x : Nat) : Thunk String := f x

open Lean in
example (n : Ident) : Term := n

对于 th，使用 Lean.Parser.Command.print : command#print 可以看到，函数应用的求值会延迟到请求该延迟计算的值时：

def th : (Int → String) → Nat → Thunk String :=
fun f x => { fn := fun x_1 => f ↑x }#print th

def th : (Int → String) → Nat → Thunk String :=
fun f x => { fn := fun x_1 => f ↑x }

在线查看 ↪

强制转换不会用于解析广义字段记法：此时只考虑项的推断类型。不过，可以使用类型标注触发到具有所需广义字段之类型的强制转换。强制转换也不会用于解析 OfNat 实例：即使 OfNat Nat 有默认实例，从 Nat 到 α 的强制转换也不能让自然数字面量用于 α。

强制转换与广义字段记法

名称 Nat.bdiv 未定义，但 Int.bdiv 存在。查找字段 bdiv 时，不会考虑从 Nat 到 Int 的强制转换：

example (n : Nat) := n.Invalid field `bdiv`: The environment does not contain `Nat.bdiv`, so it is not possible to project the field `bdiv` from an expression
  n
of type `Nat`bdiv 2

Invalid field `bdiv`: The environment does not contain `Nat.bdiv`, so it is not possible to project the field `bdiv` from an expression
  n
of type `Nat`

这是因为只有当期望类型与推断类型不同时才会插入强制转换，而广义字段是根据点号前项的推断类型解析的。添加类型标注可以触发强制转换；此外，它还会使整个标注项的推断类型成为 Int，从而找到函数 Int.bdiv。

example (n : Nat) := (n : Int).bdiv 2

在线查看 ↪

强制转换与 OfNat

Bin 是表示二进制数的归纳类型。

inductive Bin where
  | done
  | zero : Bin → Bin
  | one : Bin → Bin

def Bin.toString : Bin → String
  | .done => ""
  | .one b => b.toString ++ "1"
  | .zero b => b.toString ++ "0"

instance : ToString Bin where
  toString
    | .done => "0"
    | b => Bin.toString b

反复应用 Bin.succ 可以将二进制数转换为自然数：

def Bin.succ (b : Bin) : Bin :=
  match b with
  | .done => Bin.done.one
  | .zero b => .one b
  | .one b => .zero b.succ

def Bin.ofNat (n : Nat) : Bin :=
  match n with
  | 0 => .done
  | n + 1 => (Bin.ofNat n).succ

即使将 Bin.ofNat 注册为强制转换，自然数字面量也不能用于 Bin：

attribute [coe] Bin.ofNat

instance : Coe Nat Bin where
  coe := Bin.ofNat

#eval (failed to synthesize instance of type class
  OfNat Bin 9
numerals are polymorphic in Lean, but the numeral `9` cannot be used in a context where the expected type is
  Bin
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.9 : Bin)

failed to synthesize instance of type class
  OfNat Bin 9
numerals are polymorphic in Lean, but the numeral `9` cannot be used in a context where the expected type is
  Bin
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.

这是因为强制转换会在类型不匹配时插入，但无法合成 OfNat 实例并不是类型不匹配。

可以在 OfNat Bin 实例的定义中使用该强制转换：

instance : OfNat Bin n where
  ofNat := n

1010#eval (10 : Bin)

在线查看 ↪

大多数新的强制转换都可以这样定义：声明 Coe 类型类的实例，并将 coe 属性应用于执行强制转换的函数。为了更精细地控制强制转换，或使其能用于更多上下文，Lean 还提供了其他可实现的类，本章其余部分将对此加以介绍。

定义强制转换：十进制数

十进制数可以定义为数位数组。

structure Decimal where
  digits : Array (Fin 10)

添加强制转换后，它们不仅可用于期望 Nat 的上下文，也可用于期望任何 Nat 可强制转换至的类型的上下文。

@[coe]
def Decimal.toNat (d : Decimal) : Nat :=
  d.digits.foldl (init := 0) fun n d => n * 10 + d.val

instance : Coe Decimal Nat where
  coe := Decimal.toNat

下面将 Decimal 同时视为 Int 和 Nat，以展示这一点：

def twoHundredThirteen : Decimal where
  digits := #[2, 1, 3]

def one : Decimal where
  digits := #[1]

-212#eval (one : Int) - (twoHundredThirteen : Nat)

-212

在线查看 ↪

类型类

Coe.{u, v} (α : semiOutParam (Sort u)) (β : Sort v) :
  Sort (max (max 1 u) v)
Coe.{u, v} (α : semiOutParam (Sort u))
  (β : Sort v) : Sort (max (max 1 u) v)

Coe α β 是从 α 到 β 的强制转换类型类。它可以与其他 Coe 实例传递地组成转换链。当 x 的类型为 α，但它出现在预期类型为 β 的上下文中时，Lean 会自动使用该强制转换。可以使用运算符 ↑x 显式触发强制转换。

实例构造子

Coe.mk.{u, v}

方法

coe : α → β

将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。