LSR 018 - Never 底类型与 raise 终止效应规范¶

基本信息¶

LSR 编号 018
标题 Never 底类型与 raise 终止效应规范
作者 Ziyang-Bai
状态草案
类型标准规范
创建日期 08-27-2026
归属项目编译器、运行时、标准库

摘要¶

定义 Lamina 内部底类型 Never、终止效应、模块内文本终止函数 raise 和 std.mathematics_error.raise 的静态类型与运行时语义。Never 表示求值以终止效应结束的表达式；raise 先求值载荷，再生成 VM 运行时故障并结束当前执行路径。

技术规范¶

1. 术语¶

本规范使用下列术语：

Never: 编译器内部底类型。其值域为空，表达式求值以终止效应结束。
正常返回: 表达式产生一个值，控制流进入后继求值位置。
终止效应: 表达式生成运行时故障，当前执行路径结束，控制流展开至执行边界并清理已取得的资源。
载荷: raise 接收的值。VM 将载荷转换为诊断文本。
执行边界: VM 顶层运行入口或 Lamina 回调入口。终止效应在该边界转换为进程诊断或回调错误结果。

2. `Never` 的表示¶

Never 是编译器内部底类型，类型诊断使用 Never 作为内部拼写。它不引入可构造的运行时值，也不要求某种类型池、值标签或指令布局。表达式、函数和模块继续使用 Lamina 核心语言的静态检查框架 [1]。

Never 的值域为空。类型为 Never 的表达式以终止效应结束当前执行路径，后继求值位置只接收正常返回表达式产生的值。

raise("stopped") # 表达式类型为内部 Never

3. 赋值关系¶

当实际表达式类型为 Never 时，类型检查器接受任意期望类型。该关系写作：

Never <: T

其中 T 表示任意完整类型。

该规则应用于：

变量初始化
函数实参
显式返回
尾表达式返回
条件分支

编译器内部的未知类型状态、none、Null 和 Never 保持独立，也不等于数学等价查询返回的固定状态 std.cas.Unknown。

4. 类型统一¶

分支和复合表达式按下列规则统一 Never：

unify(Never, T)         = T
unify(T, Never)         = T
unify(Never, Never)     = Never

if 表达式使用统一结果作为整体类型。

func choose(ok bool) -> int {
    if ok {
        42
    } else {
        raise("unavailable")
    }
}

上例 then 分支的基本类型为 num，值 42 满足 int 约束， else 分支类型为 Never，因此 if 的基本类型为 num，正常返回值仍须满足 int 约束。

当全部分支类型均为 Never 时，整个表达式类型为 Never。

5. 内建错误值¶

std.mathematics_error 公开导出固定内建类型 MathError 及同名构造函数 [2]：

func MathError(code text, operation text, message text) -> MathError

MathError 保存三个只读 text 字段：

code：供程序识别的错误类别
operation：发生错误的运算或函数名称
message：面向用户的诊断文本

构造函数按源码从左到右对三个实参各求值一次。字段类型在调用处检查；成功构造后可通过 error.code、error.operation 和 error.message 读取。两个 MathError 值按三个字段的文本值逐一比较相等。

标准字符串表示为 MathError("code", "operation", "message")，字段按上述顺序输出。每个字段使用双引号包围；字段中的双引号和反斜杠加反斜杠转义，换行、回车和制表符分别写成 \n、\r 和 \t。

import std.mathematics_error

let error = mathematics_error.MathError(
    "DomainError", "divide", "zero divisor"
)
let operation = error.operation

普通数学函数直接返回计算结果，计算失败沿本规范的终止效应传播。MathError 用于保留错误类别、运算名称和诊断内容。

6. 函数返回¶

函数尾表达式为 Never 时，函数体满足任意声明返回类型。

func fail(message text) -> int {
    raise(message)
}

函数的声明结果仍为带 int 值约束的 num，函数体实际尾表达式类型为 Never。执行 fail 时产生终止效应，不伪造一个整数结果。正常返回路径满足声明的返回类型和值约束，终止路径不进入正常后继；是否使用独立终止指令、内联或普通调用由实现决定。

7. 函数类型关系¶

函数类型的参数列表、值约束和量纲契约保持相容检查。实际函数返回 Never 时，其函数值满足参数契约相同、返回类型为 T 的期望函数类型：

func(P...) -> Never <: func(P...) -> T

该放宽只作用于 Never 返回。其他函数类型仍须检查完整参数和结果契约；不能只因 int、real 等标注的基本类型均为 num，就把只接受整数的函数传给可能以任意实数调用的函数位置。

func invoke(f func(text) -> int, message text) -> int {
    f(message)
}

invoke(raise, "boom")

raise 的参数列表为 (text)，实际返回类型为 Never，因此实参满足 func(text) -> int。执行 invoke 时，调用 f 产生终止效应。

8. 文本 `raise` 绑定¶

每个已编译模块的源码作用域具有下列内建可调用绑定：

func raise(message text) -> Never

该绑定具有下列属性：

源码名为 raise
参数类型为 text
返回类型为内部 Never
绑定在当前模块源码作用域中可见
绑定保持模块私有，不进入模块公开导出
调用产生本规范定义的终止效应
用户同名函数声明产生保留绑定重定义诊断

raise 按普通标识符解析规则参与表达式检查。直接调用、变量捕获、参数传递和回调调用具有相同的可观察语义，不要求实现通过同一个物理函数体或调用帧执行。

let fail = raise
fail("boom")

9. 结构化 `raise` 绑定¶

std.mathematics_error 作为标准库模块公开导出下列普通函数 [2]：

func raise(error MathError) -> Never

