Catlab.jl is a framework for applied and computational category theory, written in the Julia language. Catlab provides a programming library and interactive interface for applications of category theory to scientific and engineering fields. It emphasizes monoidal categories due to their wide applicability but can support any categorical structure that is formalizable as a generalized algebraic theory.
The documentation contains several example notebooks, as well as partial API docs. However, we readily acknowledge that the documentation is not as well developed as it should be. Feel free to ask questions! Besides the GitHub issues, we have a #catlab.jl stream on the Julia Zulip (preferred) and also a #catlab channel on the Julia Slack (less preferred).
Catlab is experimental software and is missing many features, big and small. Moreover, the computational aspects of category theory are generally underdeveloped, both theoretically and practically. On the flip side, this means that there are lots of opportunities to do new and interesting things! Applied category theory is a young field and is likely to grow significantly.
We welcome contributions and are committed to supporting prospective contributors, regardless of experience level with category theory. If you are interested in contributing, please let us know.
Catlab is, or will eventually be, the following things.
Programming library: First and foremost, Catlab provides data structures, algorithms, and serialization for applied category theory. Macros offer a convenient syntax for specifying categorical doctrines and type-safe symbolic manipulation systems. Wiring diagrams (aka string diagrams) are supported through specialized data structures and can be serialized to and from GraphML (an XML-based format) and JSON.
Interactive computing environment: Catlab can also be used interactively in Jupyter notebooks. Symbolic expressions are displayed using LaTeX and wiring diagrams are visualized using Compose.jl, Graphviz, or TikZ.
Computer algebra system: Catlab will serve as a computer algebra system for categorical algebra. Unlike most computer algebra systems, all expressions are typed using fragment of dependent type theory called generalized algebraic theories. We will implement core algorithms for solving word problems and reducing expressions to normal form with respect to several important doctrines, such as those of categories and of symmetric monoidal categories. For the computer algebra of classical abstract algebra, see AbstractAlgebra.j and Nemo.jl.
Catlab is not currently any of the following things, although we do not rule out that it could eventually evolve in these directions.
Automated theorem prover: Although there is some overlap between computer algebra and automated theorem proving, Catlab cannot be considered a theorem prover because it does not produce formal certificates of correctness (aka proofs).
Proof assistant: Likewise, Catlab is not a proof assistant because it does not produce formally verifiable proofs. Formal verification is not within scope of the project.
Graphical user interface: Catlab does not provide a wiring diagram editor or other graphical user interface. It is primarily a programming library, not a user-facing application. However, it could be used as the backend for such an application.