feat: add docs website

website/zh-CN/design/composability.md

@@ -0,0 +1,72 @@
+# 可组合性与插件系统
+
+## 组合
+
+编程的本质就是组合。将小的构建块拼装为更大的系统，再将大系统作为块继续拼装——这是从函数到模块到微服务一脉相承的思想。
+
+组合可以分为两种：
+
+- **静态组合**：编译期确定的组合，例如函数调用、模块导入。
+- **动态组合**：运行时确定的组合，例如热更新、插件加载/卸载。
+
+静态组合是逻辑的组合；动态组合为可组合性引入了时间和空间两个新维度。
+
+## 三种可组合性
+
+| 维度 | 定义 | 对应问题 |
+|------|------|----------|
+| **逻辑可组合性** (Logical) | 功能能否被任意拆分和组装 | 接口设计是否正交 |
+| **时间可组合性** (Temporal) | 能否灵活、安全地控制组合的运行时序 | 能否热加载/卸载而不泄漏 |
+| **空间可组合性** (Spatial) | 能否灵活、安全地管理组合的依赖关系 | 依赖缺失时行为是否确定 |
+
+一门编程语言或应用框架越多地使用组合范式，就称它的可组合性越好。
+
+## 传统插件系统的问题
+
+插件系统是动态组合的典型形式。浏览器扩展、IDE 插件、操作系统驱动，都是其实例。然而大多数插件系统并不可靠。
+
+### 不可逆的插件化
+
+以 VSCode 为例：
+
+- 卸载或更新插件时需要重启整个系统。
+- 无法在运行时追踪和回收副作用，导致内存泄漏和非预期的资源占用。
+- 即便提供了 `deactivate` 钩子，也无法强制开发者正确实现清理逻辑。
+
+**根本原因**：未做到时间可组合——系统不知道某个插件产生了哪些副作用、占用了哪些资源。
+
+### 不完全的插件化
+
+- 无法表达插件间的依赖关系，扩展能力受限。
+- 只有外围功能被下放给插件，核心功能依然通过修改主体代码来实现。
+
+**根本原因**：未做到空间可组合——系统缺乏对依赖关系的建模和管理。
+
+## Cordis 的解法
+
+Cordis 同时解决了上述两个问题：
+
+1. **可逆作用** (Revertible Effects) 实现时间可组合性——所有注册自动追踪、自动回收。
+2. **响应式余作用** (Reactive Coeffects) 实现空间可组合性——依赖声明驱动加载顺序。
+
+两者通过**上下文模型** (Context Model) 统一为单一的编程范式：开发者只需通过 `ctx` 调用框架 API，可逆性和依赖管理由框架保证。
+
+## 在 Harness 中的体现
+
+DeepSeek Harness 将 Cordis 的可组合性应用到 Agent 开发领域：
+
+```typescript
+// 一个 Harness 插件天然是可逆的
+export const inject = ['tools', 'llm'] // 空间可组合：声明依赖
+
+export function apply(ctx: Context) {
+  // 时间可组合：注册会被自动追踪和回收
+  ctx.tools.register(defineTool('my-tool', {
+    description: '...',
+    parameters: { /* ... */ },
+    async execute(args) { /* ... */ },
+  }))
+}
+```
+
+插件卸载时，tool 自动注销、事件监听自动移除——无需手动清理。依赖的服务（如 `llm`）消失时，插件自动挂起；恢复时自动重新加载。

website/zh-CN/design/context-model.md

