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`` 的表达式以终止效应结束当前执行路径，后继求值位置只接收正常返回表达式产生的值。

.. code-block:: text

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


3. 赋值关系
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   Never <: T


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

该规则应用于：

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

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

4. 类型统一
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

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


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

.. code-block:: text

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


上例中 then 分支类型为 ``int``，else 分支类型为 ``Never``，``if`` 表达式类型为 ``int``。

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

.. code-block:: text

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


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

5. ADT 泛型绑定
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   type Box<T> = Box(T)

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


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

6. 函数返回
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

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


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

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

7. 函数类型关系
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

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


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

.. code-block:: text

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

   invoke(raise, "boom")


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

8. 文本 ``raise`` 绑定
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


编译器在每个已编译模块的源码作用域注入下列普通函数绑定：

.. code-block:: text

   func raise(message text) -> Never


该绑定具有下列属性：

- 源码名为 ``raise``
- 参数名义类型为 ``text``
- 返回类型为内部 ``Never``
- 绑定在当前模块源码作用域中可见
- 绑定保持模块私有，不进入模块公开导出
- 函数体以 ``Raise`` 终止操作结束
- 用户同名函数声明产生保留绑定重定义诊断

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

.. code-block:: text

   let fail = raise
   fail("boom")


9. 结构化 ``raise`` 绑定
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   func raise(error MathError) -> Never


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

.. code-block:: text

   import std.mathematics_error

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


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

.. code-block:: text

   let fail = mathematics_error.raise


10. 终止效应
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

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

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

.. code-block:: text

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


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

11. 顶层效应
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

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

文本载荷的诊断格式为：

.. code-block:: text

   RuntimeError: <message>


.. code-block:: text

   raise("boom")


产生：

.. code-block:: text

   RuntimeError: boom


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

.. code-block:: text

   RuntimeError: MathError(code, operation, message)


12. 回调效应
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

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

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

13. VM ``Raise`` 操作
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   Raise source_reg


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

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

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

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

14. 求值次数
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   raise(make_message())


规范求值顺序为：

1. 调用 ``make_message`` 一次
2. 将返回文本传给 ``raise``
3. 转换文本载荷一次
4. 产生终止效应

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

.. code-block:: text

   let fail = raise
   fail(make_message())


15. 诊断
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   cannot redefine builtin `raise`


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

.. code-block:: text

   RuntimeError: <payload>


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

.. code-block:: text

   RuntimeError: MathError(...)


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

16. 一致性要求
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

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

17. 引用
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


.. [1] :doc:`LSR-000 - Lamina 核心语言规范（草案） <LSR-000>` - 定义表达式、函数、模块和静态类型检查框架
.. [2] :doc:`LSR-004 - 标准库 <LSR-004>` - 定义 ``std`` 模块和标准错误类别
.. [3] :doc:`LSR-005 - 模式匹配 <LSR-005>` - 定义 ``match`` 表达式、穷尽检查和分支类型
.. [4] :doc:`LSR-011 - 代数数据类型 <LSR-011>` - 定义 ``MathError`` 所使用的 ADT 名义类型与字符串表示边界