Note. 显式错误规则与 Kotlin 的底类型

Glomzzz
2026-10-10
About

以词项的集合的语法和一步规约的十条求值规则为基础，可以另行加入错误项 $wrong$ ，并规定错误传播（注意这些新增规则属于扩展语言，不改动原语言）．只写 $succ true ⟶ wrong$ 还不完整：还要处理 $succ false$ 、 $pred true$ 、非布尔条件，以及嵌套位置里的错误．

记 $𝑏$ 为 $true$ 或 $false$ ， $nv$ 为值与数值中的数值．可以补上这些错误规则，其中 $op$ 分别取 $succ$ 、 $pred$ 、 $iszero$ ：

E-OpBool：前提无；结论 op b ⟶ wrong E-IfNat：前提无；结论 if nv then t_(2) else t_(3) ⟶ wrong E-OpWrong：前提无；结论 op wrong ⟶ wrong E-IfWrong：前提无；结论 if wrong then t_(2) else t_(3) ⟶ wrong

原同余规则继续向正在求值的子项推进．于是 $succ (if true then false else 0)$ 先规约到 $succ false$ ，再规约到 $wrong$ ； $pred (succ true)$ 先变成 $pred wrong$ ，再向外传播成 $wrong$ ． $wrong$ 本身不再规约，需要单独作为异常终点，与原来定义的普通值区分开．未选中的分支仍不会求值，例如 $if true then 0 else wrong$ 得到 $0$ ，不能不分位置地把整项都传播成错误．

Kotlin 可以显式写出这种异常控制流：

fun succ(x: Any): Int = when (x) {
    is Int -> x + 1
    else -> throw IllegalArgumentException("succ expects an Int")
}

fun fail(message: String): Nothing =
    throw IllegalArgumentException(message)

fun requireNat(n: Int): Int =
    if (n >= 0) n else fail("negative number")

// succ(true) 会抛出异常；requireNat(-1) 也会抛出异常．
// 这里借用 Kotlin 的 Int 演示错误处理，不把机器整数当作无界自然数．

fun succ(x: Any): Int = when (x) {
    is Int -> x + 1
    else -> throw IllegalArgumentException("succ expects an Int")
}

fun fail(message: String): Nothing =
    throw IllegalArgumentException(message)

fun requireNat(n: Int): Int =
    if (n >= 0) n else fail("negative number")

// succ(true) 会抛出异常；requireNat(-1) 也会抛出异常．
// 这里借用 Kotlin 的 Int 演示错误处理，不把机器整数当作无界自然数．

requireNat requireNat 的 else else 分支之所以能放在需要 Int Int 的位置，是因为 fail(...) fail(...) 的类型为 Nothing Nothing ，表示它不会正常返回一个值． Kotlin 的类型系统规格把 Nothing Nothing 定义成底类型，通常写作 $⊥$ ．它是任何类型的子类型，即 $⊥ < : 𝑇$ 对任意 $𝑇$ 成立．这里 $𝑆 < : 𝑇$ 表示子类型关系，即 $𝑆$ 是 $𝑇$ 的子类型；相关类型规则允许 $𝑆$ 类型的表达式用在要求 $𝑇$ 类型的位置．因此不返回的失败分支可以和返回 Int Int 的成功分支放在同一个 if if 里．

这里要分清三个不同层次的概念： $wrong$ 是对象语言里的错误词项， IllegalArgumentException IllegalArgumentException 是 Kotlin 的异常对象， $⊥$ 是描述表达式不会正常产出值的类型． Nothing Nothing 没有正常的值，与异常对象或 null null （ Nothing? Nothing? ）都不同．抛异常的表达式可以具有底类型，死循环表达式同样不会返回，可见“错误”与 $⊥$ 并不等同．

仅仅补上运行时错误规则，不会自动得到这样的子类型系统．若把显式异常加入类型与类型判断的定型系统，也必须写明异常如何定型，并相应重述进展与保型；不能直接套用未扩展语言的证明就声称“良类型程序永不抛异常”．类型安全采用的则是未扩展语言：不加入错误项，让类型规则排除受阻．

Note. 显式错误规则与 Kotlin 的底类型

References

Backlinks