💻 computer science

You may implement this later: Cofunctors as partial implementations

本文提出将共函子（或逆函子）解释为一种部分实现，其将特定的后端选择（例如数据表示和算法）延迟到运行时，并根据系统状态进行决策。

原作者： Vincent Wang-Maścianica

发布于 2026-08-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Vincent Wang-Maścianica

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在软件工程的世界里，构建一个系统往往感觉就像在组装一台复杂的机器，在拧下第一颗螺栓之前，每一个齿轮都必须被选定。工程师经常面临一个困境：他们需要设计程序的整体结构，例如数据库或网络服务，但目前还无法决定具体的细节，比如使用哪种存储引擎或如何处理数据复制。处理这种不确定性的传统方法通常是在开始时就为整个系统锁定一组特定的选择，或者等到最后时刻才填补空白。这创造了一个僵化的过程，使得前进的路径在目的地完全清晰之前就已经固定了下来。挑战在于寻找一种构建能够进化的系统的方法，让早期做出的决策能够自然地塑造后续可用的选项，而不必强迫程序员过早地做出最终方案的承诺。

牛津大学的一位研究人员提出了一种思考这一问题的新方法，使用一个被称为“余函子”（cofunctor）的数学概念来描述软件如何分阶段构建。其核心思想是将软件系统视为一个不断变化的义务与选择的集合，而非一个完成的成品。想象一张房屋的设计蓝图，它始于一个基本轮廓。随着建筑师增加一个新房间，蓝图并不仅仅是变大了，它还会更新所需的材料清单。如果建筑师决定增加二层，蓝图可能现在需要一个更坚固的地基，这是一个在房屋还是单层时并不相关的选择。这种新方法允许工程师在设计过程中携带这些不断演进的清单，确保每一项新决策都与之前的决策相兼容，同时仍为后续细节留出空间。

论文指出，现有的管理软件配置的工具往往过于僵化。它们通常要求在最开始就定义一组全局参数，这意味着如果开发过程中出现了新需求，系统无法轻易适应。例如，选择以特定方式存储数据可能会在稍后迫使做出关于如何跨不同服务器进行数据复制的决策，但标准方法难以动态地将这两个决策联系起来。作者建议，通过将软件系统视为一种“部分实现”（partial implementation），即系统的当前状态决定了接下来的可用选择，我们可以创建一个更灵活的工程过程。这不仅仅是延迟决策，而是通过构建系统，使得做出一个决策的行为能自然地更新下一个决策的菜单。

为了证明这一点，作者使用了数据存储系统的例子。最初，系统可能仅仅被定义为一个存放数据的地方。在这个阶段，工程师尚未决定是使用本地数据库、远程服务还是特定的文件格式。随着设计的推进，工程师可能会增加一个要求，即数据必须具有持久性，这意味着它必须在掉电后依然存在。这一新需求更新了系统的状态，引入了关于耐久性的新选择。随后，如果工程师决定为了安全起见将数据复制到多个位置，系统会再次更新。这第二次变化可能会引入一个事务协议的要求，而这是一个在系统仅作为简单存储时并不存在的细节。这种方法的妙处在于，系统会自动检查冲突。如果工程师选择了一个无法处理事务的简单文件格式，系统会在添加复制需求时立即标记此冲突，而不是等到代码编写完成并发生故障时才发现。

研究人员展示了这种方法可以创建“可执行迁移计划”。该系统不仅是写下一份需求清单，还可以生成一个逐步计划，说明如何将一个基础存储器转化为一个复杂的、经过复制的存储器。这个计划可以分阶段构建，其中每一步都针对系统的当前状态进行验证。如果某个步骤被跳过或顺序错误，系统可以检测到错误。例如，一个在创建持久化存储之前就尝试进行数据复制的计划会被拒绝，因为必要的基石尚不存在。这确保了最终系统是建立在坚实的逻辑路径之上的，其中每一次变化都与之前的变化历史保持一致。

一个关键发现是，这种方法并不要求工程师预先列出系统所有可能的未来状态。在许多传统方法中，人们必须预先定义所有可能的配置，这往往会导致选项的“组合爆炸”，令人应 overwhelming（难以应付）。在这里，系统只追踪当前活跃的义务。随着新需求的增加，新的选择会出现；随着旧需求的满足，它们也会消失。这使得复杂性保持在可控范围内。作者指出，虽然该想法背后的数学框架很深奥，但其实际应用却很直观：它只是提供了一种管理决策流的方法，并尊重它们之间的依赖关系。

论文还讨论了为什么这个想法此前未能在编程领域得到广泛采用。术语“余函子”在历史上常与其他概念混淆，导致对其特定用途缺乏清晰认识。此外，以往解决类似问题的尝试（如涉及数据库更新或模块化编程）通常侧重于不同的方面，比如保持数据一致性或合并代码模块，而不是关注实现选择的动态演进。作者建议，通过将余函子重新定义为一种“部分实现”的工具，这一概念变得更加易于理解，并能直接应用于软件工程师的日常工作中。

最终，这项工作为我们如何构建复杂系统提供了新的视角。它表明，处理不确定性的最佳方式不是冻结设计，也不是完全开放设计，而是创建一个让设计自然进化的结构。通过将软件视为一份关于选择与义务的“活文档”，工程师可以构建出稳健、灵活且易于推理的系统。其结果是一种允许在构建复杂系统的同时，将最终的、具体的细节留给真正需要它们的时刻的方法，从而确保所走的路径始终是逻辑一致的。

技术摘要：作为部分实现的余函子（Cofunctors）

