Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.

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