以 [定义] 项的集合 的语法和 [定义] 一步归约 的十条求值规则为基础，可以另行加入错误项 $\text{wrong}$，并规定错误传播。以下讨论的是这门扩展语言，不把新增规则当作未扩展语言的规则。只写 $\text{succ }\text{ true }⟶\text{ wrong}$ 还不完整：还要处理 $\text{succ }\text{ false}$、$\text{pred }\text{ true}$、非布尔条件，以及嵌套位置里的错误。

记 $𝑏$ 为 $\text{true}$ 或 $\text{false}$， 为 [定义] 值与数值 中的数值。可以补上这些错误规则，其中 $\text{op}$ 分别取 $\text{succ}$、$\text{pred}$、$\text{iszero}$：

原同余规则继续向正在求值的子项走。于是 $\text{succ }\left(\text{if }\text{ true }\text{ then }\text{ false }\text{ else }0\right)$ 先归约到 $\text{succ }\text{ false}$，再归约到 $\text{wrong}$；$\text{pred }\left(\text{succ }\text{ true}\right)$ 先变成 $\text{pred }\text{ wrong}$，再向外传播成 $\text{wrong}$。$\text{wrong}$ 本身不再归约，应被识别为一种异常终点，而非原来定义的普通值。未选中的分支仍不会求值，例如 $\text{if }\text{ true }\text{ then }0\text{ else }\text{ 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 分支为什么能放在需要 Int Int 的位置？ fail(...) fail(...) 的类型是 Nothing Nothing ，表示它不会正常返回一个值。Kotlin 的 类型系统规格把 Nothing Nothing 定义成底类型（bottom type），通常写作 $\perp$、读作 bottom。它是任何类型的子类型（subtype），即 $\perp <:𝑇$ 对任意 $𝑇$ 成立。这里 $𝑆<:𝑇$ 的意思是：$𝑆$ 类型的表达式可以放进要求 $𝑇$ 类型的上下文。因此不返回的失败分支可以和返回 Int Int 的成功分支放在同一个 if if 里。

必须区分三个对象：$\text{wrong}$ 是对象语言里的错误项， IllegalArgumentException IllegalArgumentException 是 Kotlin 的异常对象，$\perp$ 是描述表达式不会正常产出值的类型。异常对象本身不是 Nothing Nothing ； Nothing Nothing 没有正常的值，也不是 null null （ Nothing? Nothing? 是另一回事）。抛异常的表达式可以具有底类型，永远循环的表达式也可以不返回，所以不能把“错误”与 $\perp$ 当作同义词。

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