It came up yesterday that the nLab article on GATs is wrong, not to mention missing any discussion of their semantics, so I thought I’d say a couple of words about that here.
A GAT is a type theory in which you can make the judgments that A is a type, that t is a term of a type A, and that two types or two terms of a type are equal. What makes GATs GATs is that you can make judgments like x:A,y:B\vdash C(x,y)\text{ type}, so that types can depend on terms. You can, by all means, write something like x,y:A,f,g:B(x,y)\vdash C(f,g)\text{ type}, as you would for presenting a 2-category, which is where the nLab article looks to me like it gets confused. So, in short, GATs are simply dependent type theories, which can rapidly take you in a very different direction than something like essentially algebraic theories.
The canonical kind of model M for a GAT is an interpretation of its independent types A as sets A_M, its singly-dependent types x:A\vdash B(x)\text{ type} as families B_M(a) of sets indexed by elements of A_M, and so on through families of families, families of families of families, et cetera. Then, terms are interpreted as functions, so if your GAT contains the rule x:A\vdash f(x):B then your model has a function f_M:A_M\to B_M, while if it has a rule like x:A,y:B(x),z:C(x,y)\vdash f(x,y,z): D(x,y,z), which is a more characteristic kind of term judgment, then for all a\in A_M,b\in B_M(a), c\in C_M(a,b), you have to provide an element f_M(a,b,c) of D_M(a,b,c). If your theory contains equations between types or terms, these equations also have to be satisfied in the model.
All of this is probably the natural generalization of the notion of model for any kind of theory you personally enjoy modeling, just with lots of extra variables encoding the dependency of the types. The next question about any type theory is: what is the general kind of category I can model this sort of thing in, can I prove that a category of syntactic deductions is the initial such category, and if so, isn’t it true that a general model of my type theory is just a structure-preserving functor from that initial model? In more familiar cases, this leads to descriptions of things like free categories with finite products or even free toposes–see Mike Shulman’s sadly incomplete book Categorical Logic from a Categorical Point of View for a number of very edifying examples of this process.
GATs lead to a rather unusual approach, in comparison, because there’s no really familiar kind of category characterized by having a well-behaved notion of “families of objects indexed by another object”. In introducing GATs, Cartmell resolved this question by introducing contextual categories. The contextual category freely (probably, I think there are questions about initiality theorems here) generated by a GAT is literally its category of contexts, such as the context x:\text{Ob},f,g:\text{Hom}(x,x) in the GAT of a category. A morphism from a context \Gamma = x_1:A_1,\ldots,x_n:A_n to a context \Delta = y_1:B_1,\ldots, y_m:B_m is a family of terms t_i : B_i(t_1,\ldots,t_{i-1}), all in context \Gamma. I’m being as fast and loose with notation as I think I can get away with, here; Cartmell’s 1984 paper does this all properly. Anyway, as an example of a morphism of contexts, let \Gamma= x,y:\text{Ob},f:\text{Hom}(x,y),g:\text{Hom}(y,x),\alpha:\text{Hom}(f,f),\beta:\text{Hom}(g,g) then let \Delta=a:\text{Ob},m:\text{Hom}(a,a),\zeta:\text{Hom}(m,m), and define t_1=x,t_2=fgfg, and t_3=\alpha^2*\beta^3*\alpha*\text{id}_g.
This gives a category of contexts and modulo some \alpha-equivalence-type business, it is the free contextual category generated by your GAT. What is a contextual category in general, though? Well, the nLab’s rather nice article on the categorical semantics of dependent type theory defines a contextual category as a kind of category of attributes, which is a discrete fibration E\to B together with a map of fibrations into [the part of] B's codomain fibration [that exists]. Thus every point of E determines an arrow of B and arrows of E determine pullback squares in B. It’s not required that E be a subcategory of B's arrow category, although it seems like it usually is?
The way the category of contexts of a GAT becomes a category with attributes is by letting the fiber of E\to B over some context \Gamma be the set of context extensions \Gamma,x:A for all a. It turns out you can pull back the canonical maps \Gamma,x:A \to \Gamma along any context morphism into \Gamma (using substitution), and that’s that.
On top of the category-with-attributes structure, the objects of a category with contexts have lengths in \mathbb N. There’s a unique object of length 0, the fiber of E\to B over a b of length n consists of objects of length n+1, and every object b of positive length is the domain of a unique map b\to b' in the image of the map from E to the arrow category of B. In other words, the objects form a tree and that tree is equipped with a functor back into B. In the category of contexts of a GAT, the tree structure is determined by context extensions.
The key example of a category with contexts, for Cartmell, was the category of families of sets, whose objects of length n are the set-indexed families of objects of length n-1, and whose objects of length 1 are sets. So a length-2 object is a family of families of sets, and so on. This is the basic category in which GATs have models, which are equivalently contextual-category-morphisms out of the category of contexts of the GAT. (Definition is an exercise.)
However, you can’t help but notice that you’ve never used this category in your life! We certainly don’t implement it in AlgebraicJulia, even though our life is based on GATs. It seems instead that what’s been going on since Cartmell is an amazing amount of work to try to model dependent type theory, i.e. to interpret GATs, in actual normal people categories, or as nearly as possible. At the heart of the difficulty here is that the stratification by object length makes a contextual category much closer to the syntax. Specifically, the canonical pullbacks are easily set up to be strictly functorial, which is important for accurately interpreting a GAT (since the pullbacks correspond to substitution of terms.) If you want to interpret a GAT in plain sets, for instance, then you might feel good since a family of sets over B is equivalent to a function into B…But then you might feel bad because pullbacks in \text{Set} are not strictly functorial.
I don’t know all that much about this post-Cartmell story, but you should read the nLab article. The most important upshot is that every locally cartesian closed category gives rise to a canonical contextual category, thus, is a good place to interpret GATs, by doing various strictifications to its codomain fibration.
I hope that helps clarify some things for some people! A very interesting aspect of this all to me is that we at AlgebraicJulia purport not to really be doing dependent type theory, but instead like to use GATs just as a convenient syntax for nice simple algebraic structures like monoidal categories that just happen to have a bit of dependency structure. I’m not sure whether to think of this as a whole different direction in the application of GATs than what all the people in the industry of constructing contextual categories are up to, or whether everything’s more unified than it looks at first glance. I’d love to hear whether anybody knows or wonders anything about any of this.