@@ -0,0 +1,129 @@
+# 上下文模型
+
+上下文 (Context) 是 Cordis 将作用与余作用统一的运行时模型。它提供了一种编程范式，允许开发者无心智负担地编写时间、空间可组合的程序。
+
+## 作用上下文 (Effect Context)
+
+当副作用被记录到全局环境时，$\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)$ 也就变成了一个更大的 $\mathcal{C}$。
+
+递归地定义：
+
+$$
+\begin{matrix}
+\mathcal{C}_1=\mathcal{C}_0\times\left(\mathcal{C}_0\to\mathcal{C}_0\right)\\
+\mathcal{C}_2=\mathcal{C}_1\times\left(\mathcal{C}_1\to\mathcal{C}_1\right)\\
+\cdots\\
+\mathcal{C}_{n+1}=\mathcal{C}_n\times\left(\mathcal{C}_n\to\mathcal{C}_n\right)\\
+\end{matrix}
+$$
+
+每一层 $\mathcal{C}$ 包含上一层的状态，同时记录了上一层的副作用。
+
+利用递归类型得到真正的作用上下文：
+
+$$
+\mathcal{C}=\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)
+$$
+
+这就是 Cordis Context 的理论根基：**上下文既是状态容器，又是副作用追踪器。**
+
+## 上下文的派生
+
+当一个插件被加载时，从当前上下文派生出新的上下文实例：
+
+```
+Root Context
+├── Plugin A Context   ← 管理 A 的副作用
+│   └── Sub-plugin Context
+└── Plugin B Context   ← 管理 B 的副作用
+```
+
+- 子级上下文管理插件内部的全部副作用
+- 插件整体作为一个副作用被父级上下文收集
+- 父级 dispose 时，子级先被 dispose（保证依赖逆序）
+
+## 余作用上下文 (Coeffect Context)
+
+余作用由作用产生：
+
+- **提供服务**本身是一种作用——它占用了服务命名空间资源
+- 因此服务的提供被记录在作用上下文中
+- 上下文将作用与余作用关联起来，提供了统一的时间、空间可组合性
+
+```typescript
+// 提供服务 = 一个 effect（占用 ctx.llm 这个 "资源"）
+class LlmService extends Service {
+  // 当此插件卸载时，ctx.llm 被回收（effect 的逆操作）
+  // 所有依赖 llm 的插件因 coeffect 不满足而挂起
+}
+```
+
+## 基于上下文的开发范式
+
+上下文模型提供了两个关键优势：
+
+### 无感性 (Transparent)
+
+框架将领域中的所有方法都封装为 effect 版本。开发者只需调用 `ctx` 上的方法，就能自动获得时间/空间可组合性：
+
+```typescript
+export function apply(ctx: Context) {
+  // 以下每一行都是 effect——卸载时自动逆序回收
+  ctx.on('agent/step-result', validateResult)
+  ctx.tools.register(myTool)
+  ctx.llm.registerAdapter(['my-model'], adapter)
+
+  // 开发者无需知道"可逆作用"的存在
+  // 只需通过 ctx 调用，框架保证一切安全
+}
+```
+
+### 渐进性 (Incremental)
+
+可以逐步将现有框架中的 API 替换为可组合版本，无需一次性重写：
+
+```typescript
+// 第一步：用 ctx.effect 包装遗留 API
+ctx.effect(() => {
+  const legacy = legacySystem.register(handler)
+  return () => legacySystem.unregister(legacy)
+})
+
+// 第二步：在未来将遗留 API 原生改造为 effect
+// 两种方式可以并存
+```
+
+## 在 Harness 中的完整图景
+
+DeepSeek Harness 的运行时是一个 Context 树：
+
+```
+Root Context (Cordis 应用)
+├── dsh-session (提供 ctx.sessions)
+├── dsh-tools (提供 ctx.tools)
+├── dsh-llm (提供 ctx.llm)
+│   └── deepseek-adapter (注册模型适配器)
+├── dsh-agent-loop (提供 ctx.agentLoop)
+├── dsh-bash (提供 ctx.bash)
+│   └── bash-local (本地执行器实现)
+├── dsh-fs (提供 ctx.fs)
+│   └── fs-local (本地 FS 实现)
+├── dsh-system-prompt (提供 ctx.systemPrompt)
+└── Agent Context (由 agents.create() 派生)
+    ├── Agent 自己注册的 tools
+    ├── Agent 的 session
+    └── Subagent Context (进一步派生)
+```
+
+每个节点都是一个 Context 实例。插件加载/卸载、服务出现/消失、Agent 创建/销毁——这一切都在 Context 树上以统一的语义发生。
+
+## 总结
+
+| 概念 | 解决的问题 | Cordis 机制 |
+|------|-----------|-------------|
+| 作用上下文 | 副作用追踪与回收 | `ctx.effect()` / `fiber.dispose()` |
+| 上下文派生 | 副作用的层级隔离 | `ctx.plugin()` 创建子 Context |
+| 余作用上下文 | 依赖的动态管理 | `inject` 声明 + 服务生命周期 |
+| 统一范式 | 开发者无需关心底层机制 | 只需通过 `ctx` 调用 API |
+
+这就是为什么 Harness 能在保持「一切皆插件」的同时，不给插件开发者增加心智负担——**上下文模型把复杂性封装在了框架内部**。

