GATlab：用广义代数理论进行建模与编程|代数|广义

GATlab：用广义代数理论进行建模与编程

GATlab: Modeling and Programming with Generalized

Algebraic Theories

https://arxiv.org/pdf/2404.04837v3

摘要

范畴和范畴结构作为科学与工程建模中有用的抽象工具，正日益得到认可。为了在软件中统一地实现范畴论数学模型，我们引入了 GATlab，这是一种嵌入在通用编程语言中的、用于代数规约的领域特定语言。GATlab 基于广义代数理论（GATs），这是一种扩展了依赖类型的代数理论的逻辑系统，旨在涵盖范畴论。使用 GATlab，程序员可以指定广义代数理论及其模型，包括基于符号表达式的自由模型，以及由宿主语言中的任意代码定义的计算模型。此外，程序员可以定义理论之间的映射，并利用它们以声明式的方式将一个理论的模型迁移到另一个理论的模型。简而言之，GATlab 旨在为计算机代数和软件接口设计提供一个基于广义代数理论的统一环境。在本文中，我们描述了 GATlab 的设计、实现及应用。

关键词：广义代数理论，GATs，代数规约，编程语言，应用范畴论

1 引言

范畴论长期以来一直被认为是编程中一种有用的组织原则。范畴论与类型论之间广泛的对应关系——起源于笛卡尔闭范畴与带积类型的 lambda 演算之间的等价性 [21]——促使语言设计者将各种各样的范畴概念引入编程语言中。在这种用法中，范畴论充当了编程语言的数学模型，通常为其提供指称语义。但这并不是范畴论在编程中能扮演的唯一角色。应用范畴论学者已经展示了范畴论如何能够形式化科学与工程中潜在的复合结构，从关系数据库到随机和量子过程，再到微分方程和动力系统 [37,15,13,24]。范畴论现在成为了主题领域的数学模型，而（像任何模型一样）如果它能在软件中实现，它将是最有用的。因此，我们需要一个能够轻松表达并计算范畴结构的软件系统。

这一目标可以通过根据范畴论思想设计宿主语言来实现，但原则上并不依赖于它。事实上，目前这两种角色之间存在张力，因为最自然地表达范畴概念的依赖类型语言往往缺乏科学与工程计算的功能，而科学家和工程师最常用的语言则通常只有极简的类型系统。这个问题可以从两个方向着手解决。在这项工作中，我们展示了如何增强现有的技术计算语言，为其添加高级类型系统，从而实现对范畴结构的统一计算。

与其试图将完整的依赖类型理论强行移植到弱类型编程语言上，我们采用广义代数理论（Generalized Algebraic Theories），这是代数理论的扩展，足以公理化范畴结构。广义代数理论（GAT）[8,9]——更贴切地称为依赖类型代数理论 [33]——与（有类型或排序的）代数理论类似，区别在于其类型可以依赖于项。GAT 的原型例子是范畴论，其中态射的类型依赖于一对对象，即定义域和陪域。尽管 GAT 是一种相对简单的类型理论，但它足以公理化本质上任何由配备了额外代数（方程）定义的结构的范畴所组成的理论。可作为 GAT 公理化的范畴结构示例包括：范畴；预层和余预层；幺半范畴（无论是严格的还是弱的，辫状的还是对称的）；配备了选定有限积或有限极限的范畴；以及 2-范畴、双范畴和双重范畴。

1.1 贡献

在本文中，我们描述了 GATlab 的设计与实现，这是一个基于 Julia 编程语言构建的嵌入式领域特定语言的广义代数理论编程框架。GAT 长期以来一直是 Catlab 的基础，Catlab 是一个专注于科学和工程应用的应用范畴论框架。我们最近从头重写了 GAT 系统，并显著扩展了其功能。这是我们首次在印刷出版物中对其进行描述。

GATlab 的主要贡献包括：

在技术编程语言中提供一种基于极简依赖类型理论的代数规约语言；
支持包含超过 90 个可重用理论的标准库，范围从群和环等经典代数结构到幺半范畴和预层等范畴结构；
实现对 GAT 模型的统一计算，包括基于符号表达式的自由模型，以及由宿主语言中的任意代码定义的计算模型；
通过理论的态射，以声明式和代数的方式将一个理论的模型迁移到另一个理论。

