# 作用与余作用

## 作用 (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 能被安全热替换的根本原因。