website/zh-CN/design/effects-coeffects.md

@@ -0,0 +1,69 @@
+# 作用与余作用
+
+## 作用 (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 能被安全热替换的根本原因。

website/zh-CN/design/index.md

@@ -0,0 +1,39 @@
+# 系统设计
+
+DeepSeek Harness 建立在 Cordis 微内核之上，采用「一切皆插件」的架构。本节阐述这套设计背后的理论基础和设计哲学。
+
+## 核心思想
+
+Harness 追求三种可组合性的统一：
+
+| 维度 | 含义 | Cordis 对应机制 |
+|------|------|----------------|
+| 逻辑可组合性 | 功能能否自由拆分和拼装 | 插件系统、事件系统 |
+| 时间可组合性 | 运行时能否安全地加载/卸载功能 | 可逆作用、自动清理 |
+| 空间可组合性 | 依赖关系能否被安全地声明和管理 | 服务生命周期、依赖注入 |
+
+这三种可组合性在上下文模型中统一为单一的编程范式。
+
+## 目录
+
+- [可组合性与插件系统](./composability) — 组合的本质，以及传统插件系统为什么不可靠
+- [作用与余作用](./effects-coeffects) — Cordis 效果系统的理论模型
+- [可逆作用](./revertible-effects) — 时间可组合性的形式化定义与证明
+- [响应式余作用](./reactive-coeffects) — 空间可组合性的服务语义
+- [上下文模型](./context-model) — Context 如何将作用与余作用统一
+
+## 设计如何映射到 Harness
+
+| 理论概念 | Harness 中的体现 |
+|----------|-----------------|
+| 可逆作用 | `ctx.tools.register()` 返回 disposer；插件卸载时工具自动注销 |
+| 响应式余作用 | `inject: ['llm']` 声明依赖；LLM 适配器不可用时插件自动挂起 |
+| 上下文派生 | 子 Agent 拥有独立 Context，继承父级服务但有独立生命周期 |
+| Waterfall 事件 | `agent/request` 链式拦截，任一监听器可决定最终请求参数 |
+| Capability seam | bash/fs/web 三层拆分：接口 → 实现 → 模型工具 |
+
+## 进一步阅读
+
+- [插件与生命周期](/zh-CN/develop/framework/) — 实践中的 Fiber 状态机
+- [服务与依赖](/zh-CN/develop/framework/service) — 服务声明与注入
+- [能力的三层拆分](/zh-CN/develop/practice/) — Capability seam 模式

website/zh-CN/design/reactive-coeffects.md

