How would a mathematician write down the generalized algebraic theory (GAT) for multicategories? It would be something like this:
\vdash \mathsf{Ob}:: \mathbf{Type}
For n\in\mathbf N:
x_1,\ldots,x_n, y :: \mathsf{Ob}\vdash \mathsf{Hom}_n(x_1,\ldots, x_n;y) :: \mathbf{Type}
For each m\in\mathsf{List}(\mathbf N) of length n:
x_{11},\ldots,x_{1m_1},\ldots,y_n,z :: \mathsf{Ob}, f_1:: \mathsf{Hom}_{m_1}((x_{1i});y_1),\ldots, g::\mathsf{Hom}_n((y_j),z)
\rule{11cm}{1pt}
\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad(f_i)\circ g::\mathsf{Hom}((x_{ij}),z).
…and so on to give the units and the associativity and unitality axioms.
Standard mathematical notation allows us to casually specify an infinite algebraic theory in finite space in this way. And if we can do it on paper…We should be able to do it on the computer!
But Gatlab and the older GAT implementation in Catlab can’t do this trick, because the computer doesn’t think it’s nearly as trivial as the mathematician does. In particular, if your syntax restricts GATs to be finite (i.e., plausibly typeable into a computer), then the GAT above doesn’t even exist.
That’s annoying.
So, we were just talking about how to add a little extra “sugar”[1] to Gatlab to let us type in something very similar to what I typed above and get an acceptable theory.
The core of what we’re looking for is dependent contexts. We want to be able to treat the context x_1::T_1,\ldots,x_n::T_n, for types T_i, as a single context for purposes of the explicit syntax. But what are these contexts depending on? Well, most simply, they’re depending on a natural number. In pure GAT syntax, we can’t define the type \mathsf{Nat}, though. The problem is that the universal property of \mathsf{Nat} says that the type \mathsf{Nat}\to T maps from T\times (T\to T) for any type T. But in plain GAT syntax, you can’t construct \mathsf{Nat}\to T or anything else that quantifies over your types. Of course, we could start adding in these missing type constructors, but a key interesting question about Gatlab is to see how far we can get without constructing another model of full dependent type theory!
What this shakes out to is that these contexts are not depending on terms of a type in our theory, so it makes the most sense to go to a two-level type theory, where the natural numbers live somewhere outside.
The outer type theory will be as trivial as we can possibly get away with. We’ll have the judgment \Theta\ \mathsf{nctxt}, whose intended meaning is that \Theta is a context of variables each ranging over (external/actual/Julia) natural numbers. As exemplified in the composition axiom for multicategories, we need to allow for multiple indexing variables, so we’ll assume a fresh set of variables i,j,k,\ldots. Then the generating rules for our outer type theory, using \vdash' instead of \vdash for permissible inferences in the outer theory, are \vdash' []\ \mathsf{nctxt} and \Theta\ \mathsf{nctxt} \vdash' \Theta,i\ \mathsf{nctxt}, whenever i does not occur in \Theta. Thus an \mathsf{nctxt} is just going to be a list of indexing variables, with no types attached to them.
To link the outer theory to the inner theory, we want to be able to say that whenever we have a context depending on an outer variable i, which is to say roughly speaking an \mathbf N-indexed family of contexts, we can build a single context subsuming all those contexts at once, which will produce the specific contexts by evaluating i. Thus we need to add some \lambda-abstraction to our theory:
\Theta\vdash' \Gamma\ \mathsf{ctxt}, \Theta,i\vdash' \Gamma,\Delta\ \mathsf{ctxt}
\rule{4cm}{1pt}
\Theta \vdash' \Gamma, \lambda i.\Delta\ \mathsf{ctxt}
This might look like the kind of thing I just said I wouldn’t want to do, but notice that the \lambda-abstraction occurs only over an outer variable. This variable is also untyped, so probably the outer type theory here is just a straight unityped \lambda-calculus.
That’s pretty much all I wanted to say on syntax! Of course there are lots of axioms that I didn’t state. In particular, we might want \vdash' judgments giving types and terms dependent on i, as well as just contexts. That said, here’s a proposal for something quite close to Gatlab code for a finite (in the code sense rather than the mathematical sense!) axiomatization of multicategories[2]:
\vdash \mathsf{Ob} :: \mathbf{Type}
i\vdash' (x_i),y :: \mathsf{Ob}\vdash \mathsf{Hom}((x_i),y) :: \mathbf{Type}
i,j\vdash' ((x_i)_j),y_j,z ::\mathsf{Ob},(f_j)::\mathsf{Hom}((x_i)_j,y_j),g::\mathsf{Hom}((y_j),z) \vdash g\circ (f_j) :: \mathsf{Hom}((x_{ij}),z)
Look, ma, no ellipses! There’s a sneaky flattening of a double list in there but I don’t think it’s much of anything to worry about in terms of the semantics.
OK, what about the semantics? Let’s say we want to generate a multicategory. Then we should give a set of objects as well as a function that takes a natural number i and a list of i+1 elements of the object set and returns a set of homs. I phrased that sentence to be quite easy to translate into code: my claim is that the actual semantics-in-code of the theory above will be that we have a Julia type or Catlab set Ob together with literal Julia function from the Julia type Int to the type of Julia functions from i+1-fold tuples in Ob to Julia types or Catlab sets.
Here’s a rough attempt to present an infinite multicategory in this way.
M = @present ThMultCat
x,y::Ob
f::Hom((x,y,x),y)
@∀ i g(i)::Hom(fill(i)(x),y)
f∘(g(2),id(y),g(3)) == whatever
I still haven’t really gotten up to speed on the syntaxes for explicit instances in Gatlab, so maybe we’ll see whether Owen shows up to try to make an explicit instance of this theory. The main things we notice from the syntactic presentation here is that we need to be able to write explicit lists like (x,y,x) and that we need some conveniences like the fill function to copy x a bunch of times. It seems likely enough to me that we could make these list-variables just be Julia vectors and ride off of that capability. All that said, as far as explicit instances, the key thinking I want to re-emphasize is that you would give a Function in Int->DataType [or to Set] to get, for instance, all the homs Hom(fill(i)(x),y), and more generally if you make an enum type {x,y} then you should be able to specify all the homs in this multicategory by giving a Function in Vector{{x,y}}\to Type. Then once more, to give the generators g(i) you need a Function on UInt and landing in the appropriate multi-homset for each input. This is another dependent function, but you can handle this either cheaply, by just not specifying the output type in Julia, or more fancily, by writing a zero-variable function parameterized by a UInt. Julia allows for a soft kind of dependent typing in this way: the thing that keeps it from getting complicated is that you can only parameterize by primitive types.
Alright, that’s more than enough for today! Curious to hear whether anybody knows any good context for this idea. It’s another thing that seems likely to be largely invisible to people focused on full dependent type theory, since once you can construct Nat you can construct Vect{T} and get probably everything we’re getting here from constructors based on terms of Vect.