参数类型为第 5 节定义的 std.mathematics_error.MathError。该函数接收完整错误值，并以其标准字符串表示作为终止载荷。

import std.mathematics_error

func abort(error mathematics_error.MathError) -> int {
    mathematics_error.raise(error)
}

mathematics_error.raise 是普通模块成员。限定调用、函数值捕获和回调传递共享同一静态类型和运行时效应。

let fail = mathematics_error.raise

10. 终止效应¶

调用任一 raise 函数时，运行时按下列顺序执行：

按普通调用规则求值并绑定实参，各求值一次
对载荷执行一次标准字符串转换
生成 Runtime 类别的故障，保留文本或完整 MathError 诊断
结束当前执行路径，展开至当前执行边界，完成沿途临时值和资源清理

不要求为 raise 建立普通调用帧；内联、专用操作或其他实现方式必须保持求值次数、故障内容、清理顺序和边界传播一致。若实参求值或载荷转换先失败，传播该原错误，不得继续执行或用一个新 raise 载荷掩盖它。

终止效应沿表达式求值上下文传播。外层函数调用、算术表达式、条件表达式和变量初始化在收到该效应后结束当前执行路径。

let value = compute(raise("stopped"))

上例先执行 raise("stopped")。compute 的函数体不进入执行，value 不获得运行时值。

11. 顶层效应¶

终止效应到达 VM 顶层运行入口时，运行入口执行下列动作：

清理当前执行路径持有的调用状态
清理临时值并释放其所有权
输出故障诊断
返回非零进程状态

文本载荷的诊断格式为：

RuntimeError: <message>

raise("boom")

产生：

RuntimeError: boom

MathError 载荷保留第 5 节定义的完整字符串表示：

RuntimeError: MathError("DomainError", "divide", "zero divisor")

12. 回调效应¶

终止效应到达 Lamina 回调入口时，回调入口执行下列动作：

展开回调创建的执行状态
恢复外层执行状态
清理回调临时值与已取得的资源
将故障诊断转换为回调错误结果

回调与顶层路径保留相同的错误类别、操作和载荷语义。原生调用边界只接收回调错误结果，不要求跨不支持展开的 C 帧传播异常。原生调用者必须检查并向外传播该错误，不能继续使用不存在的回调结果或返回成功。

13. 实现自由与可观察行为¶

本规范不规定 Raise 指令宽度、寄存器格式、函数末尾字节码、分派表或反汇编布局，也不要求每次终止效应经过普通调用帧。实现可采用专用指令、调用或其他机制，但必须保持相同的错误载荷、求值次数、路径终止、资源清理和执行边界行为。优化不得执行终止点之后的副作用。

统一 num 不取消普通参数或返回约束检查。失败的数域检查、具体整数取值检查、资源限制、取消和内部故障均沿错误通道传播；不能用未求值式、零值或 std.cas.Unknown 代替错误。只有声明支持未求值结果的数学求值接口可返回这种数学值 [2]。

14. 求值次数¶

raise(payload_expression) 对 payload_expression 求值一次。VM 对求值结果执行一次字符串转换。

raise(make_message())

规范求值顺序为：

调用 make_message 一次
将返回文本传给 raise
转换文本载荷一次
产生终止效应

函数值调用保持相同顺序：

let fail = raise
fail(make_message())

15. 诊断¶

用户声明名为 raise 的函数时，分析器报告：

cannot redefine builtin `raise`

文本终止效应到达顶层时，运行时报告：

RuntimeError: <payload>

结构化数学错误终止效应到达顶层时，运行时报告：

RuntimeError: MathError(...)

分析诊断指向用户声明的 raise 标识符。运行时诊断使用载荷的标准字符串表示。

16. 一致性要求¶

符合本规范的实现验证下列行为：

if 的一个分支类型为 Never 时，另一分支决定整体类型
函数尾表达式为 raise 时满足声明返回类型
raise 作为函数值调用时产生文本终止效应
raise 作为具体返回类型回调传递时产生相同终止效应
mathematics_error.raise 作为限定函数值传递时保留完整错误载荷
用户 raise 声明产生保留绑定重定义诊断
文本载荷顶层诊断为 RuntimeError: <message>
MathError 的三个字段保持只读，顶层诊断包含按字段顺序转义后的完整错误内容
终止效应阻止当前路径的正常后继，并在顶层和回调边界完成规定的资源清理与错误传播

LSR 018 - Never 底类型与 raise 终止效应规范¶

基本信息¶

摘要¶

技术规范¶

1. 术语¶

2. `Never` 的表示¶

3. 赋值关系¶

4. 类型统一¶

5. 内建错误值¶

6. 函数返回¶

7. 函数类型关系¶

8. 文本 `raise` 绑定¶

9. 结构化 `raise` 绑定¶

10. 终止效应¶

11. 顶层效应¶

12. 回调效应¶

13. 实现自由与可观察行为¶

14. 求值次数¶

15. 诊断¶

16. 一致性要求¶

17. 引用¶

LSR

导航

Related Topics

LSR 018 - Never 底类型与 raise 终止效应规范¶

基本信息¶

摘要¶

技术规范¶

1. 术语¶

2. Never 的表示¶

3. 赋值关系¶

4. 类型统一¶

5. 内建错误值¶

6. 函数返回¶

7. 函数类型关系¶

8. 文本 raise 绑定¶

9. 结构化 raise 绑定¶

10. 终止效应¶

11. 顶层效应¶

12. 回调效应¶

13. 实现自由与可观察行为¶

14. 求值次数¶

15. 诊断¶

16. 一致性要求¶

17. 引用¶

2. `Never` 的表示¶

8. 文本 `raise` 绑定¶

9. 结构化 `raise` 绑定¶