你有沒有遇到過這種情況：VSCode
裝了個插件，用完想卸載，結果發現根本卸載不乾淨，非得重啟整個編輯器不可？
這不是VSCode的鍋，這是幾乎所有插件系統的通病。你以為點了"禁用"按鈕就萬事大吉，實際上插件在內存里註冊的定時器、打開的文件句柄、訂閱的事件監聽，可能還在悄悄運行。真要乾淨地清除，唯一可靠的辦法是重啟整個進程,把所有狀態推倒重來。
這篇來自北京大學和DeepSeek聯合團隊的論文,想解決的就是這個看似簡單實則棘手的問題：能不能讓軟體系統里的組件,像插拔隨身碟一樣,說加載就加載,說拔出就徹底拔出,不留一點痕跡？
問題到底難在哪
先說個具體數字。研究者調查了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%都需要重啟才能徹底卸載乾淨。
