强制转换

在数学中，用同一个符号来在不同的语境中代表数学对象的不同方面是很常见的。例如，如果在一个需要集合的语境中给出了一个环，那么理解为该环对应的集合也是很有道理的。在编程语言中，有一些规则自动地将一种类型转换为另一种类型也是很常见的。例如，Java 允许 byte 自动转换为一个 int，Kotlin 也允许非空类型在可为空的语境中使用。

在 Lean 中，这两个目的都是用一个叫做 强制转换（coercions） 的机制实现的。当 Lean 遇到了在某语境中某表达式的类型与期望类型不一致时，Lean 在报错前会尝试进行强制转换。不像 Java，C，和 Kotlin，强制转换是通过定义类型类实例实现的，并且是可扩展的。

正数

例如，每个正数都对应一个自然数。之前定义的函数 Pos.toNat 可以将一个 Pos 转换成对应的 Nat：

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

函数 List.drop，的类型是 {α : Type} → Nat → List α → List α，它将列表的前缀移除。将 List.drop 应用到 Pos 会产生一个类型错误：

[1, 2, 3, 4].drop (2 : Pos)

application type mismatch
  List.drop 2
argument
  2
has type
  Pos : Type
but is expected to have type
  Nat : Type

因为 List.drop 的作者没有让它成为一个类型类的方法，所以它没有办法通过定义新实例的方式来重写。

Coe 类型类描述了类型间强制转换的重载方法。

class Coe (α : Type) (β : Type) where
  coe : α → β

一个 Coe Pos Nat 的实例就足够让先前的代码正常工作了。

instance : Coe Pos Nat where
  coe x := x.toNat

#eval [1, 2, 3, 4].drop (2 : Pos)

[3, 4]

用 #check 来看隐藏在幕后的实例搜索。

#check [1, 2, 3, 4].drop (2 : Pos)

List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat

链式强制转换

在寻找强制转换时，Lean 会尝试通过一系列较小的强制转换来组成一个完整的强制转换。例如，已经存在一个从 Nat 到 Int 的强制转换实例。由于这个实例结合了 Coe Pos Nat 实例，我们就可以写出下面的代码：

def oneInt : Int := Pos.one

这个定义用到了两个强制转换：从 Pos 到 Nat，再从 Nat 到 Int。

Lean 编译器在存在循环强制转换的情况下不会陷入无限循环。例如，即使两个类型 A 和 B 可以互相强制转换，在转换中 Lean 也可以找到一个路径。

inductive A where
  | a

inductive B where
  | b

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

提示：双括号 () 是构造子 Unit.unit 的简写。在派生 Repr B 实例后，

#eval coercedToB

结果为：

B.b

Option 类型类似于 C# 和 Kotlin 中可为空的类型：none 构造子就代表了一个不存在的值。 Lean 标准库定义了一个从任意类型 α 到 Option α 的强制转换，效果是会将值包裹在 some 中。这使得 option 类型用起来更像是其他语言中可为空的类型，因为 some 是可以忽略的。例如，可以找到列表中最后一个元素的函数 List.getLast?，就可以直接返回值 x 而无需加上 some：

def List.last? : List α → Option α
  | [] => none
  | [x] => x
  | _ :: x :: xs => last? (x :: xs)

实例搜索找到强制转换，并插入对 coe 的调用，该调用会将参数包装在 some 中。这些强制转换可以是链式的，这样嵌套使用 Option 时就不需要嵌套的 some 构造子：

def perhapsPerhapsPerhaps : Option (Option (Option String)) :=
  "Please don't tell me"

仅当 Lean 遇到推断出的类型和剩下的程序需要的类型不匹配时，才会自动使用强制转换。在遇到其它错误时，强制转换不会被使用。例如，如果遇到的错误是实例缺失，强制类型转换不会被使用：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

这可以通过手动指定 OfNat 所需的类型来解决：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  (392 : Nat)

此外，强制转换用一个上箭头手动调用。

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  ↑(392 : Nat)

