Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2404.04837 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929634382184448 |
|---|---|
| author | Lynch, Owen Brown, Kris Fairbanks, James Patterson, Evan |
| author_facet | Lynch, Owen Brown, Kris Fairbanks, James Patterson, Evan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_04837 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | GATlab: Modeling and Programming with Generalized Algebraic Theories Lynch, Owen Brown, Kris Fairbanks, James Patterson, Evan Logic in Computer Science Programming Languages 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. |
| title | GATlab: Modeling and Programming with Generalized Algebraic Theories |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2404.04837 |