简而言之，GATlab 旨在成为科学与工程中范畴结构化建模工具的结构化和符号化基础。

1.2 相关工作

GATs 的数学理论及其在软件中的应用都有着悠久的历史。本节我们将回顾其中部分历史，并阐释 GATlab 与之的关系。

最古老的相关研究脉络是泛代数（universal algebra）理论。“泛代数”这一术语至少可追溯至怀特海 [39]，但该学科直到伯克霍夫 1946 年的论述 [3] 才奠定了形式化基础。后来，劳维尔在其博士论文中展示了泛代数中的许多构造如何自然地源于范畴论的基本概念 [23]。

泛代数的早期实现见于 OBJ 和 Clear 语言 [16,5]。Clear 语言的模块系统影响了标准 ML 模块系统的设计 [28,29] 以及后续 OBJ 系列语言的迭代版本 [17]。这些泛代数概念的现代表现形式可见于 Maude 等系统 [12]。我们最初为 GATlab 设定的目标之一，便是在 Julia 中构建一个受 ML 启发的模块系统，使理论的实现成为可具体化的对象，正如签名（signature）的实现在 ML 中那样。直到后来我们才意识到，ML 模块本身便是受泛代数启发的，因此从某种意义上说，GATlab 继承了一个久负盛名的传统。

然而，GATlab 超越了这一传统，它采用了广义代数理论，将泛代数扩展至包含依赖类型，而这正是范畴论所必需的。用依赖类型扩展泛代数的挑战已通过多种方式得到解决。一种途径是通过逻辑框架（LF），该框架最早由 [20] 提出。逻辑框架是一种操纵依赖类型论语法的代数方法，即通过将依赖类型论嵌入到另一个依赖类型论中来实现。GATlab 扮演着与 LF 类似的“元”角色，但不支持对变量进行量化的类型构造子。另一方面，GATlab 提供了 LF 所不具备的其他功能，例如向理论中添加任意方程的能力。此前人们认为这是一个坏主意，因为它会破坏类型检查和相等性检查的可判定性。但正如我们将展示的，即使在缺乏可判定类型检查的情况下，利用 GATs 仍能完成有趣且有用的工作。

GATlab 强调以理论态射作为在不同理论间转换及通过余极限组合理论的手段，这一思路也见于数学知识管理（MKM）系统 MMT [34]；MMT 支持更广泛的理论类别，但对计算语义的关注较少。同样，这种 MKM 方法也见于 MathScheme [6] 以及关于理论展示组合子的相关工作 [7]。

最后，GATlab 是范畴及其他范畴结构的计算实现。此方向上的相关项目包括 Rydeheard 和 Burstall 的计算范畴论 [36]，以及 CAP（Categories, Algorithms, and Programming）计算机代数系统 [19,2]。

2 背景：广义代数理论及其模型

我们回顾广义代数理论（GATs）背后的主要思想，重点关注其语法（包括数学记号和 GATlab 编程记号）以及其标准的集合论语义。GATs 由 John Cartmell 在其博士论文 [8] 中引入，随后在出版物 [9] 中发表，本文省略的许多细节可参阅该文献。作为进一步的参考，Pitts [33, §6] 和 Taylor [38, Chapter VIII] 介绍了基于 Cartmell 的 GATs 的类型理论。

2.1 GATs 的语法

项构造器（Term constructor） 带类型的项由项构造器引入。项本身及其类型均可依赖于上下文中的变量。

项相等性（Term equality） 断言上下文中项之间等式的公理，通过项相等性来指定。

例如，范畴论包含两个类型构造器，分别对应对象和态射；两个项构造器，分别对应复合和单位态射；以及三个项相等性，分别对应结合律、左单位律和右单位律公理。

作为技术补充说明，我们注意到，根据 Cartmell 的观点，GATs 还允许第四种判断，即类型之间的相等性。我们遵循 Taylor [38] 的做法，在 GATlab 中排除了类型相等性。这一限制简化了系统，即便它并未解决类型检查问题（因为依赖类型仍可能因其所依赖的项之间的等式而产生非平凡的相等关系）。从范畴论的角度来看，禁止显式的类型相等性并无损失，因为类型之间的等式无论如何都更适合用同构来处理。