在一些情况下，这可以保证 Lean 找到了正确的实例。这也会让程序员的意图更加清晰。

非空列表与依值强制转换

当 β 类型中的值可以对应每一个 α 类型中的值时，Coe α β 实例才是合理的。将 Nat 强制转换为 Int 是合理的，因为 Int 类型中包含了全部的自然数。类似地，一个从非空列表到常规列表的强制转换也是合理的，因为 List 类型可以表示每一个非空列表：

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

这使得非空列表可以使用全部的 List API。

另一方面，我们不可能写出一个 Coe (List α) (NonEmptyList α) 的实例，因为没有任何一个非空列表可以表示一个空列表。这个限制可以通过其他方式的强制转换来解决，该强制转换被称为 依值强制转换（dependent coercions） 。当是否能将一种类型强制转换到另一种类型依赖于具体的值时，依值强制转换就派上用场了。就像 OfNat 类型类需要具体的 Nat 来作为参数，依值强制转换也接受要被强制转换的值作为参数：

class CoeDep (α : Type) (x : α) (β : Type) where
  coe : β

这可以使得只选取特定的值，通过加上进一步的类型类约束或者直接写出特定的构造子。例如，任意非空的 List 都可以被强制转换为一个 NonEmptyList：

instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := { head := x, tail := xs }

强制转换为类型（本节中 sort 的翻译待讨论）

在数学中，一个建立在集合上，但是比集合具有额外的结构的概念是很常见的。例如，一个幺半群就是一些集合 S，一个 S 中的元素 s，以及一个 S 上结合的二元运算，使得 s 在运算的左侧和右侧都是中性的。 S 是这个幺半群的“载体集”。自然数集上的零和加法构成一个幺半群，因为加法是满足结合律的，并且为任何一个数字加零都是恒等的。类似地，自然数上的一和乘法也构成一个幺半群。幺半群在函数式编程中的应用也很广泛：列表，空列表，和连接运算符构成一个幺半群。字符串，空字符串，和连接运算符也构成一个幺半群：

structure Monoid where
  Carrier : Type
  neutral : Carrier
  op : Carrier → Carrier → Carrier

def natMulMonoid : Monoid :=
  { Carrier := Nat, neutral := 1, op := (· * ·) }

def natAddMonoid : Monoid :=
  { Carrier := Nat, neutral := 0, op := (· + ·) }

def stringMonoid : Monoid :=
  { Carrier := String, neutral := "", op := String.append }

def listMonoid (α : Type) : Monoid :=
  { Carrier := List α, neutral := [], op := List.append }

给定一个幺半群，我们就可以写出一个 foldMap 函数，该函数在一次遍历中将整个列表中的元素映射到载体集中，然后使用幺半群的运算符将它们组合起来。由于幺半群有单位元，所以当列表为空时我们就可以返回这个值。又因为运算符是满足结合律的，这个函数的用户不需要关心函数结合元素的顺序到底是从左到右的还是从右到左的。

def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

尽管一个幺半群是由三部分信息组成的，但在提及它的载体集时使用幺半群的名字也是很常见的。说“令 A 为一个幺半群，并令 x 和 y 为 A 中的元素”是很常见的，而不是说“令 A 为一个幺半群，并令 x 和 y 为载体集中的元素”。这种方式可以通过定义一种新的强制转换来在 Lean 中实现，该转换从幺半群到它的载体集。

CoeSort 类型类和 Coe 大同小异，只是要求强制转换的目标一定要是一个 sort，即 Type 或 Prop。词语 sort 指的是这些分类其他类型的类型——Type 分类那些本身分类数据的类型，而 Prop 分类那些本身分类其真实性证据的命题。正如在类型不匹配时会检查 Coe 一样，当在预期为 sort 的上下文中提供了其他东西时，会使用 CoeSort。

从一个幺半群到它的载体集的强制转换会返回该载体集：

instance : CoeSort Monoid Type where
  coe m := m.Carrier

