11.1. 强制转换插入🔗

从一种类型搜索到另一种类型的强制转换这一过程称为强制转换插入。在以下原本会发生错误的情形中，会尝试进行强制转换插入：

项的期望类型不等于为该项找到的类型。
期望得到类型或命题，但该项的类型不是宇宙。
某项像函数一样被应用，但其类型不是函数类型。

显式请求强制转换时，也会插入强制转换。强制转换可能插入的每种情形都有对应的前缀运算符，用来触发相应的插入。

由于强制转换会自动插入，嵌套的类型标注提供了一种精确控制强制转换所涉及类型的方法。如果 α 与 β 不是同一类型，((e : α) : β) 会先令 e 具有类型 α，再插入从 α 到 β 的强制转换。

发现强制转换后，用于找到它的实例会被展开，并从结果项中移除。在可能的范围内，最终项中不会出现对 Coe.coe 及相关函数的调用。这一展开过程使项更易读。更重要的是，这意味着强制转换可以将被转换的项包装在函数中，从而控制其求值。

用强制转换控制求值

结构体 Later 表示一个可在将来通过调用其所含函数来求值的项。

structure Later (α : Type u) where
  get : Unit → α

从任意值到延迟值的强制转换，是通过创建函数将其包装起来实现的。

instance : CoeTail α (Later α) where
  coe x := { get := fun () => x }

然而，如果强制转换插入产生的是对 CoeTail.coe 的应用，那么该强制转换在运行时不会产生预期效果，因为被转换的值会先求值，再保存在函数的闭包中。不过，由于强制转换的实现会被展开，这个实例仍然有用。

def tomorrow : Later String :=
  (Nat.fold 10000
    (init := "")
    (fun _ _ s => s ++ "tomorrow") : String)

打印所得定义可以看到，计算位于函数体内：

def tomorrow : Later String :=
{ get := fun x => Nat.fold 10000 (fun x x_1 s => s ++ "tomorrow") "" }#print tomorrow

def tomorrow : Later String :=
{ get := fun x => Nat.fold 10000 (fun x x_1 s => s ++ "tomorrow") "" }

在线查看 ↪

强制转换中的重复求值

由于 Coe 实例的内容会在强制转换插入期间展开，多次使用其实参的强制转换应当谨慎确保只进行一次求值。为此，可以使用不属于该实例的辅助函数，也可以使用 Lean.Parser.Term.let : termlet 对被转换的项求值，然后复用所得值。

结构体 Twice 要求两个字段具有相同的值：

structure Twice (α : Type u) where
  first : α
  second : α
  first_eq_second : first = second

定义从 α 到 Twice α 的强制转换的一种方式，是使用辅助函数 twice。 coe 属性将其标记为强制转换，使其能在证明目标和错误消息中正确显示。

@[coe]
def twice (x : α) : Twice α where
  first := x
  second := x
  first_eq_second := rfl

instance : Coe α (Twice α) := ⟨twice⟩

展开 Coe 实例时，对 twice 的调用会保留下来，使其实参在执行函数体之前求值。因此，所得项中只包含一次 Lean.Parser.Term.dbgTrace : termdbg_trace：

{ first := 5, second := 5, first_eq_second := _ }hello
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)

下面用它来展示效果：

hello

将辅助函数内联到 Coe 实例中，会得到一个重复 Lean.Parser.Term.dbgTrace : termdbg_trace 的项：

instance : Coe α (Twice α) where
  coe x := ⟨x, x, rfl⟩

{ first := 5, second := 5, first_eq_second := _ }hello
hello
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)

hello
hello

为求值结果引入一个中间名称，可以避免重复 Lean.Parser.Term.dbgTrace : termdbg_trace：

instance : Coe α (Twice α) where
  coe x := let y := x; ⟨y, y, rfl⟩

{ first := 5, second := 5, first_eq_second := _ }hello
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)

hello

在线查看 ↪