具体而言，这一限制使得种类检查（sort-checking）和种类推断（sort-inference）变得相当简单。种类推断用于确定项的类型所使用的类型构造器。例如，它将一个项归类为对象或态射，而不必确切地找出该态射的定义域或陪域。这是一种实用且快速的检查，我们在 GATlab 的大多数操作中都会执行它，能够捕获表层的错误。

2.3 GATs 的替代方案

广义代数理论属于一族本质上等价的逻辑，这些逻辑扩展了代数理论的逻辑，以涵盖范畴论及其他类似理论。除了 GATs 之外，这些逻辑中最著名的是本质代数理论（essentially algebraic theories）[1, §3.D]、有限极限草图（finite limit sketches）和有限极限理论（finite limit theories）。Cartmell 勾勒了一个论证，大意是在其集合论语义下，广义代数理论和本质代数理论具有等价的模型范畴 [9, §6]。与此同时，本质代数理论和有限极限草图直接被意图作为有限极限理论（一种理论的不变量概念）的语法呈现。

原则上，这些逻辑中的任何一种都可以扮演 GATs 在 GATlab 中所扮演的角色。我们选择 GATs 是出于实用考虑：尽管它们的元理论很复杂，但 GATs 能产生迄今为止最易读且最直观的范畴结构理论的呈现形式，往往与其教科书形式非常相似。

3 GATlab 中的 GAT 模型

在软件工程的语境下，GATs 扮演着接口或形式规约的角色。因此，GAT 的模型就是实现该接口并满足该形式规约的数据结构。

3.1 代数理论的模型

3.2 将依赖类型纳入模型

到目前为止，我们在 GATlab 中仅考虑了代数理论的模型。鉴于 Julia 并不完全具备依赖类型，我们如何扩展这些经典的模型概念以支持依赖类型呢？[10] 我们曾考虑过两种在非依赖语言中对依赖类型进行建模的方法。以范畴为例来考察这两种方法具有启发意义。

在这种风格下，我们可以如下实现有限集范畴，或者更确切地说，是其骨架。首先，我们为这个范畴的对象和态射定义数据结构。

在原始 Catlab 对 GATs 的实现中，采取的做法是将定义域和陪域与态射的数据一同存储。事实上，定义域或陪域往往无法从态射的数据中推导出来。在上面的例子中，将函数的数据表示为一个值数组只能确定其值域（range），而不能确定其陪域（codomain），因此陪域必须单独存储。虽然这种方法很直观，但其缺点是态射的数据结构必须携带额外的数据。因此，一个由态射组成的图表最终可能会存储许多对象的冗余副本。

本节最后，我们将演示如何创建一个以基范畴为参数的切片范畴模型。首先，我们声明一个模型结构体。

3.3 GAT 的自由模型

associate，针对结合律规范化二元运算
associate_unit，针对结合律和单位律规范化二元运算
associate_unit_inv，针对结合律、单位律和逆元规范化二元运算
distribute_unary，将一元运算分配到二元运算上
involute，规范化对合一元运算
normalize_zero，当表达式包含零时将其坍缩为零

然而，这些仅仅是我们发现有用的规范化策略；我们的方法并不排除实现其他策略的可能性。

4 GAT 的态射

虽然总是可以编写任意函数将一个理论的模型转换为另一个理论的模型，但必须编写的代码往往晦涩难懂且不易验证。在许多情况下，解决这一问题的办法在于不同的 GAT 之间通过态射（也称为解释）相互关联。利用 GAT 的态射，我们实现了一种声明式且可验证的语法，用于将一个理论的模型迁移到另一个理论。

4.1 GAT 态射的语法

例如，考虑将幺半群语言中的语句翻译为自然数算术语言：

上述例子可以与用户声明的、类型错误或给出无效解释的态射进行对比：

4.2 GAT 态射子类的数据结构

GAT 的态射具有高度的表现力，这也带来了一定程度的复杂性。考虑那些限制性更强、但所需指定数据更少的 GAT 态射会是很有用的。这些限制更强的 GAT 态射也使得计算（例如推挽图）变得更加容易。GATlab 定义了不少于四种数据结构来实现不同表现力的 GAT 态射：