有了这个强制转换，类型签名变得不那么繁琐了：

def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
  let rec go (soFar : M) : List α → M
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

另一个有用的 CoeSort 使用场景是它可以让 Bool 和 Prop 建立联系。就像在有序性和等价性那一节我们提到的，Lean 的 if 表达式需要条件为一个可判定的命题而不是一个 Bool。然而，程序通常需要能够根据布尔值进行分支。 Lean 标准库并没有定义两种 if 表达式，而是定义了一种从 Bool 到命题的强制转换，即该 Bool 值等于 true：

instance : CoeSort Bool Prop where
  coe b := b = true

如此，这个 sort 将是一个 Prop 而不是 Bool。

强制转换为函数（本节翻译需要润色）

许多在编程中常见的数据类型都会有一个函数和一些额外的信息组成。例如，一个函数可能附带一个名称以在日志中显示，或附带一些配置数据。此外，将一个类型放在结构体的字段中（类似于 Monoid 的例子）在某些上下文中是有意义的，这些上下文中存在多种实现操作的方法，并且需要比类型类允许的更手动的控制。例如，JSON 序列化器生成的值的具体细节可能很重要，因为另一个应用程序期望特定的格式。有时，仅从配置数据就可以推导出函数本身。

CoeFun 类型类可以将非函数类型的值转换为函数类型的值。 CoeFun 有两个参数：第一个是需要被转变为函数的值的类型，第二个是一个输出参数，决定了到底应该转换为哪个函数类型。

class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where
  coe : (x : α) → makeFunctionType x

第二个参数本身是一个可以计算类型的函数。在 Lean 中，类型是一等公民，可以作为函数参数被传递，也可以作为返回值，就像其他东西一样。

例如，一个将常量加到其参数的函数可以表示为围绕要添加的量的包装，而不是通过定义一个实际的函数：

structure Adder where
  howMuch : Nat

一个为参数加上5的函数的 howMuch 字段为 5：

def add5 : Adder := ⟨5⟩

这个 Adder 类型并不是一个函数，将它应用到一个参数会报错：

#eval add5 3

function expected at
  add5
term has type
  Adder

定义一个 CoeFun 实例让 Lean 来将 adder 转换为一个 Nat → Nat 的函数：

instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3

因为所有的 Adder 都应该被转换为 Nat → Nat 的函数，CoeFun 的第二个参数就被省略了。

当我们需要这个值来决定正确的函数类型时，CoeFun 的第二个参数就派上用场了。例如，给定下面的 JSON 值表示：

inductive JSON where
  | true : JSON
  | false : JSON
  | null : JSON
  | string : String → JSON
  | number : Float → JSON
  | object : List (String × JSON) → JSON
  | array : List JSON → JSON
deriving Repr

一个 JSON 序列化器是一个结构体，它不仅包含它知道如何序列化的类型，还包含序列化代码本身：

structure Serializer where
  Contents : Type
  serialize : Contents → JSON

对字符串的序列化器只需要将所给的字符串包装在 JSON.string 构造子中即可：

def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

将 JSON 序列化器视为序列化其参数的函数需要提取可序列化数据的内部类型：

instance : CoeFun Serializer (fun s => s.Contents → JSON) where
  coe s := s.serialize

有了这个实例，一个序列化器就能直接应用在参数上。

def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

这个序列化器可以直接传入 buildResponse：

#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"

JSON.object
  [("title", JSON.string "Functional Programming in Lean"),
   ("status", JSON.number 200.000000),
   ("record", JSON.string "Programming is fun!")]

附注：将 JSON 表示为字符串

当 JSON 被编码为 Lean 对象时可能有点难以理解。为了帮助保证序列化的响应是我们所期望的，写一个简单的从 JSON 到 String 的转换器可能会很方便。第一步是简化数字的显示。 JSON 不区分整数和浮点数，Float 类型即可用来代表二者。在 Lean 中，Float.toString 包括数字的后继零。

