diff --git a/rfc/0009.md b/rfc/0009.md new file mode 100644 index 000000000..fc3f18c3f --- /dev/null +++ b/rfc/0009.md @@ -0,0 +1,117 @@ +--- +title: | + `0009` Instances in tt +author: Kevin Carlson +date: 2026-05-08 +bibliography: _references.bib +--- + +{{< include _macros.qmd >}} + +::: {.callout-note} +### RFC status + +This RFC is essentially about +[#1246](https://github.com/ToposInstitute/CatColab/pull/1246). +::: + +## Summary + +The vision for CatColab is to integrate theories, their +models, and their instances into one general system; the purpose of this +RFC is to open a plan on extending DoubleTT to include instances, +especially to allow for gluing of instances via instantiation, +as we already support for models of discrete double theories. + +## Instances are diagrams + +As in `catlog::dbl`, we here implement instances basically via diagrams, +that is, an instance $I:1\nrightarrow X$ of a model $X$ can be seen as +a model morphism $D: Y\to X$ such that the discrete opfibration over $X$ +freely generated by $D$ coincides with the Grothendieck construction $\int I.$ +See my and Evan's [paper](https://arxiv.org/abs/2510.08861) on instances for +details on this relationship. However, since a key desideratum is to be able +to glue instances together using the specialization types of DoubleTT, we do +need the type theory to understand that a diagram is really generating a discrete +opfibration, not to leave it inert. + +## Diagrams are pseudo-terms + +In the current design, DoubleTT interprets a diagram $I$ over $X$ as a special +kind of term of $X$; that is, we are adding to the type theory a new judgment +form $I :_D X$ saying that $I$ is a term of $X$ in the diagram sense. +These diagrammatic terms are easier to produce than the basic terms of +DoubleTT, where for instance there are no closed terms of types corresponding +to models. Specifically, for every object type `ot` in our theory, and +every declaration `Q : ot` in our model `X`, we provide a new type +`Over(Q)`, whose terms are intended to be all the things that might lie over `Q` +in any `X`-instance, and then we can build diagrams over `X` using generators +from these types, eg a diagram whose sole generator is `q : Over(Q)` +corresponds to the $X$-instance freely generated by an element over `Q`. + +## This changes contexts + +This means that contexts in the augmented DoubleTT now have variables of +two kinds; for instance you might have $x : X , I :_D X, y : Y$ as a context. +You can see this change reflected in `tt::context`, where basically `lookup` +ignores diagram-type variables and `lookup_diagram` ignores ordinary variables. + +## Specialization uses the discrete opfibration property + +Suppose my model is, say, the schema for graphs `Gr`, and I want to glue together +two diagrams, say two copies of the walking edge `Edge : Instance(Gr) = [e : Over(E)]` +(This is notional syntax, not quite what you type in .dbltt files), +aiming to produce the walking path of length 2. Well, `Edge` has no names available +for its vertices! We want to be able to declare something like +`Path2 : Instance(Gr) = [e1 : Edge, e2 : Edge] & .tgt(e1) = .src(e2)`. +So, we allow for almost exactly that, having the elaborator construct the implicit elements +of a diagram implied by the discrete opfibration condition. Currently we treat the +problem of infinite instances without any neurons, just iterating out to a +fixed number of steps. More urgently, I suspect the algorithm as of May 8 is literally +wrong when the model has equations in it, TBD. + +## Text front-end + +In `catlog/examples/tt/test_instances.dbltt`, you can see some cases of the intended +usage. The main example of substance is this: +``` +diagram I2 : @Instance(WeightedGraph) := [ + v1 : @over .V, + v2 : @over .V, + w : @over .Weight, + we : Edge & [.src(e) := v1, .tgt(e) := v2, .weight(e) := w], + wf : Edge & [.src(e) := v2, .tgt(e) := v1, .weight(e) := w] +] +``` + +Here `Edge` is the walking edge, as above, though now considered as a *weighted* graph. +Thus `I2` is the weighted graph generated by two edges in opposite directions and with +equal weights. The elaborator strips out the `@Instance` decoration once it adds +`I2` as a diagram-kind variable to the context, while elaborating `Edge` into a +genuine edge, whose vertices *canonically* have the sames `src(e)` and `tgt(e)`. So +the evaluation syntax in those names is made of cardboard; we haven't introduced a +new kind of term or anything to handle it at this point. + +## Model generation + +`tt:modelgen` builds a `DisreteDblModelDiagram` from a `diagram` declaration and +validates it using the machinery from `catlog::dbl`. + +## Questions and to-dos + +- Is this special term kind a good idea? Is it normal? How do plain terms of + models relate to instancey terms? Could the latter subsume the former? I had initially + been imagining `Instance(X)` as a pseudo-universe type with its terms, the instances, + themselves types, since if you think of them as models they feel typey, but that didn't + seem to work as well, not least because we don't really want universes in our type theory, + so we'd be faking a bit. +- How will this interact with Evan's RFC on internal languages, incorporating terms of + models for specifying their morphisms? I kind of hope they're largely orthogonal but they're + both substantial modifications to the type theory, and it's not entirely clear to me that + Evan's work is even non-breaking for DoubleTT. It's also notable that Evan doesn't really use + terms and substitutions at the type level in his RFC. What's up with that vis a vis this? +- Next up and low risk is the notebook elaborator, so we can put these into the app. +- High priority but higher risk is to get thinking about modal instances. We don't understand these + real well mathemaically. +- Mostly blue-sky but exciting to wonder about: what kind of migrations on instances are induced by substitutions + between model types?