70 lines
3.1 KiB
Markdown
70 lines
3.1 KiB
Markdown
# 作用与余作用
|
|
|
|
## 作用 (Effects)
|
|
|
|
Effects 是程序中对系统状态或外部环境产生影响的操作：I/O、状态修改、资源占用等。
|
|
|
|
学术界对作用有两种主要建模方式：
|
|
|
|
### 单子作用 (Monadic Effects)
|
|
|
|
- 通过单子 (monad) 将副作用封装为类型安全的计算链。
|
|
- 提供 `return`（纯值注入）和 `bind`（链式组合）两个基本操作。
|
|
- 以纯函数式的方式处理带有副作用的计算。(Moggi 1991, Wadler 1992)
|
|
- 代表语言：Haskell (IO Monad)、Rust (Result/Option)
|
|
|
|
### 代数作用 (Algebraic Effects)
|
|
|
|
- 允许在函数中"抛出"一个 effect，在调用栈的更高层次"捕获"并处理。
|
|
- 类似异常处理，但更通用——处理后可以恢复执行。
|
|
- 代表语言：Koka、Eff、OCaml 5+ (Kiselyov 2018, Kawahara 2020)
|
|
|
|
## 余作用 (Coeffects)
|
|
|
|
Coeffects 是程序执行时依赖的上下文信息：环境变量、系统资源、外部服务等。
|
|
|
|
- Coeffects 是 effects 的对偶 (dual) 概念，通常通过余单子 (comonad) 建模。(Petricek 2013, 2014; Brünnler 2014)
|
|
- 更前沿的理论将带有资源的上下文建模为 **graded algebra**（有序半环加最大元）：
|
|
- 加法 = 并行组合；0 元 = 无资源
|
|
- 乘法 = 串行组合；1 元 = 单位资源
|
|
- 序 = 资源约束；最大元 = 无限资源
|
|
- (Breuvart 2015, Gaboardi 2016, Dal Lago 2022)
|
|
|
|
## 现有理论的不足
|
|
|
|
这些理论主要面向**静态分析**和**短时程序**：
|
|
|
|
1. **缺乏运行时追踪**：类型系统能标记副作用的存在，但无法在运行时追踪和回收。对长时运行程序（服务端、Agent），这意味着资源泄漏不可避免。
|
|
|
|
2. **缺乏动态性**：面向编译期分析，无法处理运行时的加载/卸载需求。
|
|
|
|
3. **崩溃而非降级**：类型不满足时直接拒绝编译或运行时崩溃，而长时运行程序更希望安全降级——挂起不满足依赖的部分，而非停止整个系统。
|
|
|
|
## Cordis 的突破
|
|
|
|
Cordis 选择了不同的路径——在运行时层面解决可组合性问题：
|
|
|
|
| 现有理论 | Cordis 方案 |
|
|
|----------|-------------|
|
|
| 类型标记副作用 | 运行时追踪并自动回收副作用 |
|
|
| 编译期拒绝 | 运行时挂起/恢复 |
|
|
| 面向短时程序 | 面向长时运行程序设计 |
|
|
|
|
这由两个互补机制实现：
|
|
|
|
- **[可逆作用](./revertible-effects)** — 将副作用形式化为可逆的群操作
|
|
- **[响应式余作用](./reactive-coeffects)** — 将依赖建模为具有生命周期的服务
|
|
|
|
## 在 Agent 开发中的意义
|
|
|
|
对 DeepSeek Harness 而言，作用/余作用模型直接支撑了以下能力：
|
|
|
|
| 作用 (Effect) | 余作用 (Coeffect) |
|
|
|---------------|-------------------|
|
|
| 注册一个 tool | 依赖 tool registry 服务 |
|
|
| 注册一个 LLM adapter | 依赖 LLM 服务接口 |
|
|
| 监听 session 事件 | 依赖 session 服务存在 |
|
|
| 启动子进程 | 依赖 bash executor 实现 |
|
|
|
|
每一个 effect 都可逆（tool 可注销、adapter 可移除）；每一个 coeffect 都有生命周期（服务消失则依赖者挂起）。这就是 Agent 能被安全热替换的根本原因。
|