#eval (5 : Float).toString

"5.000000"

解决方案是写一个小函数，这个函数可以清理掉所有的后继零，和后继的小数点：

def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

有了这个定义，#eval dropDecimals (5 : Float).toString 结果为 "5"，#eval dropDecimals (5.2 : Float).toString 结果为 "5.2"。

下一步是定义一个辅助函数来连接字符串列表，并在中间添加分隔符：

def String.separate (sep : String) (strings : List String) : String :=
  match strings with
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

这个函数用于处理 JSON 数组和对象中的逗号分隔元素。 #eval ", ".separate ["1", "2"] 结果为 "1, 2"，#eval ", ".separate ["1"] 结果为 "1"，#eval ", ".separate [] 结果为 ""。

最后，需要一个字符串转义程序来处理 JSON 字符串，以便包含 "Hello!" 的 Lean 字符串可以输出为 ""Hello!"”。幸运的是，Lean 编译器已经包含了一个用于转义 JSON 字符串的内部函数，叫做 Lean.Json.escape。要使用这个函数，可以在文件开头添加 import Lean。

将 JSON 值转换为字符串的函数被声明了 partial，因为 Lean 并不知道它是否停机。这是因为出现在函数中的 asString 的递归调用被应用到了 List.map，这种模式的递归已经复杂到 Lean 无法知道递归过程中值的规模是否是减小的。在一个只需要产生 JSON 字符串而不需要让过程在数学上是合理的的应用中，让函数是 partial 的不太可能造成麻烦。

partial def JSON.asString (val : JSON) : String :=
  match val with
  | true => "true"
  | false => "false"
  | null => "null"
  | string s => "\"" ++ Lean.Json.escape s ++ "\""
  | number n => dropDecimals n.toString
  | object members =>
    let memberToString mem :=
      "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
    "{" ++ ", ".separate (members.map memberToString) ++ "}"
  | array elements =>
    "[" ++ ", ".separate (elements.map asString) ++ "]"

有了这个定义，序列化的结果更加易读了：

#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString

"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"

可能会遇到的问题

自然数字面量是通过 OfNat 类型类重载的。因为在类型不匹配时才会触发强制转换，而不是在找不到实例时，所以当对于某类型的 OfNat 实例缺失时，并不会触发强制转换：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

设计原则

强制转换是一个强大的工具，请负责任地使用它。一方面，它可以使 API 设计得更贴近领域内使用习惯。这是繁琐的手动转换函数和一个清晰的程序间的差别。正如 Abelson 和 Sussman 在《计算机程序的构造和解释》（ Structure and Interpretation of Computer Programs ）（麻省理工学院出版社，1996年）前言中所写的那样：

写程序须以让人读明白为主，让计算机执行为辅。

明智地使用强制转换，可以使得代码更加易读——这是与领域内专家的交流的基础。然而，严重依赖强制转换的 API 会有许多限制。在你自己的代码中使用强制转换前，认真思考这些限制。

首先，强制转换只应该出现在类型信息充足，Lean 能够知道所有参与的类型的语境中。因为强制转换类型类中并没有输出参数这么一说。这意味着在函数上添加返回类型注释可以决定是类型错误还是成功应用强制转换。例如，从非空列表到列表的强制转换使以下程序得以运行：

def lastSpider : Option String :=
  List.getLast? idahoSpiders

另一方面，如果类型注释被省略了，那么结果的类型就是未知的，那么 Lean 就无法找到对应的强制转换。

def lastSpider :=
  List.getLast? idahoSpiders

application type mismatch
  List.getLast? idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.34258 : Type

通常来讲，如果一个强制转换因为一些原因失败了，用户会收到原始的类型错误，这会使在强制转换链上定位错误变得十分困难。

最后，强制转换不会在字段访问符号的上下文中应用。这意味着需要强制转换的表达式与不需要强制转换的表达式之间仍然存在重要区别，而这个区别对用户来说是肉眼可见的。

Lean 函数式编程