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

2. `Never` 的表示¶

Never 只存在于编译期类型池。类型诊断使用 Never 作为内部拼写。源代码类型语法保持现有类型名集合，运行时值表示保持现有 ValueKind 集合。表达式、函数和模块继续使用 Lamina 核心语言的静态检查框架 [1]。

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

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

3. 赋值关系¶

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

Never <: T

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

该规则应用于：

变量初始化
函数实参
显式返回
尾表达式返回
条件分支
模式匹配分支
ADT 构造器字段检查

Unknown、none、Null 和 Never 保持各自独立的类型身份。

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 分支类型为 int，else 分支类型为 Never，if 表达式类型为 int。

穷尽 match 表达式按 LSR-005 的分支检查规则折叠所有分支类型 [3]。Never 分支保持其他正常返回分支确定的结果类型。

match state {
    Ready(value) => value,
    Failed(message) => raise(message)
}

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

5. ADT 泛型绑定¶

ADT 构造器字段接收类型为 Never 的实际表达式时，字段检查成立，泛型参数绑定保持当前状态。

type Box<T> = Box(T)

let value = Box(raise("missing"))

raise 的终止效应先于构造器创建并结束当前路径。类型推导保持 T 的当前绑定状态，其他字段或期望类型继续决定 T。

6. 函数返回¶

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

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

函数的声明返回类型保持 int；函数体的实际尾表达式类型为 Never。执行 fail 时产生终止效应。

编译器为正常返回函数生成 Ret 终止操作，为以终止效应结束的内建函数生成 Raise 终止操作。函数末尾的终止操作与函数体实际控制流一致。

7. 函数类型关系¶

函数类型的参数列表保持精确相等。实际函数返回 Never 时，其函数值满足参数列表相同、返回类型为 T 的期望函数类型：

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

该规则只作用于 Never 返回。其他函数类型继续使用参数列表和返回类型精确相等规则。

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 终止操作结束
用户同名函数声明产生保留绑定重定义诊断

raise 按普通标识符解析规则参与表达式检查。直接调用、变量捕获、参数传递和回调调用均调用同一函数体。

let fail = raise
fail("boom")

9. 结构化 `raise` 绑定¶

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

func raise(error MathError) -> Never

其参数使用 std.mathematics_error.MathError 的名义 ADT 类型 [4]。该函数求值完整错误值，并以错误值的标准字符串表示作为终止载荷。

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 函数时，VM 按下列顺序执行：

求值实参一次
将实参存入函数参数位置
进入普通 Lamina 函数调用帧
读取载荷值
调用一次载荷的标准字符串转换
构造 Runtime 类别的 VmFault
结束当前指令流
展开 VM 调用帧至当前执行边界

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

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

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

11. 顶层效应¶

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

清理当前 VM 调用帧
清理寄存器中的临时值
输出故障诊断
返回非零进程状态

文本载荷的诊断格式为：

RuntimeError: <message>

raise("boom")

产生：

RuntimeError: boom

MathError 载荷保留完整 ADT 字符串表示：

RuntimeError: MathError(code, operation, message)

12. 回调效应¶

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

展开回调创建的 VM 帧
恢复外层 VM 寄存器和帧指针
清理回调寄存器区域
将 VmFault 诊断转换为回调错误结果

回调调用路径与顶层调用路径使用同一 Raise 操作和 VmFault 类型。终止故障在 VM 内部产生，原生调用边界只接收回调错误结果。

13. VM `Raise` 操作¶

字节码提供四字节 Raise 指令：

Raise source_reg

source_reg 保存已求值载荷。其余指令字节保持固定宽度布局。

Raise 和 Ret 都是函数终止操作。汇编器检查函数最后一条指令；最后一条为 Raise 时，函数字节码在该位置结束。

VM 的两种分派实现共享相同 Raise 处理器语义：

直接线程分派表包含 Raise 标签
switch 分派包含 Raise 分支
指令元数据使用单寄存器格式
反汇编器显示 raise 和源寄存器

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 时，另一分支决定整体类型
穷尽 match 的 Never 分支参与底类型统一
函数尾表达式为 raise 时满足声明返回类型
raise 作为函数值调用时产生文本终止效应
raise 作为具体返回类型回调传递时产生相同终止效应
mathematics_error.raise 作为限定函数值传递时保留完整错误载荷
用户 raise 声明产生保留绑定重定义诊断
文本载荷顶层诊断为 RuntimeError: <message>
MathError 载荷顶层诊断包含完整 MathError(...)
Raise 结束函数字节码，当前执行路径在该指令终止

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

基本信息¶

摘要¶

技术规范¶

1. 术语¶

2. `Never` 的表示¶

3. 赋值关系¶

4. 类型统一¶

5. ADT 泛型绑定¶

6. 函数返回¶

7. 函数类型关系¶

8. 文本 `raise` 绑定¶

9. 结构化 `raise` 绑定¶

10. 终止效应¶

11. 顶层效应¶

12. 回调效应¶

13. VM `Raise` 操作¶

14. 求值次数¶

15. 诊断¶

16. 一致性要求¶

17. 引用¶

LSR

导航

Related Topics

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

基本信息¶

摘要¶

技术规范¶

1. 术语¶

2. Never 的表示¶

3. 赋值关系¶

4. 类型统一¶

5. ADT 泛型绑定¶

6. 函数返回¶

7. 函数类型关系¶

8. 文本 raise 绑定¶

9. 结构化 raise 绑定¶

10. 终止效应¶

11. 顶层效应¶

12. 回调效应¶

13. VM Raise 操作¶

14. 求值次数¶

15. 诊断¶

16. 一致性要求¶

17. 引用¶

2. `Never` 的表示¶

8. 文本 `raise` 绑定¶

9. 结构化 `raise` 绑定¶

13. VM `Raise` 操作¶