@@ -0,0 +1,90 @@
+# 响应式余作用
+
+响应式余作用 (Reactive Coeffects) 是 Cordis 实现**空间可组合性**的核心机制。
+
+- 将代码中的资源依赖抽象为服务 (service) 的概念
+- 通过运行时生命周期语义，实现自动、安全、高效的资源管理
+
+## 依赖的本质是生命周期
+
+传统的依赖注入（如 Angular DI、Spring IoC）解决的是"怎么拿到依赖"的问题，但忽略了一个关键问题：**依赖是有生命周期的**。
+
+一个数据库连接池可能重启，一个 API 服务可能下线，一个 LLM adapter 可能被热替换。当依赖消失时，依赖者应当如何表现？
+
+- 崩溃？——对长时运行程序不可接受。
+- 继续运行？——可能产生不一致状态。
+- **自动挂起，等待恢复？**——Cordis 的选择。
+
+## 服务与生命周期
+
+Cordis 将程序中的资源依赖抽象为**服务** (service)：
+
+- 任何插件都可以声明自己依赖的服务列表
+- 服务存在明确的生命周期（提供、撤销）
+- 运行时对依赖不满足的插件**等待**，而非拒绝
+- 服务生命周期结束前，依赖该服务的插件**先一步被回收**
+
+```typescript
+// LLM 适配器插件：提供 llm 服务
+export class LlmService extends Service {
+  static inject = ['http']  // 自身依赖 http
+  // 当 http 不可用时，LlmService 自动挂起
+  // 挂起导致 ctx.llm 不可用
+  // 所有 inject: ['llm'] 的插件级联挂起
+}
+```
+
+## 与现有理论的对比
+
+### 与 Comonad 余作用比较
+
+基于 Comonad 的余作用（Petricek 2013）将上下文建模为静态结构，侧重于编译期分析。Cordis 的响应式余作用额外引入了**时序语义**：
+
+- 服务可在运行时出现/消失
+- 依赖关系随之动态建立/解除
+- 效果的生命周期由依赖关系决定
+
+### 与 Grade Algebra 余作用比较
+
+基于 Grade Algebra 的余作用（Gaboardi 2016）用有序半环描述资源的组合规则。Cordis 的服务依赖可以建模为**交换半群**：
+
+- 服务名构成依赖集合
+- 集合并（∪）对应并行依赖
+- 交换律：依赖 A + B ≡ 依赖 B + A（声明顺序无关）
+- 结合律：依赖分组方式不影响语义
+
+但 Cordis 还增加了代数不具备的运行时行为：当集合中的某个服务不可用时，整个依赖集不满足，触发挂起。
+
+## 在 Cordis 中的实现
+
+```typescript
+// 声明依赖
+export const inject = ['tools', 'llm']
+
+export function apply(ctx: Context) {
+  // 到这里时，ctx.tools 和 ctx.llm 一定可用
+  // 如果任一服务消失，此插件自动卸载
+  // 服务恢复后，自动重新执行 apply
+}
+```
+
+服务生命周期变化时的行为：
+
+```
+llm service 可用 → 依赖 llm 的插件 PENDING → ACTIVE
+llm service 消失 → 依赖 llm 的插件 ACTIVE → DISPOSED
+llm service 恢复 → 依赖 llm 的插件重新 PENDING → ACTIVE
+```
+
+## 为什么 Agent 需要响应式余作用
+
+在 Harness 场景下，响应式余作用直接支撑：
+
+| 场景 | 行为 |
+|------|------|
+| LLM adapter 热替换 | 依赖 `llm` 的插件自动挂起/恢复，中间不丢状态 |
+| 按需加载 bash 执行器 | bash tool 只在 `bash` 服务就绪后注册 |
+| 子 Agent 独立服务空间 | 通过 `ctx.isolate()` 隔离服务实例，互不干扰 |
+| 可选能力降级 | `inject: { web: { required: false } }` 允许 web 不可用时继续运行 |
+
+这意味着 Harness 插件开发者无需编写防御性的 "if service exists" 检查——框架保证：当你的 `apply` 被调用时，声明的依赖一定已就绪。

website/zh-CN/design/revertible-effects.md

