0004 Internal languages for models
This RFC is tracked in #1212.
1 Summary
Any pragmatic tool for “programming” inside categorical structures will include a pointful notation to define morphisms (programs), based on variables and function application as in a conventional programming language. Such a notation is the internal language for the categorical structure. This RFC seeks a uniform method to construct the internal languages of different categorical structures, suitable for implementation in CatColab. The technical approach involves a two-level type theory parameterized by a modal double theory.
2 Motivation
Several styles of notation are commonly used to denote a morphism in a categorical structure. Among text-based notations, the most important distinction is between point-free notations, which do not involve “elements” or “variables,” and pointful notations, which do. To illustrate, suppose that f: X \to Y and g: Y \to Z are composable morphisms in a category. Their composite is denoted in point-free notation as g \circ f or f \cdot g, or in pointful notation as |x: X| g(f(x)) (to use a Rust-style programming syntax) or x: X \vdash g(f(x)): Z (to use a type-theoretic syntax).
In a bare category, the most general data that can be composed is a path of morphisms, and there is little practical difference between point-free and pointful notations. However, as more categorical structure is introduced, the difference can become dramatic. As another example—still tiny by practical standards—suppose that f: X \times Y \to W, g: X \to W', and h: W \times W' \to Z are morphisms in a cartesian category. The composite morphism with signature X \times Y \to Z can be written in point-free notation as
(\Delta_X \times 1_Y) \cdot (1_X \times \sigma_{X, Y}) \cdot (f \times g) \cdot h,
which the reader must exert some effort to compile in their head, in contrast to the pointful notation
x : X,\ y : Y \vdash h(f(x, y), g(x)) : Z,
which is just the familiar syntax for composing functions. Besides its familiarity, the key ergonomic advantage of pointful notation is that operations like copying and permuting, which must be explicitly stated in point-free notation, become implicit.
A less obvious benefit of pointful notation is finding canonical forms for morphisms in free categorical structures. Consider again morphisms in a bare category. Using point-free syntax based on the standard biased axioms for a category, a ternary composite of morphisms f, g, and h admits two different expressions, h
\circ (g \circ f) and (h \circ g) \circ f, that denote the same morphism, by the associativity law. Yet, using pointful notation, it is possible to form only one term denoting this morphism, namely x : X \vdash h(g(f(x))): Z. The pointful notation thus gives a canonical form for morphisms in a free category. Of course, in this case, it is just as easy to produce a canonical form without using variables. That’s what the Path data structure in catlog does.
Finding canonical forms becomes more difficult as categorical structure accumulates. For example, let X \xrightarrow{f} Y \xrightarrow{g} Z and X' \xrightarrow{f'} Y' \xrightarrow{g'} Z' be morphisms in a monoidal category. In point-free syntax, two different expressions,
(g \circ f) \otimes (g' \circ f') \qquad\text{and}\qquad (g \otimes g') \circ (f \otimes f'),
denote the same morphism, by the interchange law. Moreover, due to the symmetry of the situation, there is no obvious reason to prefer one over the other. In the pointful notation of a suitable type theory, this symmetry is broken, and there will be a canonical way to denote this morphism, namely
(x, x'): X \otimes X' \vdash (g(f(x)), g'(f'(x'))): Z \otimes Z'.
Intuitively, this term corresponds to the first of the above point-free expressions, whereas the second has no counterpart because forming and applying the tensored operation g \otimes g' is not allowed. This point of view—that type theory is a toolkit to find canonical forms for morphisms—is a theme in Shulman’s lecture notes on categorical logic (Shulman 2016).
In short, among textual notations, pointful notation has both practical advantages, being familiar and ergonomic, as well as theoretical ones, inasmuch as it sometimes leads to canonical forms.
Before moving on, it’s worth acknowledging that point-free notation is not without its own merits. Conveniently for computer implementation, point-free notation can be mechanically extracted for any categorical structure defined in a suitable formal language, such as GATs or double theories. In contrast, while the field of type theory has recurring principles and techniques, designing a type theory remains a fiddly business. Finding the internal language of a new categorical structure—a type theory whose types and terms faithfully denote such categories’ objects and morphisms—is often a research problem in its own right. So, the research problem behind this RFC is that while CatColab has a uniform meta-logic for (parts of) logic at the level of categorical semantics, we now need a uniform approach at the level of type-theoretic syntax.
Not only is point-free syntax readily available for any categorical structure, it is equivariant under categorical duality, whereas pointful notation is intrinsically biased toward the domain of a morphism (its inputs) and also, to a lesser extent, toward cartesian logics, in which variables can be freely duplicated and discarded. The happiest categorical semantics for pointful notation is a free cartesian multicategory or, what is nearly the same, a free cartesian category whose basic morphisms have codomains that are basic objects. The further one departs from this ideal, the more likely standard techniques are to break down. Nevertheless, providing an intuitive pointful syntax seems so indispensable to the vision of CatColab as a family of interoperable programming languages that we cannot neglect to pursue a unified approach.
3 Technical approach
In many traditional type theories, especially those without function types,1 the sorts and operations available to use in contexts and terms are external data that parameterize the type theory. For example, the (mainly pedagogical) type theory for categories is parameterized by a graph (Shulman 2016, sec. 1.2), and the type theory for multicategories is parameterized by a multigraph (Shulman 2016, sec. 2.4.1). In more loaded terminology, such a graph or multigraph is called a signature; its vertices, sorts; and its (multi)edges, function symbols. A key feature of the present type theory will be to internalize the signature, i.e., to make it part of the type theory itself.
In fact, we will need to keep straight three different levels:
- Double theories
- Models of a double theory
- Morphisms in a model, denoted by terms in an internal language for the model.
The first of these levels will be external to the type theory. That is, the present type theory, like the original DoubleTT, is parameterized by a double theory. The second and third levels belong to the type theory itself. Depending on the double theory, models will be categorical structures like categories or multicategories; in fact, since they are finitely presented, such models are given by combinatorial structures like graphs or multigraphs, along with generating equations. So it is free models, internal to this type theory, that play the role of signatures external to traditional type theories.
Models of a double theory are described by a dependent type theory combining standard and specialized rules. The judgmental structure is exactly that of standard dependent type theory. The type theory has record types (equivalent to but more ergonomic than dependent sums) and singleton types (to enable model composition); it does not have dependent products or universes. To this base is added specialized rules for the object and morphisms types of the double theory. All this follows the original DoubleTT, with an important exception to be described shortly.
What is here new are two additional kinds of judgments:
- contexts over an object type, and
- terms in context, or just terms, over a morphism type.
In both simple and dependent type theory, contexts are lists of typed variables, with the list structure belonging to the meta-theory. We are forced depart from this tradition since our internal languages encompass both unary type theories (Shulman 2016, 1) and multi-ary (“simple”) type theories (Shulman 2016, 2); depending on the object type, contexts may or may not be lists. Instead, we rely on the list modality in a modal double theory to supply the list structure needed for multi-ary internal languages. So, again, something usually external to the type theory is internalized. The price paid is that operations like flattening nested lists, usually swept under the meta-theoretic rug, must now be explicitly handled within in the type theory.
Another key design goal is that the type theory for morphisms be cut-free. That is, composition of morphisms should be not a primitive operation but an admissible rule: a meta-theoretic operation derivable from the other rules of the system. Eliminating primitive rules in favor of admissible ones is how type theory can produce canonical forms. Similarly, the type theory will allow constructing lists of morphism terms, but not lists of morphism generators. So, a major difference with the original DoubleTT is that point-free operations on morphisms like f \cdot g and [f, g] are not part of the type theory.
4 Mathematical specification
4.1 Double theories
For the purposes of this RFC, we reformulate a double theory as a structure interpolating between an arbitrary virtual double category (VDC) and a representable VDC (equivalent to a genuine double category).
Definition. A virtual double category is almost representable if for every multicell, every subpath of its domain has a composite.
Equivalently, by the universal property of composites, a VDC is almost representable if every multicell factors through a composition cell and, moreover, every composition cell can be factored arbitrarily as a tight composite of binary and nullary composition cells. In such a VDC, the analysis of an arbitrary multicell reduces to three simpler cases: (1) unary cells, as in an ordinary double category; (2) binary composition cells; and (3) nullary composition cells, i.e., extension cells for units. This case analysis will appear directly the rules of our type theory.
Definition. A double theory is an almost representable virtual equipment, i.e., an almost representable VDC with units and restrictions.
In practice, double theories are finitely presented, but formalizing such presentations is a problem for future work.
Definition. A model of a double theory \mathbb{T} is a functor of VDCs \mathbb{T} \to \mathbb{S}\mathsf{et} that preserves restrictions (but not composites!); equivalently, a model of \mathbb{T} is a functor of virtual equipments \mathbb{T} \to \mathbb{C}\mathsf{at}, i.e., a normal functor of VDCs that preserves restrictions (but not composites of arity greater than 1).
We will use the term “double theory” somewhat loosely to refer to any object with at least the structure postulated above. A simple double theory is a double theory with exactly that structure. The only other double doctrine that we will treat is modal double theories. The list modalities will be crucial for extracting familiar-looking internal languages for “multi-ary” categorical structures like multicategories, monoidal categories, PROs, and generalizations thereof.
4.1.1 Modal theories
TODO
4.1.2 List modalities
TODO
4.2 Outer type theory: models
The outer type theory, a dependent type theory, has the standard judgments for contexts, types in context, and terms in context, as well as for equalities between types and between terms. We are agnostic as to whether substitutions are implicit or explicit. Moreover, the outer type theory has dependent record types and singleton types, though do not actually need either for present purposes. For details, see RFC-0002 and references therein.
We state the special rules for DoubleTT in full, as there are changes from the original spec. Let \mathbb{T} be a double theory.
4.2.1 Object types
Object type former: For each object \mathcal{X} in the double theory, there is a type of objects of type \mathcal{X}:
Operation application:
4.2.2 Morphism types
Morphism type former: For each proarrow P: \mathcal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathcal{Y} in the double theory, there is a type of generating morphisms of type P, depending on a pair of objects of types \mathcal{X} and \mathcal{Y}:
In particular, each object \mathcal{X} in \mathbb{T} has an identity proarrow \operatorname{id}_{\mathcal{X}}: \mathcal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathcal{X}, which we denote \operatorname{Hom}_{\mathcal{X}} and call the Hom type on \mathcal{X}. Thus the following rule is derivable:
4.2.3 List modality
Formation rules:
Computation rule, monad unit:
Computation rules, monad multiplication:
We follow tradition in defining the list monad, including the monad unit (singleton list) and monad multiplication (flattening), by induction. For practical purposes, this presentation is not very important; we’ll likely implement lists as arrays rather than linked lists. What is important is that the list operations compute: by iteratively applying the computation rules, any applications of \mu_{\mathcal{X}} and \eta_{\mathcal{X}} in terms can be eliminated.
4.3 Inner type theory: morphisms
4.3.1 Judgments
The inner type theory introduces two new judgments, both depending on contexts from the outer type theory.
Contexts: Presupposing that \mathcal{X} is an object type of \mathbb{T} and that \Gamma \vdash X: \operatorname{Ob}_{\mathcal{X}} is an object, the judgment
\Gamma \mid u: X
asserts that “u is an (inner) context of type X, in (outer) context \Gamma”.
Terms: Presupposing that P: \mathcal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathcal{Y} is a morphism type of \mathbb{T}, that \Gamma \vdash X: \operatorname{Ob}_{\mathcal{X}} and \Gamma \vdash Y: \operatorname{Ob}_{\mathcal{Y}} are objects, and that \Gamma \mid u: X is a context of type X, the judgment
\Gamma \mid u: X \vdash_P t: Y
asserts that “t is an (inner) term of type P, in context \Gamma \mid u : X”.
When \mathcal{X} = \mathcal{Y} and P = \operatorname{Hom}_{\mathcal{X}}, the subscript P on the turnstile can be dropped.
In addition, there are judgments of equality between inner contexts and between inner terms.
4.3.2 Contexts
Contexts are typically defined inductively to be lists of typed variables (i.e., variable-type pairs), but the inner contexts of this type theory are constructed differently. First of all, contexts need not be lists at all; contexts are unary by default. Only over an object type of form \mathrm{List}\mathcal{X} can we build contexts like
\Gamma \mid [x_1, x_2, x_3] : [X_1, X_2, X_3],
where the x_i are variables and the X_i are objects of type \mathcal{X} in context \Gamma. Especially in examples, we will be lulled into writing this more conventionally as
\Gamma \mid x_1: X_1,\, x_2: X_2,\, x_3: X_3,
but we caution that the latter has no official meaning in this type theory; it is only syntactic sugar for the former.
Context formation:
where x is a variable assumed not to appear in the outer context \Gamma.
Operation application:
4.3.2.1 Lists
Formation rules:
where in the latter rule, the variables appearing anywhere in u and \underline{u} are assumed to be disjoint.
Computation rule, monad unit:
Computation rules, monad multiplication: analogous to computation rules for list modality above.
4.3.3 Terms
Identity rule:
where x is a variable assumed not to appear in the outer context \Gamma. This rule can be interpreted as applying the nullary composition cell out of \mathcal{X}.
Composition rule:
where the first premise tacitly includes the assumption that the proarrows P and Q have a composite. This rule can then be interpreted as applying the binary composition cell out of P and Q.
Operation application: for each unary cell \alpha in \mathbb{T} as on the left, there is a rule as on the right:
Two special cases are worth recording. First, for each arrow F: \mathcal{X} \to \mathcal{Y} in \mathbb{T}, there is an identity cell \operatorname{id}_F = \operatorname{Hom}_F, whose application to a term t we abbreviate as F(t). With this notation, there is a derived rule:
Second, each niche in \mathbb{T} as on the left can be filled with restriction cell with domain P(F,G): \mathcal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathcal{Y}. Leaving the application of restriction cells to terms implicit, there is a derived rule:
Universal property of restriction: for each niche in \mathbb{T} as on the left, there is a rule as on the right:
Consequently, terms \Gamma \mid u: X \vdash_{P(F,G)} t: Y and \Gamma \mid F(u): F(X) \vdash_P t: G(Y) are in bijection.
Destructuring: TODO
4.3.3.1 Lists
TODO
4.4 Meta-theoretic results
TODO: Cut admissibility
5 Examples
TODO
6 Rationale and alternatives
6.1 Bespoke internal languages
An obvious alternative would be to apply the usual methodology: for each categorical structure of interest, find its internal language and produce a bespoke implementation of that type theory. In this approach, every logic in CatColab requiring an internal language would have its own custom text frontend. From the “semantics first” perspective of CatColab, this approach is not unreasonable. By carefully separating the textual syntax, the data structures for models and morphisms to which the syntax compiles, and the analyses that can be run on those data structures, we could hope to retain many of the benefits of a uniform meta-logic, at least outside the frontend. Indeed, this has been our intended approach to point-and-click graphical editors for graphs, Petri nets, and so forth, whose variety seems to defy systemization. Yet I would still rather see such an approach to internal languages as a fallback option, being at best a pragmatic compromise to the vision of CatColab as an interoperable family of modeling and programming languages.
6.2 String diagrams
Type theory is one methodology to find canonical forms for morphisms, but it’s not the only one. Among applied category theorists, the usual recipe to produce canonical forms for morphisms in monoidal categories is to use string diagrams (Selinger 2010) or their combinatorial counterparts, wiring diagrams (Patterson et al. 2020). Incidentally, string diagrams are a point-free syntax, demonstrating that pointfulness is not a necessary property of normalizing syntax.
From our “semantics first” perspective, string diagrams are not so much an alternative to type-theoretic textual notation as a complement to it. In CatColab, it is the categorical structures that are primary; both graphical and textual syntaxes should be available. Making multiple syntaxes work together seamlessly poses architectural challenges. This document, however, is solely about textual syntax.
7 Prior art
7.1 Split contexts
TODO
7.2 Two-level type theories
TODO
References
Footnotes
Type theories with function types and enough inductive types to generate standard data types such as the booleans and natural numbers commonly omit a parameterizing signature entirely, under idea that all other types and operations should be built out of the provided ones. In this RFC, however, we are exclusively concerned with type theories that do not have function types, i.e., with the internal languages of categorical structures that are not closed.↩︎