# Theories, instances, and expressions

At the core of Catlab is a system for defining generalized algebraic structures, such as categories and monoidal categories, and then creating instances of these structures in Julia code. The objects, morphisms, and even higher-order morphisms can also be represented as typed symbolic expressions, as in a computer algebra system. These expressions can be manipulated abstractly or transformed into more concrete representations, such as wiring diagrams or Julia functions.

The basic elements of this system are:

**Generalized algebraic theories**(GATs), defined using the`@theory`

macro. Categories and other typed (multisorted) algebraic structures can be defined as GATs. Alternatively, the`@signature`

macro can be used when only the signature (not the axioms) of the GAT are to be specified.**Instances**, or concrete implementations, of theories, defined using the`@instance`

macro.**Syntax systems**for theories, defined using the`@syntax`

macro. These are type-safe expression trees constructed using ordinary Julia functions.

We'll explain each of these elements in greater detail in the following sections. From the programming perspective, theories can be thought of as *interfaces* and bear some resemblance to type classes in languages like Haskell. Both instances and syntax systems can then be thought of as *implementations* of the interface.

## Theories

Generalized algebraic theories (GATs) are the natural logical system in which to define categories and related algebraic structures. GATs generalize the typed (multisorted) algebraic theories of universal algebra by incorporating a fragment of dependent type theory; they are perhaps the simplest dependently typed logics.

Catlab implements a version of the GAT formalism on top of Julia's type system, taking advantage of Julia macros to provide a pleasant syntax. GATs are defined using the `@theory`

macro.

For example, the theory of categories could be defined by:

```
@theory Category{Ob,Hom} begin
@op begin
(→) := Hom
(⋅) := compose
end
Ob::TYPE
Hom(dom::Ob, codom::Ob)::TYPE
id(A::Ob)::(A → A)
compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob)
(f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob,
f::(A → B), g::(B → C), h::(C → D))
f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))
id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B))
end
```

The code is simplified only slightly from the official Catlab definition of `Category`

. The theory has two *type constructors*, `Ob`

(object) and `Hom`

(morphism). The type `Hom`

is a dependent type, depending on two objects, named `dom`

(domain) and `codom`

(codomain). The theory has two *term constructors*, `id`

(identity) and `compose`

(composition).

Notice how the return types of the term constructors depend on the argument values. For example, the term `id(A)`

has type `Hom(A,A)`

. The term constructor `compose`

also uses *context variables*, listed to the right of the `⊣`

symbol. These context variables can also be defined after a `where`

clause, but the left hand side must be surrounded by parentheses. This allows us to write `compose(f,g)`

, instead of the more verbose `compose(A,B,C,f,g)`

(for discussion, see Cartmell, 1986, Sec 10: Informal syntax).

Notice the `@op`

call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as `@op (⋅) := compose`

to define a single alias. Here we utilize this functionality by replacing the `Hom`

and `compose`

methods with their equivalent Unicode characters, `→`

and `⋅`

respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.

In general, a GAT consists of a *signature*, defining the types and terms of the theory, and a set of *axioms*, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, Catlab supports the specification of both signatures and the axioms, but is not currently utilizing the axiom definitions in any way, reflecting its status as a programming library, not a proof assistant. It is the programmer's responsibility to ensure any declared instances of an algebraic structure satisfy its axioms.

#### References

- Cartmell, 1986: Generalized algebraic theories and contextual categories, DOI:10.1016/0168-0072(86)90053-9
- Cartmell, 1978, PhD thesis:
*Generalized algebraic theories and contextual categories* - Pitts, 1995: Categorical logic, Sec 6: Dependent types

## Instances

A theory can have one or more *instances*, or instantiations by ordinary Julia types and functions. This feature builds on Julia's support for generic functions with multiple dispatch.

Instances are declared using the `@instance`

macro. In an instance of a theory, each theory type is mapped to a Julia type and each term is mapped to a Julia method of the same name. For example, the category of matrices could be defined as an instance of the theory `Category`

defined above:

```
using LinearAlgebra: I
struct MatrixDomain
eltype::Type
dim::Int
end
@instance Category{MatrixDomain, Matrix} begin
dom(M::Matrix) = MatrixDomain(eltype(M), size(M,1))
codom(M::Matrix) = MatrixDomain(eltype(M), size(M,2))
id(m::MatrixDomain) = Matrix{m.eltype}(I, m.dim, m.dim)
compose(M::Matrix, N::Matrix) = M*N
end
```

```
A = Matrix{Float64}([0 1; 1 0])
id(dom(A))
```

```
2×2 Matrix{Float64}:
1.0 0.0
0.0 1.0
```

In this instance, the theory type `Ob`

is mapped to the custom Julia type `MatrixDomain`

. The latter type has two fields, a Julia type `eltype`

representing a field $k$ and an integer `dim`

representing the dimensionality $n$, and so can be interpreted as the $n$-dimensional vector space $k^n$. The theory `Hom`

is mapped to the standard Julia type `Matrix`

.

## Syntax systems

Theories can also be instantiated as systems of symbolic expressions, using the `@syntax`

