GATlab: Modeling and Programming with Generalized Algebraic Theories
Owen Lynch, Kris Brown, James Fairbanks, Evan Patterson
TL;DR
GATlab presents a Julia-embedded DSL for generalized algebraic theories ($GATs$) to unify algebraic specification with software engineering in applied category theory. It provides a practical framework for declaring $GATs$, building both free symbolic representations and host-language computational interpretations, and migrating between theories via morphisms. The paper details design choices, implementation strategies (including a large library of theories, multiple model styles, and symbolic modeling), and a comprehensive morphism system with pushforwards, pullbacks, and colimit-like combinations. It also surveys extensions to dependent types, scoped hygienic macros, and potential integrations with broader computer-algebra and symbolic-dynamics tooling, highlighting pathways to richer rewrite systems and 2-categorical structures. Overall, $GATlab$ aims to deliver a scalable, readable, and interoperable platform for categorically structured modeling across science and engineering.
Abstract
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.