Measuring data types

技术摘要：测量数据类型

问题陈述
函数式编程语言（如 Haskell、Agfa、Coq）高度依赖归纳数据类型，这些类型在范畴论中被唯象地解释为自函子的初始代数，具体而言是被称为 W-型（W-types）的多项式自函子。虽然这些类型的范畴语义作为初始代数已被充分理解，但本文指出其周围的数学结构存在一个空白。具体而言，标准的范畴框架将代数之间的同态集（hom-sets）仅仅视为全同态（total homomorphisms）的集合。这无法捕捉数据类型之间“部分”或“近似”的结构关系，而这种关系对于理解同态如何以分级或分层的方式与归纳结构相互作用至关重要。作者试图通过类比 Sweedler 关于测量余代数（measuring coalgebras）的经典理论——即在域上的代数富集在余代数中——来阐明 W-型所嵌入的结构。

方法论
本文综合了两种截然不同的范畴理论：

1. Sweedler 的测量余代数： 作者回顾了经典理论，其中 $k$-代数富集在 $k$-余代数中。在这种设定下，两个代数之间的同态对象不是同态的集合，而是“部分同态”（或测量）的余代数。这些测量允许那些“接近”同态的映射，其余代数结构编码了映射在多大程度上“接近”于全同态。
2. W-型与归纳数据类型： 本文回顾了作为自函子（特别是多项式自函子）初始代数的归纳类型的范畴语义。

核心方法论是将 Sweedler 的理论从域上的代数背景推广到任意对称单子闭范畴 $\mathcal{C}$ 上的自函子 $F$ 的代数。作者假设 $\mathcal{C}$ 是局部呈现的（locally presentable），且 $F$ 是一个可达的（accessible）、松弛对称单子自函子。他们构建了 $F$-代数范畴（$\text{Alg}_F$）对 $F$-余代数范畴（$\text{coAlg}_F$）的富集。

关键技术步骤包括：

• 定义 $F$-代数和 $F$-余代数的测量（mappings $C \otimes A \to B$）和部分同态（mappings $C \to [A, B]$）。
• 证明存在一个通用测量余代数 $\text{Alg}(A, B)$，它作为富集范畴中的同态对象。
• 构造测量张量 $C \triangleright A$ 和卷积代数 $[C, B]$，以建立该范畴是张量化（tensored）且共张量化（cotensored）的。
• 将初始代数的概念推广为 $C$-初始代数，其中 $C$ 是一个余代数，类似于富集范畴理论中的加权极限（weighted limits）。

主要贡献与结果

1. 代数在余代数中的富集（定理 10）：
   核心结果指出，对于局部呈现的、闭对称单子范畴 $\mathcal{C}$ 和可达的、松弛对称单子自函子 $F$，代数范畴 $\text{Alg}_F$ 是富集、张量化且共张量化于余代数范畴 $\text{coAlg}_F$ 的。

   • 不再是同态的集合 $\text{Alg}(A, B)$，而是存在一个代表所有可能的部分同态的余代数 $\text{Alg}(A, B)$。
   • 这种富集通过自然同构进行刻画：
     $$\text{coAlg}(C, \text{Alg}(A, B)) \cong \text{Alg}(C \triangleright A, B) \cong \text{Alg}(A, [C, B])$$

2. W-型的推广：
   作者将 W-型（多项式自函子的初始代数）的概念推广为 $C$-初始代数。$C$-初始代数是一个代数 $A$，使得对于任何代数 $X$，都存在唯一的余代数同态 $C \to \text{Alg}(A, X)$。这允许根据余代数 $C$ 所编码的“形状”或“深度”对归纳类型进行更细致的分类。

3. 部分同态塔：
   本文构造了一个表示 $n$-部分同态的余代数塔 $\text{Alg}_n(A, B)$。该塔的极限 $\text{Alg}_\infty(A, B)$ 对应于 $\infty$-部分同态，它们近似于全代数同态。这为“部分归纳”提供了一个形式化机制，即可以通过逐层构建的方式归纳地建立同态。

4. 显式示例与计算：
   该理论被应用于计算机科学中的几种标准数据类型，包括：

   • 单元类型（Unit）与空类型（Empty）： 展示了平凡的富集。
   • 单子类型（Monoid Types）： 展示了单子结构如何引入测量的“扭转”（twists）。
   • 自然数： 计算了前初始代数（preinitial algebras，即 $\mathbb{N}$ 的有限截断）的通用测量余代数，并证明有限截断 $n$ 是末端 $n^\circ$-初始代数。
   • 列表（Lists）与树（Trees）： 将理论扩展到列表类型（基于单子）以及二叉/一般树。作者展示了测量如何同时控制数据结构的“形状”（深度/分支）和“扭转”（元素级的修改）。例如，他们表明，虽然从截断列表到全列表类型的全代数同态可能不存在，但测量是存在的。

意义与主张
本文声称通过将 Sweedler 现象应用于缺乏传统代数（具有单位、乘法等相干约束）的自函子，提供了 Sweeder 理论的“最纯粹形式”。作者认为，这种富集提供了研究代数间相互作用的高精度工具，超越了“是同态”或“不是同态”的二元对立。

其意义是双重的：

1. 纯数学： 它统一了测量余代数理论与 W-型理论，扩展了 Sweeder 理论的适用范围。它将初始代数的概念推广为 $C$-初始代数，为归纳类型提供了新的视角。
2. 编程语言理论： 该框架为归纳类型上的“部分”操作提供了范畴论依据。作者指出，这一结构最终可能影响函数式编程语言（如 Haskell）中归纳类型的实现，从而实现对部分数据或无限流（infinite streams）更灵活的处理。

文中明确指出，本文是之前工作 [20] 的扩展版本，增加了阐释性引言、完整的证明以及用于部分归纳的广义塔构造。作者承认，尽管该理论对于特定的自函子（如列表和树的自函子）是成立的，但在范畴 $\mathcal{C}$ 和自函子 $F$ 意义下的构造函子性仍是未来的研究课题。同样，在编程语言中的具体实现也被确定为未来的研究方向，而非当前的研究结果。