你有没有遇到过这种情况：VSCode装了个插件，用完想卸载，结果发现根本卸载不干净，非得重启整个编辑器不可？
这不是VSCode的锅，这是几乎所有插件系统的通病。你以为点了"禁用"按钮就万事大吉，实际上插件在内存里注册的定时器、打开的文件句柄、订阅的事件监听，可能还在悄悄运行。真要干净地清除，唯一靠谱的办法是重启整个进程,把所有状态推倒重来。
这篇来自北京大学和DeepSeek联合团队的论文,想解决的就是这个看似简单实则棘手的问题：能不能让软件系统里的组件,像插拔U盘一样,说加载就加载,说拔出就彻底拔出,不留一点痕迹？
问题到底难在哪
先说个具体数字。研究者调查了VSCode插件市场里安装量最高的100个插件,发现87个包含可执行代码,这意味着一旦激活,想要真正卸载它们就必须重启整个扩展宿主进程,而这会牵连所有正在运行的其他插件。
这还只是"卸载干净"这一个维度的问题。另一个维度是"插件之间怎么互相依赖"。同样是这100个热门插件,只有7个真正声明了对其他非内置插件的依赖关系。为什么这么少？因为VSCode给插件开放的接口大多是命令、视图这类固定的"插座",插件之间想要互相调用,官方提供的机制是通过一个叫`exports`的对象,但这个对象的类型是任意的（`any`）,也就是说,你调用一个依赖的插件提供的功能,类型系统完全帮不上忙,出了问题只能靠运气排查。
这两个问题,论文把它们提炼成了两个正式的学术概念。
**时间维度上的可组合性**：一个组件被移除后，它对整个系统环境造成的所有修改都必须被完整、安全地撤销。
**空间维度上的可组合性**：组件之间要能声明、发现并解决彼此的依赖关系，而且这个过程得是结构化、可验证的，不能是"能跑就行"的野路子。
这两个维度在静态场景下其实早就被解决过了。程序设计里的作用域机制、RAII（一种C++资源管理技巧，对象销毁时自动清理资源）这类手法能处理编译期就确定的资源释放；模块导入解析能处理写死在代码里的依赖关系。
但一旦进入"运行时动态加载"的世界，事情就变得棘手起来：组件是运行时才出现、运行时才消失的，它造成的影响没法用一个固定的代码作用域去框住；依赖关系也不是编译时就写死的，可能这一秒还在，下一秒就被换成了别的实现。
工业界现在普遍采用的解决方案，其实是一种"绕过问题"的思路：用操作系统的进程来实现"时间可组合性"（进程崩了就杀掉重启），用容器编排系统（比如Kubernetes）来实现"空间可组合性"（服务挂了编排系统会重新调度）。
这套办法能用，但代价不小。每次进程重启，缓存、连接、正在进行到一半的计算全部作废，重建起来动辄几秒到几分钟；为了在这段真空期不影响服务，还得多备几个副本，这是拿资源换稳定性。而在容器层面做依赖管理，天然没法表达两个共享同一个地址空间的组件之间的依赖，而且组件间调用被迫走网络，本来一次函数调用就能搞定的事，现在要经过序列化、网络传输、反序列化。
**这就好比你想给家里的电灯换个灯泡，结果被要求先把整栋楼断电重启一遍。**
灯泡（单个组件）明明是个很小的单元，但因为系统没法精细控制到灯泡这一级，只能靠"断电重启整栋楼"（重启进程/容器）这种粗暴手段来保证安全。论文的核心动机，就是想找到一种精细到组件级别的机制，让你真的能像换灯泡一样，只处理需要处理的那一小块。
从类型系统的老概念说起：效应与协效应
要理解这篇论文怎么解决问题，得先绕个弯，回顾两个编程语言理论里的经典概念。
**效应系统（Effect System）**：给程序的类型标注上"这段代码可能产生哪些副作用"的信息，让编译器能推理一段代码到底会不会修改外部状态。
**协效应系统（Coeffect System）**：跟效应系统反过来，它标注的是"这段代码需要环境提供什么"，也就是程序对外部资源、权限的依赖。
打个比方，效应回答的是"这段代码会往世界里泼多少水"，协效应回答的是"这段代码需要世界预先准备好多少水"。
效应系统的历史可以追溯到上世纪80年代末Lucassen和Gifford的工作，后来Moggi用范畴论里的"单子"（monad）给效应建了个数学模型，Wadler把这套东西在Haskell里发扬光大。协效应这边则是Petricek等人在2013年提出的，用"余单子"（comonad，单子的对偶概念）来刻画程序对上下文的依赖。
问题在于，这些经典理论几乎全是"静态"的：效应在编译期被追踪，协效应在编译期被验证，作用域是写死在程序文本里的。而动态组合场景需要的是运行时的保证，需要在组件随时可能加入和离开、依赖环境随时可能变化的情况下，依然维持这些保证。
论文的核心思路是：把效应和协效应从"编译期的类型标注"改造成"运行时能操作的实体"。这个转变听起来抽象，但接下来的具体设计会让你明白它到底意味着什么。
可撤销的效应：每次修改都自带"后悔药"
论文对"效应"的重新定义非常直接：一个效应不再只是"对状态的一次改动"，而是一个函数，输入当前状态，输出两样东西：修改后的新状态，以及一个能把状态改回去的"逆函数"。
用数学符号写就是 Γ → Γ × (Γ → Γ)，翻译成人话：给我当前的上下文（Γ代表整个系统的状态环境），我不仅告诉你改完之后长什么样，还附带一把钥匙，用这把钥匙就能把刚才的改动撤销掉。
这个设计的关键在于，逆函数不是事后靠人脑去写的补丁，而是在执行效应的那一刻，就必须同时交出来的东西。
论文引入了一个叫"效应上下文"（effect context）的结构，记作 ?Γ，本质上是一对值：当前的状态，加上一个"累加器"（accumulator）。这个累加器就是迄今为止所有已执行效应的逆函数，按照后进先出（LIFO）的顺序组合在一起。
**这就像你去餐厅点了一连串菜：先点了汤，又追加了主菜，又加了甜点。**
如果后来要取消订单，正确的做法不是随便退一个菜，而是按照点单的相反顺序一样一样撤掉：先退甜点，再退主菜，最后退汤。为什么要反着来？因为如果先撤了汤，而汤的价格可能影响到了后面主菜的套餐优惠，你直接退汤就会让账目乱掉。累加器保证了这种"先进后出"的撤销顺序，任何时候点了新东西，都是往这个撤销清单的最前面插入一条新记录，撤销时永远从最新的那条开始处理。
论文接着证明了一系列数学性质，其中最核心的一条叫"可靠性不变量"（soundness invariant）：只要每一步效应及其逆函数配对正确，那么从初始状态开始，无论中间执行了多少次效应，只要按累加器规定的顺序全部撤销一遍，系统一定能精确地回到最初的状态。
不过这里有个很现实的限制条件：这种"精确回到最初状态"其实是个理想化的说法。现实中，比如你调用`malloc`申请了一块内存，`free`释放它的时候并不会把堆的物理布局恢复原样；再比如生成了一个唯一ID，撤销之后再生成一个新ID，肯定不是原来那个。
**这就好比你在酒店办了退房手续，房间钥匙确实收回来了，但今晚睡过的那张床垫，物理层面上已经被压出了印子，退房这个动作本身不负责把床垫恢复到"从未有人睡过"的状态。**
论文对此的处理方式是引入"观察等价"（observational equivalence）的概念，只要求"从外部可观察行为上看不出差别"，而不是要求物理比特位完全一致。这是个很务实的让步，承认完全的时间旅行式撤销在真实系统里做不到，但只要外部看起来一样，就足够安全了。
反应式协效应：依赖关系自动感知变化
解决完"怎么撤销"，接下来是"怎么处理依赖"。
论文把依赖关系建模成一个键值表，叫协效应上下文，记作Σ，本质上是从"依赖的名字"（比如"数据库连接"）到"对应值"的一个部分函数（部分函数意味着不是所有键都有值，这也正好对应了"这个依赖此刻可能还没就绪"这种状态）。
每个组件会声明一个协效应规格，也就是它需要哪些依赖（比如"我需要一个数据库连接"和"我需要一个日志服务"）。系统的核心机制是：每当协效应上下文发生变化（某个依赖被提供了，或者被撤走了），系统会拿这个变化跟每个组件的声明去比对，判断出三种情况之一。
**激活**：之前这个组件的依赖没有全部满足，现在全满足了，该激活这个组件了。
**去激活**：之前依赖都满足，现在有个依赖没了，该把这个组件停掉了。
**中立**：这次变化跟这个组件毫无关系，不用管。
这个机制被称为"反应式"（reactive），因为它不是靠组件自己去轮询检查"我的依赖还在不在"，而是每次环境发生变化时，系统主动去通知、去分类、去驱动组件的激活和停用。
**这有点像你手机上的自动化脚本：一旦检测到你连上了家里的WiFi，就自动打开空调；一旦检测到WiFi断开，就自动关灯。**
你不需要每隔几秒钟手动检查一次"我现在在不在家里的WiFi范围内"，系统会替你盯着这个变化，一旦发生就立刻触发对应的动作。如果没有这套反应式机制，每个组件都得自己写一套轮询逻辑去检查依赖状态，不仅低效，而且极易出现"依赖已经没了，但组件还在傻乎乎地用一个失效的引用"这种bug。
论文还进一步扩展了这个基础模型，加入了两个精细化机制。
**协效应隔离**：允许同一个依赖名字，在不同的上下文里解析成不同的值。比如多租户系统里，不同租户访问"数据库连接"这个名字，实际拿到的是各自独立的数据库实例。这就好比公司里不同部门都叫"前台"，但你去财务部前台和去人事部前台，找的其实是完全不同的两个人，只是"前台"这个称呼一样。
**协效应拦截**：允许在依赖被访问时附加一层元数据，实现权限控制这类横切逻辑，而不需要改动依赖本身的代码。比如给一个"文件系统"依赖挂上"只读"标签，某个组件访问它的时候就自动被限制成只能读不能写，这个限制是挂在访问路径上的，跟被访问的文件系统对象本身无关。
统一上下文：把效应和协效应装进同一个容器
到这里，论文已经分别给"撤销效应"和"感知依赖"各自建了一个数学模型。但这两套东西如果各管各的，组件之间还是可能互相干扰。论文接下来做的事情，是把这两个模型合并进一个统一的容器，叫作"上下文范式"（context paradigm）。
具体做法是把效应上下文和协效应上下文融合成一个递归定义的类型：
Γ∞ ? 一个三元组，包含（当前状态，能撤销这一层效应的累加器，携带依赖信息的协效应上下文）
这个定义是递归的，意味着你可以套娃：一个上下文里嵌着另一个上下文，就像组件可以拥有子组件一样，形成一棵树状的控制结构。父级上下文汇总管理所有子级组件的效应，卸载父组件的时候，子组件的效应也会跟着被撤销，但不会波及树上的其他分支。
论文还引入了一个很关键的约束，叫"上下文中介"（context mediation）：组件跟外部世界的所有交互，必须全部经过这个统一的上下文来完成，不能有任何绕过去的路径。
具体表现为，每个协效应的"键"不仅关联一个值类型，还关联一组"允许对这个值执行的操作"。比如一个"计数器"依赖，可能只暴露"加一"和"读取当前值"这两个操作，而不是把内部的整型变量直接暴露出来让你随便改。
**这就好比银行不会把金库钥匙直接给你，而是只给你一个"取款机操作界面"：你能存钱、能取钱，但你没法直接搬箱子进金库改数字。**
如果没有这层约束，任何组件都可以随意读写共享状态的任何角落，那"撤销效应"和"追踪依赖"这两套机制就形同虚设，因为总有漏网之鱼绕开了这套记录系统。
正是因为所有交互都被强制收拢到这个统一入口，论文才能在此基础上定义出一种叫"观察等价"的关系：如果两个组件的效应互相之间没有可观察的干扰，那么它们的执行顺序可以任意调换，结果保持不变。这个性质叫"效应独立性"，是让整个系统能安全地并发处理多个组件加载卸载的数学基础。
独立性：为什么组件之间可以互不干扰地并发操作
这一部分是全文数学味最浓、但也是支撑整个系统"真正好用"的关键论证。
论文先定义了什么叫两个效应"独立"：一个效应能造成的所有状态变换，跟另一个效应能造成的所有状态变换，两两之间都能互相交换顺序而不改变最终结果。
如果两个效应各自操作的是完全不相交的键，那这个独立性几乎是显然的，你动你的抽屉，我动我的抽屉，谁先谁后都一样。
真正有意思的是那种"缠绕"（entangled）的情况：一个组件提供的键正好是另一个组件声明依赖的键。这时候两个组件之间显然不是无关的，一个是供货方，一个是用货方。论文证明，只要这个键上发生的所有操作满足"可交换性"（commutativity），也就是不管操作顺序如何，最终留下的状态在外部观察者看来是一样的，那么整个系统依然可以保证独立性。
这里有个特别精彩的设计决策，论文管这个叫"表明立场的接口设计"。举个例子：一个内存分配器，如果它对外暴露的接口只是"给我分配一块内存，返回一个句柄"，而这个句柄具体的数值（内存地址）不被任何调用者比较或依赖，那么"先分配A再分配B"和"先分配B再分配A"这两个操作序列，在外部观察者眼里是完全等价的（因为没人关心具体地址是多少，关心的只是能不能正常存取）。这种情况下，这个分配器的操作就是可交换的。
但如果这个分配器的接口设计成"必须返回当前最小的可用地址编号"（POSIX里的`open`系统调用就是这样，规定必须返回最小可用的文件描述符），那么分配顺序就会影响返回的具体编号，两次分配的顺序就变得不可交换了。
**这就像图书馆借书系统。**
如果借书证只记录"你借了这本书"，不关心具体分配给你哪个座位号，那么两个人先后来借书，谁先谁后对结果毫无影响，两种顺序看起来完全一样。但如果借书系统非要按照"先来后到"精确分配座位号1、2、3，那么两个人的借书顺序就会实实在在影响到谁拿到哪个座位号，顺序就不能随便换了。
论文引用了一篇叫"可扩展可交换性规则"（scalable commutativity rule）的相关工作，指出POSIX接口里`mmap`可以返回任意可用地址（因此可交换），而`open`必须返回最小可用描述符（因此不可交换），这个设计上的细微差异，直接决定了系统能不能在多核处理器上无锁地并行处理这些调用。这篇论文把这套思路直接用来推导"组件的哪些依赖操作可以安全地被并发、乱序处理"。
这个洞察带来的实际好处是：接口设计者只要愿意"少暴露一些细节"，就能主动把一个原本不可交换的操作，变成可交换的，从而换来更好的并发性和可组合性。这不是免费的午餐，代价是调用方能拿到的信息变少了，但很多时候调用方根本不需要那些细节。
一整套运作规则：组件的生命周期
有了效应和协效应这两套底层机制，论文接下来构建了一个完整的"演算系统"（calculus），用九条形式化规则描述一个组件从出生到死亡的完整生命周期。
组件被建模成一个三元组：它声明了哪些依赖（协效应规格），它对外提供了哪些能力（协效应提供），以及它实际执行的效应函数（做了哪些具体动作）。
而组件的每一次具体运行实例，叫作"纤维"（fiber），这个词借用了并发编程里"轻量级执行单元"的比喻。每个纤维携带自己的生命周期状态，一共有四种：
**未激活（Inactive）**：还没跑起来，等着依赖满足。
**加载中（Reloading）**：正在执行效应函数，一步一步安装自己的功能。
**已激活（Active）**：已经跑起来了，正在对外提供服务。
**卸载中（Unloading）**：正在撤销之前安装的效应，把自己的痕迹一点点清理干净。
论文用一张状态机图描述了这四个状态之间的流转，九条规则分为两类：编排规则（orchestration rules，是外部指令，比如"插入这个组件"或"移除那个组件"）和生命周期规则（lifecycle rules，是系统自己根据依赖状态变化自动触发的）。
这里有个非常巧妙的设计，叫"卫兵条件"（guard），专门用来解决一个棘手的时序问题：如果A组件依赖B组件，B组件要下线了，能不能直接把B撤了？
不行。论文的规则要求：B在正式撤销自己的效应之前，必须先等所有依赖它的消费者A完成自己的下线流程。这个等待用一个叫`relied`（被依赖着）的谓词来判断：只要还有别的已激活组件把某个键解析到B身上，B就不能真正撤销，只能先停止提供新服务，进入"卸载中"状态挂起等待。
**这就像一栋写字楼要拆除，物业不会直接把电闸拉了，而是先贴出通知，等所有租户搬完东西、办完退租手续之后，才真正切断水电、开始拆除。**
如果不这样做，直接一刀切拉闸，正在办公的租户（依赖B的消费者A）可能正在收拾东西（执行自己的卸载逻辑，比如把数据库连接归还给连接池），结果发现水电（B提供的服务）说没就没了，收拾到一半的东西就废了。
论文严格证明了这个"卫兵条件"不会导致死锁：因为一旦B开始进入卸载流程，它就会立刻从"可用服务列表"里消失，所有依赖它的消费者A也会同步检测到这个变化，从而自己也开始卸载，形成一条连锁反应，最终必然会走到B可以安全撤销的那一刻。
三个必须证明的核心定理
论文接下来花了大量篇幅证明这套系统的正确性，核心是三个定理。
**保序性（Ordering）**：一个组件只有在它所有声明的依赖都被满足的情况下才能开始激活；而且只要这个组件成功激活了，它所依赖的那个提供者，在整个消费周期内是不会消失的，一定要等消费者卸载完才轮到提供者卸载。
**进展性（Progress）**：只要系统还没达到"静止"状态（也就是所有组件都稳定在了它们该待的状态），就一定还有规则可以继续执行，不会卡死。而且论文证明了，只要依赖关系图里不存在循环（比如没有"A依赖B，B又依赖A"这种死循环），整个系统在有限步骤内必然会收敛到静止状态。
**汇聚性（Confluence）**：这是全文最有实际工程价值的一条定理。它说的是，不管这套动态加载卸载的过程走了多少种不同的调度顺序，只要最终达到静止状态，得到的系统状态跟"把最终需要激活的那些组件，按照依赖顺序，从头开始加载一遍"得到的状态是完全一致的（在观察等价的意义上）。
**这个汇聚性定理的意义，打个比方，就像你在乐高积木上不管是先搭地基再搭墙，还是零零散散今天加一块明天减一块，只要最后搭出来的成品长得一样，中间的施工顺序其实无关紧要。**
如果没有这条定理，一个动态热更新过的系统，跟一个从头静态部署的系统，理论上可能会出现"看起来一样但底层状态其实有细微差异"的隐患，这种隐患极难排查，往往要跑到生产环境很久之后才会暴露。有了汇聚性保证，运维和开发人员可以完全放心地对系统做增量式的、渐进式的重新配置，而不用担心"是不是应该重启一下更保险"这种心理负担。
落地实现：Cordis框架和真实世界的Koishi
理论讲完了，论文的第二部分把这套模型实现成了一个叫Cordis的开源框架，用TypeScript编写。
Cordis的核心库里，效应追踪的实现方式是一个叫`ctx.effect`的原语，所有对上下文的修改都必须通过它来完成。协效应这边则对应`ctx.get`和`ctx.set`两个操作，配合一个反应式通知机制（`notify`函数），一旦某个键的绑定发生变化，就自动扫描所有声明了该键的组件，重新计算它们的激活状态。
Cordis还额外实现了几个理论篇幅之外但工程上很实用的扩展。
**异步性支持**：真实系统里，效应的执行往往是异步的（比如要等一个网络请求返回），论文的理论模型假设每一步都是瞬间完成的同步操作，实现层面通过"惯性"（inertial）语义补上了这一块：一旦一个组件开始了加载或卸载的过渡，即使中途依赖状态又变了，这个过渡也会先跑完，不会被半路打断。
**失败处理**：如果一个组件在加载过程中抛出异常（比如尝试绑定的端口已被占用），系统会把这次加载当作一次失败的卸载来处理，撤销已经执行的部分效应，把错误记录在这个组件身上，但不会波及它的兄弟组件或父组件。
**热模块替换（HMR）**：这是开发体验层面很实用的功能。当你修改了源代码，Cordis能够精确判断出哪些模块真正受到了影响（通过分析模块导入关系图），只重新加载那一小撮受影响的模块，而不用重启整个应用。整个过程还带事务性保证：如果重新加载过程中出错（比如改出了语法错误），系统会自动回滚到修改前的状态，不会让应用停留在一个"半加载"的诡异中间态。
论文用一个叫Koishi的真实开源聊天机器人框架作为案例研究，这个项目已经运行了四年，积累了超过4000个社区贡献的插件。这个规模本身就说明了这套架构在实际生产环境里是站得住脚的，不是纸上谈兵。
Koishi的一个典型场景是：即时通讯适配器（对接微信、Discord等平台）作为提供者，功能性插件声明对这些适配器的依赖。当你在运行时切换存储后端，或者重新连接一个断掉的适配器，系统只会重新激活那些真正受影响的插件，其他插件安然无恙。而且这套依赖关系是完全跨作者协作的，插件A的作者和插件B的作者素不相识，唯一的协作方式就是通过声明好的协效应键名，各自约定俗成。
不过论文也很坦诚地指出了这个案例研究的局限：证据全部来自单一生态系统、单一编程语言，没法把这套范式本身的优势和TypeScript这门语言的特性、或者Koishi这个具体领域的特殊性完全区分开来。这是个观察性的存在性验证，不是严格的对照实验，具体量化这套抽象到底能带来多少开发效率提升，还是未来的工作。
边界之外的世界：这套系统管不到的地方
论文最后专门用一整节讨论了"系统边界"（system boundary）的问题，这一点我觉得特别值得展开说说，因为它诚实地划清了这套理论能力的边界。
一个位置要能被"完整撤销"，必须同时满足两个条件：系统能独占地修改它，而且能把修改前的状态记录下来以便还原。只要这两个条件有一个不成立，这个操作在效应模型里就只能被当作一个"什么都不做"（identity）的空操作，既不会被追踪，也不会被撤销。
论文把这类跨出边界的操作分成两个阶段。
**获取阶段（acquisition）**：比如`open`打开一个文件描述符，这个描述符本身作为一条记录留在系统内部，`close`就能撤销它。
**发射阶段（emission）**：比如`write`往这个文件描述符里写数据，数据一旦写出去，就流向了系统控制不到的外部世界，这个动作本身是没法被撤销的。
**这就好比你往邮筒里投了一封信。**
投递这个动作本身（获取阶段）可以被记录，你知道自己投了信，理论上你还没投递之前可以反悔把信收回来。但一旦信真的塞进了邮筒（发射阶段），你没法把信从邮政系统里追回来，这个动作已经越过了你能控制的边界。
论文提出了两种应对这种"越界效应"的思路：一种是"延迟提交"，也就是先不真的往外发送，等确认这次操作要保留下来了再真正发出去；另一种是"补偿动作"，允许写一个不完全对称但效果上抵消原操作的补偿操作，比如"退款"来抵消"扣款"，而不是要求真的把钱变回没扣之前的那个具体状态。这种补偿式的撤销，跟严格的"逆函数撤销"相比，只保证在一个更宽松的等价关系下达到一致，代价是相应的数学证明也得重新做一遍，论文明确指出这块的证明并没有自动继承前面章节的结论。
这一节让我觉得，论文的作者们没有假装自己解决了一个"万能撤销"的终极问题，而是很清楚地标出了：这套理论只对"系统边界之内"的操作提供强保证，边界之外的世界，永远需要额外的、场景相关的应对策略。
Q&A
Q1：什么是效应上下文和协效应上下文？
A：效应上下文（?Γ）是论文用来追踪程序副作用的核心结构，包含当前状态和一个能撤销所有已执行效应的累加器函数。协效应上下文（Σ）则是一张记录组件间依赖关系的键值表，每个组件声明需要哪些键，系统据此自动激活或停用组件。两者结合起来，就是论文提出的"统一上下文"（context paradigm），所有效应和协效应操作都必须通过它来完成。
Q2：Cordis框架和Koishi是什么关系？
A：Cordis是这篇论文提出的开源元框架，实现了论文里的效应追踪和协效应解析理论。Koishi是一个基于Cordis构建的真实生产级聊天机器人应用框架，已经运行四年，累计有超过4000个社区贡献的插件。论文用Koishi作为案例研究，验证Cordis这套动态组合理论在真实、大规模、多人协作场景下是否站得住脚。
Q3：为什么VSCode插件卸载不干净，要重启才能清除？
A：因为VSCode的扩展系统没有提供在运行时撤销一个插件所有副作用的机制。插件激活后注册的事件监听、定时器等状态会一直留在共享的扩展宿主进程里，`deactivate`钩子只是进程终止时的收尾回调，不能实现真正的实时移除，所以调查显示热门插件里87%都需要重启才能彻底卸载干净。