4.3 利用 GAT 态射进行计算

5 应用与扩展

在创建 GATlab 包以替代 Catlab 中的 GAT 机制时，我们的首要目标是探索新的设计决策，例如： (i) ML 模块风格的 GAT 模型，以及 Haskell 类型类风格（3.1 节）； (ii) 依赖类型的纤维化观点与索引化观点（3.2 节）； (iii) 通过作用域标签进行的卫生替换（附录 A.1）；但同时保留与 Catlab 足够的向后兼容性，以便可以增量地采用这些新功能，而不是一次性全部采用。既然已经完成了这项重大的工程工作，我们开始在整个用于应用范畴论的 AlgebraicJulia 包生态系统中利用 GATlab 的新功能。

GATlab 背后的动机之一是为符号动力系统构建功能。过去，我们在任意 Julia 函数之上构建动力系统 [24]。然而，使动力系统中的各种函数符号化解锁了一系列新能力，例如：

系统可以被优化/编译以生成更高效的代码
系统可以进行符号分析以证明其性质，而无需对其进行模拟
系统可以在不同的编程语言之间转移
定义系统的方程可以被美观地打印并显示给用户

第一篇作者写了一篇博客文章探讨了这些方向 [25]，并且我们有一个作为操作代数（operad algebra）的符号资源共享器的初步实现 [26]。值得注意的是，GATlab 允许我们实现这些符号资源共享器，使其不依赖于符号函数实现中可用的确切“原始函数”集合。例如，我们可以只允许多项式函数，或者只允许多项式和三角函数，等等。

为了支持这些系统理论能力，GATlab 的另一个主要方向是开发更丰富的计算机代数功能。我们有兴趣探索类型如何有助于为超越经典抽象代数的数学对象开发计算机代数。例如，我们已经原型化了一个理论，其中主要的研究对象是“向量丛的截面”，其中向量丛本身和向量丛所在的空间都是类型构造器的参数。这将使得微分几何中的问题能够进行 principled（有原则的）、无坐标的描述，并通过在 Decapodes [32,31] 中的应用而应用于偏微分方程。

我们正在考虑几种方式为 GATlab 添加更复杂的重写功能以用于计算机代数目的。基于对 egg 源代码 [40] 的仔细阅读，我们已经原型化了针对 GATlab 语法树的 e-graphs 实现。然而，Julia 已经有了一个优秀的 e-graphs 实现，即 Metatheory.jl [10]，我们希望与之集成。无论如何，e-graphs 的优势在于它们几乎适用于任何重写问题，这与 GATs 的通用性非常契合。然而，在环和模等专业领域中，涉及 Gröbner 基的算法可能比朴素地使用 e-graphs 高效得多。我们可以通过 Symbolics.jl [18] 和 CAP 项目 [2] 在 Julia 中访问此类计算机代数系统，因此另一个方向是将这些集成到 GATlab 中的特定理论中。

GATs 的一个局限性是，虽然我们可以为范畴指定一个 GAT，但 GATs 只有模型的 1-范畴而不是 2-范畴。因此，从范畴的 GAT 中，我们可以自动导出函子的概念，但不能导出自然变换的概念。Lambert 和 Patterson 有一个“笛卡尔双重理论”的概念 [22]，其模型自然地形成一个 2-范畴，这可能是一个比广义代数理论更自然的框架来用于“范畴的计算机代数”。

未来研究的另一个方向是随机测试。这可以通过两种方式完成。第一种是取理论中的一个任意方程（其有效性不确定），然后检查它在 GAT 的随机采样有限模型中是否为真。当然，这不能证明该方程为真，但它可以提供 Nitpick [4] 和 Alloy [30] 风格的反例。第二种方法是取一个声称的 GAT 模型，然后在该模型中采样类型的元素，以检查 GAT 中的方程是否实际成立，采用 QuickCheck [11] 和 Hypothesis [27] 的风格。这将提供一种廉价的方式来获得对实现的信心，并提高任何使用 GATlab 的代码的整体质量。

原文链接：https://arxiv.org/pdf/2404.04837v3