11. 强制🔗

当 Lean精化器期望一种类型但生成不同类型的术语时，它会尝试自动插入 coercion，这是从术语类型到预期类型的专门指定函数。通过强制转换，可以在与需要信息量较少的类型的 API 交互时使用特定类型来表示数据。它们还允许数学发展遵循“双关语”的通常做法，其中相同的符号用于代表代数结构及其载体集，其精确含义由上下文确定。

Lean 的标准库和元编程 API 定义了许多强制。一些例子包括：

Nat 可以用在需要 Int 的地方。
Fin 可以用在需要 Nat 的地方。
α 可以用在需要 Option α 的地方。强制将值包装在 some 中。
α 可以用在需要 Thunk α 的地方。强制将项包装在函数中以延迟其求值。
当一个语法类别 c1 嵌入到另一类别 c2 中时，从 TSyntax c1 到 TSyntax c2 的强制转换将执行任何必要的包装以构造有效的语法树。

使用类型类 synthesis 发现强制转换。可以通过添加适当类型类的更多实例来扩展强制转换集。

Coercions

以下所有示例都依赖于强制：

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 表明函数应用程序的评估被延迟，直到请求 thunk 的值：

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 }

Live ↪

强制转换不用于解析通用字段表示法：仅考虑术语的推断类型。但是，type ascription 可用于触发对具有所需广义字段的类型的强制。强制转换也不用于解析 OfNat 实例：即使存在 OfNat Nat 的默认实例，从 Nat 到 α 的强制转换也不允许将自然数文字用于 α。

Coercions and Generalized Field Notation

名称 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

Live ↪

Coercions and 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)

Live ↪

大多数新的强制转换可以通过声明 Coe type class 的实例并将 coe 属性应用于执行强制转换的函数来定义。为了更好地控制强制或在更多上下文中启用它们，Lean 提供了可以实现的更多类，如本章其余部分所述。

Defining Coercions: Decimal Numbers

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

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

Live ↪

type class

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 α β is the typeclass for coercions from α to β. It can be transitively chained with other Coe instances, and coercion is automatically used when x has type α but it is used in a context where β is expected. You can use the ↑x operator to explicitly trigger coercion.

Instance Constructor

Coe.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).