@@ -0,0 +1,128 @@
+# 可逆作用
+
+可逆作用 (Revertible Effects) 是 Cordis 实现**时间可组合性**的核心机制。
+
+- 在单子作用的基础上增加可逆性约束
+- 提供面向长时运行程序的作用系统
+- 确保程序可以在插件粒度上回到任意状态
+
+## 副作用的封装
+
+现实中的程序需要与各种副作用打交道。假设一个不纯函数：
+
+$$
+f_\text{impure}: \text{X}\to\text{Y}
+$$
+
+我们将所有可能的副作用用类型 $\mathcal{C}$ 封装，函数变为：
+
+$$
+f: \mathcal{C}\times\text{X}\to\mathcal{C}\times\text{Y}
+$$
+
+对于长时运行程序，忽略函数本身的入参和出参，$f$ 属于函数空间 $\mathfrak{F}=\mathcal{C}\to\mathcal{C}$。
+
+## 从幺半群到群
+
+任何函数 $f: \mathcal{C}\to\mathcal{C}$ 都是状态空间到自身的变换。在组合 $\circ$ 下构成**幺半群**：
+
+1. 封闭性：$f\circ g$ 也是 $\mathcal{C}\to\mathcal{C}$
+2. 结合律：$(f\circ g)\circ h=f\circ (g\circ h)$
+3. 单位元：$\text{id}$，使得 $f\circ\text{id}=\text{id}\circ f=f$
+
+如果额外要求每个 $f$ 存在逆元 $f^{-1}$（即副作用可回收），$\mathfrak{F}$ 升级为**群**。
+
+## 副作用都可逆吗？
+
+观察计算机中的副作用模式：
+
+| 操作 | 占用资源 | 逆操作 |
+|------|----------|--------|
+| 打开文件 | 文件描述符 | 关闭文件 |
+| 创建子进程 | 进程号 | 杀死进程 |
+| 监听端口 | 端口 | 取消监听 |
+| 添加回调函数 | 事件槽位 | 删除回调 |
+| 分配内存 | 内存区块 | 回收内存 |
+
+**副作用就是对资源的占用。** 计算机的资源天然设计为可重复使用，因此这些副作用一定是可逆的。
+
+## 追踪和回收副作用
+
+Cordis 通过 $\text{effect}$ 和 $\text{restore}$ 函子追踪和回收逆函数。
+
+### effect 函子
+
+$$
+\begin{array}{}
+\text{effect}&:&
+\left(\mathcal{C}\to\mathcal{C}\right)&\to&
+\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)&\to&
+\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)\\
+\text{effect}&=&f&\mapsto&\left(c, h\right)&\mapsto&\left(f(c), h\circ f^{-1}\right)
+\end{array}
+$$
+
+直觉：执行 $f$ 产生的副作用记入状态 $c$，同时将逆操作 $f^{-1}$ 追加到回收链 $h$ 中。
+
+### 同态性证明
+
+$\text{effect}$ 是从 $\mathcal{C}\to\mathcal{C}$ 到 $\mathcal{C}\times(\mathcal{C}\to\mathcal{C})\to\mathcal{C}\times(\mathcal{C}\to\mathcal{C})$ 的同态：
+
+$$
+\begin{aligned}
+\text{effect}\ (f\circ g) \left(c, h\right)
+&=\left((f\circ g)(c), h\circ (f\circ g)^{-1}\right)\\
+&=\left(f(g(c)), h\circ g^{-1}\circ f^{-1}\right)\\
+&=\left(\text{effect}\ f\right)\left(g(c), h\circ g^{-1}\right)\\
+&=\left(\text{effect}\ f\right)\circ\left(\text{effect}\ g\right) \left(c, h\right)
+\end{aligned}
+$$
+
+这意味着：组合两个操作后再追踪 = 分别追踪后再组合。副作用追踪与执行顺序无关。
+
+### restore 函子
+
+$$
+\begin{array}{}
+\text{restore}&:&
+\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)&\to&
+\mathcal{C}\times\left(\mathcal{C}\to\mathcal{C}\right)\\
+\text{restore}&=&\left(c, h\right)&\mapsto&\left(h(c),\text{id}\right)
+\end{array}
+$$
+
+直觉：将回收链 $h$ 应用到当前状态，一次性回收所有已追踪的副作用。
+
+## 在 Cordis 中的实现
+
+理论映射到 API：
+
+| 数学概念 | Cordis API | 说明 |
+|----------|-----------|------|
+| $\text{effect}(f)$ | `ctx.effect(() => { ...; return dispose })` | 注册副作用并返回清理函数 |
+| $\text{restore}$ | `fiber.dispose()` | 执行 Fiber 的整个回收链 |
+| $f^{-1}$ | dispose 返回值 / cleanup 函数 | 逆操作 |
+
+```typescript
+export function apply(ctx: Context) {
+  // effect: 创建资源，返回其逆操作
+  ctx.effect(() => {
+    const server = startServer(8080)     // f: 占用端口
+    return () => server.close()          // f⁻¹: 释放端口
+  })
+
+  // 框架 API 内部已封装 effect
+  ctx.on('event', handler)               // 内部: effect(addListener, removeListener)
+  ctx.tools.register(myTool)             // 内部: effect(addTool, removeTool)
+}
+// 当此插件被卸载时，restore 自动按逆序执行所有 f⁻¹
+```
+
+## 为什么 Agent 需要可逆作用
+
+在 Harness 场景下，可逆作用直接支撑：
+
+- **热替换 LLM 适配器**：卸载旧适配器（回收注册）、加载新适配器，无需重启
+- **动态 tool 管理**：根据对话上下文动态添加/移除 tool，不泄漏
+- **子 Agent 生命周期**：子 Agent 完成后，其注册的所有临时 tool 和监听器自动清理
+- **优雅关闭**：进程退出时所有插件按依赖逆序 dispose，确保资源完全释放