macro. The symbolic expressions are expression trees, as commonly used in computer algebra systems. They are similar to Julia's `Expr`

type but they are instead subtyped from Catlab's `GATExpr`

type and they have a more refined type hierarchy.

A single theory can have different syntax systems, treating different terms as primitive or performing different simplication or normalization procedures. Catlab tries to make it easy to define new syntax systems. Many of the theories included with Catlab have default syntax systems, but the user is encouraged to define their own to suit their needs.

To get started, you can always call the `@syntax`

macro with an empty body. Below, we subtype from Catlab's abstract types `ObExpr`

and `HomExpr`

to enable LaTeX pretty-printing and other convenient features, but this is not required.

```
@syntax CategoryExprs{ObExpr, HomExpr} Category begin
end
A, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]
f, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)
compose(compose(f,g),h)
```

\[\left(f \cdot g\right) \cdot h : A \to D\]

The resulting symbolic expressions perform no simplification. For example, the associativity law is not satisfied:

`compose(compose(f,g),h) == compose(f,compose(g,h))`

`false`

Thus, unlike instances of a theory, syntactic expressions are not expected to obey all the axioms of the theory.

However, the user may supply logic in the body of the `@syntax`

macro to enforce the axioms or perform other kinds of simplification. Below, we use the `associate`

function provided by Catlab to convert the binary expressions representing composition into $n$-ary expressions for any number $n$. The option `strict=true`

tells Catlab to check that the domain and codomain objects are strictly equal and throw an error if they are not.

```
@syntax SimplifyingCategoryExprs{ObExpr, HomExpr} Category begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
end
A, B, C, D = [ Ob(SimplifyingCategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]
f, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)
compose(compose(f,g),h)
```

\[f \cdot g \cdot h : A \to D\]

Now the associativity law *is* satisfied:

`compose(compose(f,g),h) == compose(f,compose(g,h))`

`true`

### Primitive versus derived operations

In some algebraic structures, there is a choice as to which operations should be considered primitive and which should be derived. For example, in a cartesian monoidal category, the copy operation $\Delta_X: X \to X \otimes X$ can be defined in terms of the pairing operation $\langle f, g \rangle$, or vice versa. In addition, the projections $\pi_{X,Y}: X \otimes Y \to X$ and $\pi_{X,Y}': X \otimes Y \to Y$ can be defined in terms of the deleting operation (terminal morphism) or left as primitive.

In Catlab, the recommended way to deal with such situations is to define *all* the operations in the theory and then allow particular syntax systems to determine which operations, if any, will be derived from others. In the case of the cartesian monoidal category, we could define a signature `CartesianCategory`

by inheriting from the builtin theory `SymmetricMonoidalCategory`

.

```
@signature CartesianCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
mcopy(A::Ob)::(A → (A ⊗ A))
delete(A::Ob)::(A → munit())
pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
proj2(A::Ob, B::Ob)::((A ⊗ B) → B)
end
nothing # hide
```

We could then define the copying operation in terms of the pairing.

```
@syntax CartesianCategoryExprsV1{ObExpr,HomExpr} CartesianCategory begin
mcopy(A::Ob) = pair(id(A), id(A))
end
A = Ob(CartesianCategoryExprsV1.Ob, :A)
mcopy(A)
```

Alternatively, we could define the pairing and projections in terms of the copying and deleting operations.

```
@syntax CartesianCategoryExprsV2{ObExpr,HomExpr} CartesianCategory begin
pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))
proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))
proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))
end
A, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ]
f, g = Hom(:f, A, B), Hom(:g, A, C)
pair(f, g)
```

## API

`Catlab.GAT`

— ModuleGeneralized algebraic theories (GATs) in Julia.

`Catlab.GAT.invoke_term`

— MethodInvoke a term constructor by name on an instance.

This method provides reflection for GATs. In everyday use the generic method for the constructor should be called directly, not through this function.

Cf. Julia's builtin `invoke()`

function.

`Catlab.GAT.theory`

— FunctionRetrieve generalized algebraic theory associated with abstract type.

For example, if `Category`

is imported from `Catlab.Theories`

, then `theory(Category)`

returns the theory of a category.

`Catlab.GAT.@instance`

— MacroDefine an *instance* of a generalized algebraic theory (GAT).

`Catlab.GAT.@signature`

— MacroDefine a signature for a generalized algebraic theory (GAT).

A signature is the same as a theory, except it may not contain axioms, and therefore only three kinds of things can go in the signature body:

- Type constructors, indicated by the special type
`TYPE`

, e.g.,`Hom(X::Ob,Y::Ob)::TYPE`

- Term constructors, e.g.,
`id(X::Ob)::Hom(X,X)`

- Function aliases, e.g.,
`@op Hom :→`

A signature can extend existing theories (at present only one).

`Catlab.GAT.@theory`

— MacroDefine a generalized algebraic theory (GAT).

Four kinds of things can go in the theory body:

- Type constructors, indicated by the special type
`TYPE`

, e.g.,`Hom(X::Ob,Y::Ob)::TYPE`

