Skip to content

Commit

Permalink
added "what is a GAT" section
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Oct 17, 2023
1 parent 0700539 commit 4e617cc
Showing 1 changed file with 16 additions and 0 deletions.
16 changes: 16 additions & 0 deletions docs/src/concepts/theories.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,21 @@
# Theories

## What is a GAT?

Generalized Algebraic Theories (GATs) are the backbone of GATlab so let's expand a bit on GATs and how they fit into the bigger picture of algebra.

An algebraic structure, like a group or category, is a mathematical object whose axioms all take the form of equations that are universally quantified (the equations have no exceptions). That’s not a formal definition but it’s a good heuristic. There are different ways to make this precise. The oldest, going back to universal algebra in the early 20th centrury, are algebraic theories.

[Universal algebra](https://en.wikipedia.org/wiki/Universal_algebra) (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples ("models") of algebraic structures. For instance, rather than take particular groups as the object of study, in universal algebra one takes the class of groups as an object of study. In an algebraic theory, you have a collection of (total) operations and they obey a set of equational axioms. Classically, there is only a single generating type, but there are also typed or multi-sorted versions of algebraic theories. Most of the classical structures of abstract algebra, such as groups, rings, and modules, can be defined as algebraic theories.

Importantly, the theory of categories is [not algebraic](https://mathoverflow.net/q/354920). In other words, a category cannot be defined as a (multi-sorted) algebraic theory. The reason is that the operation of composition is partial, since you can only compose morphisms with compatible (co)domains. Now, categories sure feel like algebraic structures, so people have come up with generalizations of algebraic theories that accomodate categories and related structures.

The first of these was Freyd’s essentially algebraic theories. In an essentially algebraic theory, you can have partially defined operations; however, to maintain the equational character of the system, the domains of operations must themselves be defined equationally. For example, the theory of categories would be defined as having two types, Ob and Hom, and the composition operation `compose(f::Hom,g::Hom)::Hom` would have domain given by the equation `codom(f) == dom(g)`. As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.

Later, Cartmell proposed generalized algebraic theories, which solves the same problem but in a different way. Rather than having partial operations, you have total operations but on dependent types (types that are parameterized by values). So now the composition operation has signature `compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) ⊣ [A::Ob, B::Ob, C::Ob]` exactly as appears in GATlab. This is closer to the way that mathematicians actually think and write about categories. For example, if you look at the definitions of category, functor, and natural transformation in [Emily Riehl’s textbook](http://www.math.jhu.edu/~eriehl/context/), you will see that they are already essentially in the form of a GAT, whereas they require translation into an essentially algebraic theory. Nevertheless, GATs and essentially algebraic theories have the same expressive power, at least in their standard set-based semantics. GATs provide a version of the computer scientist's type theory that plays well with the mathematician's algebra, thus, providing a perfect opportunity for computer algebra systems.

## The `@theory` macro

The result of the `@theory` macro is a module with the following members:

1. For each *declaration* in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like `dom` and `codom`), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use `Base.+` as a method for a theory. For instance, `ThCategory` has functions `Ob, Hom, dom, codom, compose, id, ⋅`.
Expand Down

0 comments on commit 4e617cc

Please sign in to comment.