问题陈述
在函数式编程和软件工程中，标准的实现模型是函子（functor）：即从规范范畴（ $S$ ）到具体实现范畴（ $C$ ）的映射，其中每个规范对象和态射都会被立即分配一个具体的实例化。然而，现实世界的软件开发通常需要阶段性配置（staged configuration），即实现选择（例如，数据表示、算法、后端协议）会被推迟。

现有的方法（如 ML 的参数化模块 functor）依赖于一个预先提供的全局参数类型 $P$ （即 $S \times P \to C$ ）。这种模型在处理**状态依赖型（state-dependent）**的选择时会失效：在某一阶段做出的选择（例如，选择持久化后端）可能会引入新的义务或约束（例如，要求特定的序列化格式或事务协议）。挑战在于如何建模这样一种系统：其可用实现选择的集合随着规范的演进而动态变化，且无需预先枚举所有可能的最终配置。

方法论
本文建议使用余函子（cofunctors，亦称为 retrofunctors）来建模部分实现（partial implementations）。该方法通过基于规范范畴 $S$ 和选择函子 $Choice: S \to \mathbf{Set}$ 构建一个部分实现范畴 $P$ 来实现。

状态依赖的选择： 对于每个规范对象 $A$ ，存在一个选择状态集 $Choice(A)$。这些状态代表了部分配置，其中某些字段已固定，而其他字段仍处于开放状态（义务）。
选择的传输（Transport of Choices）： 规范态射 $f: A \to B$ 诱导一个“传输”函数 $f^*: Choice(A) \to Choice(B)$ 。该函数通过携带现有选择并根据规范的变化引入新的义务或冲突，来更新实现状态。
余函子结构： 余函子被定义为一个跨距（span） $S \xleftarrow{p} \Lambda \xrightarrow{q} P$ $S p Λ q P$ ，其中：
- $q$ 在对象上是双射（将 $P$ 的对象识别为对 $(A, c)$ ，其中 $A \in S$ 且 $c \in Choice(A)$ ）。
- $p$ 是一个离散欧纤维（discrete opfibration），编码了选择的依赖菜单。
- 态射映射 impl 接收一个规范变化 $f$ 和一个当前选择 $c$ ，从而产生一个实现态射。至关重要的是，该态射的目标取决于传输后的选择 $f^*c$ 。
组合律： 复合规范变化 $g \circ f$ 的实现定义为：实现 $f$ 及其选择 $c$ ，更新状态为 $f^*c$ ，然后实现 $g$ 及其新状态。这确保了操作顺序尊重义务的演进。

本文通过 Idris 实现展示了这一点，利用依赖类型来强制要求实现状态（即选择）在每次规范转换中都被正确地更新和追踪。

核心贡献

概念性解读： 主要贡献在于将余函子作为部分实现进行的新颖解释。虽然余函子（或 retrofunctors）在范畴论中已存在（例如在 delta 镜 lens 或内部范畴的语境下），但本文明确将其框架化为管理延迟、状态依赖型实现选择的一种机制。
动态义务管理： 与静态参数化不同，这种方法允许实现选择的“菜单”动态变化。它支持如下场景：后期的阶段（如复制）可以引入新的需求（如事务日志），而这些需求在早期阶段（如简单存储）并不存在；同时也能检测冲突（例如，非事务性后端无法满足复制需求），而无需预先定义所有可能的组合。
可执行迁移计划： 该框架支持构建可执行的迁移计划，通过组合实现步骤。它区分了传输（transports）（由规范演进驱动的变化）与细化（refinements）（在不改变规范的情况下填补选择状态中的空缺）。
与替代方案的比较： 本文认为，虽然像 Backpack（用于静态 mixin 链接）或 tagless-final 编码（用于推迟解释器）这类工具解决了相关问题，但它们并不原生支持运行中系统的状态索引变换（state-indexed transformation），即在其中义务被增量且组合地解决。

结果与示例
论文提供了一个存储系统从通用 Store 演进到 PersistentStore，最后到 ReplicatedStore 的具体示例。

场景： 从一个包含 SQLite 后端但 serialiser 和 cache 尚未定义的选择状态开始。
过程：
1. 持久化（Persist）： 传输状态，保留后端，同时记录持久化义务。
2. 复制（Replicate）： 再次传输状态。如果后端是 SQLite，它能成功引入 protocol 义务。如果后端是 FlatFile（非事务性），则传输过程会显式导致 Conflict（冲突）状态。
结果： 系统生成一个类型化的迁移计划，该计划组合了这些步骤。该计划可以被执行以产生一个具体的系统（例如 SQLite/CBOR/LRU/Raft），或者在出现冲突时被拒绝。组合律确保了“持久化并复制”的单次路径过程等价于“先持久化后复制”的阶段性执行过程。

意义与主张
本文谦虚地声称，其使用的要素（余函子、阶段性配置、依赖类型）并非原创。其具体的贡献在于将这些范畴结构与函数式编程中部分实现这一实际问题联系起来的概念性解读。

作者断言，**“余函子是部分实现”**这一口号是一个新的、使问题明朗化的洞察。这种解读为以下方面提供了形式化基础：

管理其中选择依赖于当前规范状态的复合部分实现。
将义务管理的环境（余函子）与最终语义（到具体范畴的函子）分离。
在系统架构不断演进的系统中，处理动态迁移和配置。

文章总结道，尽管余函子已被用于单子范畴论和数据库更新传播（lens）中，但将其作为管理函数式编程中状态依赖型实现选择的独立工具的应用此前被忽视了，这可能是由于术语上与反变函子（contravariant functors）的混淆，以及镜（lens）文献中数据库理论视角的统治地位所致。

技术摘要：作为部分实现的余函子（Cofunctors）

类似论文