- Term constructors, e.g.,
`id(X::Ob)::Hom(X,X)`

- Function aliases, e.g.,
`@op Hom :→`

- Equality axioms, e.g.,
`f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))`

A theory can extend existing theories (at present only one).

`Catlab.Syntax`

— ModuleSyntax systems for generalized algebraic theories (GATs).

In general, a single theory may have many different syntaxes. The purpose of this module to enable the simple but flexible construction of syntax systems.

`Catlab.Syntax.GATExpr`

— TypeBase type for expression in the syntax of a GAT.

We define Julia types for each *type constructor* in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)

The concrete types are structurally similar to the core type `Expr`

in Julia. However, the *term constructor* is represented as a type parameter, rather than as a `head`

field. This makes dispatch using Julia's type system more convenient.

`Base.Meta.show_sexpr`

— MethodShow the syntax expression as an S-expression.

Cf. the standard library function `Meta.show_sexpr`

.

`Catlab.GAT.invoke_term`

— MethodInvoke a term constructor by name in a syntax system.

This method provides reflection for syntax systems. In everyday use the generic method for the constructor should be called directly, not through this function.

`Catlab.Syntax.functor`

— MethodFunctor from GAT expression to GAT instance.

Strictly speaking, we should call these "structure-preserving functors" or, better, "model homomorphisms of GATs". But this is a category theory library, so we'll go with the simpler "functor".

A functor is completely determined by its action on the generators. There are several ways to specify this mapping:

Specify a Julia instance type for each GAT type, using the required

`types`

tuple. For this to work, the generator constructors must be defined for the instance types.Explicitly map each generator term to an instance value, using the

`generators`

dictionary.For each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the

`terms`

dictionary.

The `terms`

dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.

`Catlab.Syntax.parse_json_sexpr`

— MethodDeserialize expression from JSON-able S-expression.

If `symbols`

is true (the default), strings are converted to symbols.

`Catlab.Syntax.show_latex`

— MethodShow the expression in infix notation using LaTeX math.

Does *not* include `$`

or `\[begin|end]{equation}`

delimiters.

`Catlab.Syntax.show_unicode`

— MethodShow the expression in infix notation using Unicode symbols.

`Catlab.Syntax.to_json_sexpr`

— MethodSerialize expression as JSON-able S-expression.

The format is an S-expression encoded as JSON, e.g., "compose(f,g)" is represented as ["compose", f, g].

`Catlab.Syntax.@syntax`

— MacroDefine a *syntax* system for a generalized algebraic theory (GAT).

A syntax system consists of Julia types (with top type `GATExpr`

) for each type constructor in the signature, plus Julia functions for

*Generators*: creating new generator terms, e.g., objects or morphisms*Accessors*: accessing type parameters, e.g., domains and codomains*Term constructors*: applying term constructors, e.g., composition and monoidal products

Julia code for all this is generated by the macro. Any of the methods can be overriden with custom simplification logic.

`Catlab.Rewrite`

— ModuleRewriting for GAT expressions.

The current content of this module is just a stopgap until I can implement a generic term rewriting system.

`Catlab.Rewrite.associate`

— MethodSimplify associative binary operation.

Maintains the normal form `op(e1,e2,...)`

where `e1`

,`e2`

,... are expressions that are *not* applications of `op()`

`Catlab.Rewrite.associate_unit`

— MethodSimplify associative binary operation with unit.

Reduces a freely generated (typed) monoid to normal form.

`Catlab.Rewrite.associate_unit_inv`

— MethodSimplify associative binary operation with unit and inverses.

`Catlab.Rewrite.distribute_unary`

— MethodDistribute unary operation over binary operation.

`Catlab.Rewrite.involute`

— MethodSimplify involutive unary operation.

`Catlab.Present`

— ModuleFinite presentations of a model of a generalized algebraic theory (GAT).

We support two methods for defining models of a GAT: as Julia objects using the `@instance`

macro and as syntactic objects using the `@present`

macro. Instances are useful for casting generic data structures, such as matrices, abstract tensor systems, and wiring diagrams, in categorical language. Presentations define small categories by generators and relations and are useful in applications like knowledge representation.

`Catlab.Present.add_definition!`

— MethodAdd a generator defined by an equation.

`Catlab.Present.add_equation!`

— MethodAdd an equation between terms to a presentation.

`Catlab.Present.add_generator!`

— MethodAdd a generator to a presentation.

`Catlab.Present.add_generators!`

— MethodAdd iterable of generators to a presentation.

`Catlab.Present.equations`

— MethodGet all equations of a presentation.

`Catlab.Present.generator`

— MethodRetrieve generators by name.

Generators can also be retrieved using indexing notation, so that `generator(pres, name)`

and `pres[name]`

are equivalent.

`Catlab.Present.generator_index`

— MethodGet the index of a generator, relative to generators of same GAT type.

`Catlab.Present.generators`

— MethodGet all generators of a presentation.

`Catlab.Present.has_generator`

— MethodDoes the presentation contain a generator with the given name?

`Catlab.Present.@present`

— MacroDefine a presentation using a convenient syntax.