ModalTT: A Type Theory for Modal Virtual Double Theories
## Overview {#slide-1 data-menu-title="Overview"} I will be talking about a type theory and accompanying DSL for specifying **modal virtual double theories**.
. . . Some familiarity with virtual double categories (VDCs) will be assumed. Very little type theory background will (hopefully) be required. . . .
This project is ongoing and there is still much work to be done on both the implementation and type theory. Please be gentle with me. :) ## Outline {#slide-2 data-menu-title="Outline"} The next 50 minutes of our lives should look roughly as follows: . . . 1. Motivate the software problem this project is attempting to solve. . . . 2. Outline some past work that motivated our approach. . . . 3. Briefly demo our DSL. . . . 4. Describe our type theory for modal virtual double theories. . . . 5. (Maybe questions? Who can say what the world will look like in an hour.) # Motivation
## DoubleTT and categorical logic {#slide-3 data-menu-title="DoubleTT: Theories and Models"} [CatColab]{.define} [@catcolab] is a collaborative modelling platform based on categorical logic. . . . [DoubleTT]{.define} [@doublett] is a component of CatColab which facilitates model composition using a type theory for models of double theories. . . . The **theory** for a particular logic defines the "shape" of its models. Formally: . . . * a [theory]{.define} is a fibrational VDC (possibly unital, possibly with loose composites) equipped with zero or more double monads, called modalities. . . . * a [model]{.define} $M$ of a theory $\mathbb{T}$ is a restriction-preserving functor $$M : \mathbb{T} \to \mathbb{S}\mathrm{pan}$$ ## DoubleTT and categorical logic {#slide-4 data-menu-title="Example Theories (1)"} [Example:]{.define} the theory of categories is a unital VDC with a single object and no (nonunital) tight/loose arrows. . . .
[Example:]{.define} the theory of monoidal categories is a unital VDC, equipped with "the" list monad $\mathrm{List}$, generated by an object $X$ and a tight morphism $$\otimes: \mathrm{List}(X) \to X$$ (These are equipped with the usual axioms making $\otimes$ a monoidal product.) ## DoubleTT and categorical logic {#slide-5 data-menu-title="Example Theories (2)"} [Example:]{.define} the theory of promonads is a unital VDC with an object $X$, a proarrow $P : X \proto X$ such that the loose composite $P \odot P$ is defined and is equal to $P$, and a virtual cell $\theta$: ```{.tikzcd} \begin{tikzcd}[column sep=1em] & X & \\ X & {} & X \arrow[equals, from=1-2, to=2-1] \arrow["\theta"{description}, draw=none, from=1-2, to=2-2] \arrow[equals, from=1-2, to=2-3] \arrow["P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-3] \end{tikzcd} ``` . . . such that the cell equalities below are satisfied: ```{.tikzcd} \begin{tikzcd} & X & X \\ X & X & X \\ X && X \arrow[""{name=0, anchor=center, inner sep=0}, "P"{inner sep=.8ex}, "\shortmid"{marking}, from=1-2, to=1-3] \arrow[equals, from=1-2, to=2-2] \arrow[equals, from=1-3, to=2-3] \arrow[equals, from=2-1, to=1-2] \arrow[""{name=1, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow[equals, from=2-1, to=3-1] \arrow[""{name=2, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-2, to=2-3] \arrow[equals, from=2-3, to=3-3] \arrow[""{name=3, anchor=center, inner sep=0}, "{P\odot P}"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \arrow["\theta"{description}, draw=none, from=1-2, to=1] \arrow["{1_P}"{description}, draw=none, from=0, to=2] \arrow["{\mathrm{comp}}"{description}, draw=none, from=2-2, to=3] \end{tikzcd} \hspace{1em} = \hspace{1em} \begin{tikzcd} X & X \\ X & X \arrow[""{name=0, anchor=center, inner sep=0}, "P"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow[equals, from=1-1, to=2-1] \arrow[equals, from=1-2, to=2-2] \arrow[""{name=1, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow["{1_P}"{description}, draw=none, from=0, to=1] \end{tikzcd} \hspace{1em} = \hspace{1em} \begin{tikzcd} X & X & \\ X & X & X \\ X && X \arrow[""{name=0, anchor=center, inner sep=0}, "P"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow[equals, from=1-1, to=2-1] \arrow[equals, from=1-2, to=2-2] \arrow[equals, from=1-2, to=2-3] \arrow[""{name=1, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow[equals, from=2-1, to=3-1] \arrow[""{name=2, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-2, to=2-3] \arrow[equals, from=2-3, to=3-3] \arrow[""{name=3, anchor=center, inner sep=0}, "P \odot P"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \arrow["{1_P}"{description}, draw=none, from=0, to=1] \arrow["\theta"{description}, draw=none, from=1-2, to=2] \arrow["{\mathrm{comp}}"{description}, draw=none, from=2-2, to=3] \end{tikzcd} ``` ## Specifying custom theories {#slide-6 data-menu-title="Specifying Custom Theories: Goal"} Currently the theories available in DoubleTT are constructed directly in Rust, rather than a dedicated language. Users are limited to a small handful of pre-defined options unless they manually introduce their own using CatColab's internal data structures. . . . [Goal:]{.define} allow the user to easily define their favorite theory in a small DSL by . . . 1. specifying a signature (generators) . . . 2. specifying axioms (relations) . . . 3. with a guarantee that the DSL only accepts theories which are well-defined (without requiring any internal consistency checks later). ## Specifying custom theories {#slide-7 data-menu-title="Specifying Custom Theories: Idea"} [Idea:]{.define} annotate the user-specified theory with types, such that a theory which successfully typechecks is always valid. . . .
[Observation:]{.define} user-defined axioms can equate any pair of cells with the same boundary, so this amounts to a type theory for the internal language of VDCs. . . .
[Remark:]{.define} as we saw for the theory of promonads, theories may also equate (pro)arrows, so even checking compatibility of cell boundaries is nontrivial. # Past Work
## An internal logic of VDCs {#slide-8 data-menu-title="An Internal Logic of VDCs"} Hayato Nasu's [past work](https://arxiv.org/pdf/2410.06792) [@nasu] on a type theory for (fibrational, cartesian) VDCs guided the early stages of this project. . . . [Idea:]{.define} describe a pointful syntax [@doublett; @shulman] for the constructs in a VDC, which reduces equivalent (via universal property) structures to a single normal form. ## An internal logic of VDCs {#slide-9 data-menu-title="VDC-Syntax Correspondence"} The correspondence between constructs in a VDC and the syntax of Nasu's type theory is outlined below:
| VDC Construct | Syntactic Form | Example | |-------|-----------------------|----------| | [Object]{.define} | Type | $X \Leftrightarrow X \text{ type}$ | | [Product]{.define} | Context | $\prod_{i=1}^n X_i \Leftrightarrow x_1 : X_1, \dots, x_n : X_n \text{ ctx}$ | | [Morphism]{.define} | Term | $s : \Gamma \to X \Leftrightarrow \Gamma \vdash s : X$ | | [Proarrow]{.define} | Protype | $P :\Gamma \proto \Delta \Leftrightarrow \Gamma ; \Delta \vdash P(s ; t) \text{ protype}$ | | [Proarrow path]{.define} | Procontext | $\Gamma_0 \proto \Gamma_1 \proto \cdots \proto \Gamma_n \Leftrightarrow \rho_1 : P_1, \dots, \rho_n : P_n \text{ proctx}$ | | [(Globular) Cell]{.define} | Proterm | $\mu : P_1, \dots, P_n \proto Q \Leftrightarrow \Gamma_0 ; \dots ; \Gamma_n \vert \rho_1 : P_1, \dots, \rho_n : P_n \vdash \mu : Q$ | : {tbl-colwidths="[25,25,70]"} ## An internal logic of VDCs {#slide-10 data-menu-title="Proterm Example (Identity)"} #### Example The (tight) identity cell ```{.tikzcd} \begin{tikzcd} X & Y \\ X & Y \arrow[""{name=0, anchor=center, inner sep=0}, "P"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow[equals, from=1-1, to=2-1] \arrow[equals, from=1-2, to=2-2] \arrow[""{name=1, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow["{1_P}"{description}, draw=none, from=0, to=1] \end{tikzcd} ``` . . . ...is represented by the proterm $$x : X, y : Y \vert p : P(x ; y) \vdash p : P(x ; y)$$ ## An internal logic of VDCs {#slide-11 data-menu-title="Proterm Example (Composite)"} #### Example The virtual composite cell ```{.tikzcd} \begin{tikzcd} X & Y & Z \\ {X'} & {Y'} & {Z'} \\ {X''} && {Z''} \arrow[""{name=0, anchor=center, inner sep=0}, "M"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow["f"', from=1-1, to=2-1] \arrow[""{name=1, anchor=center, inner sep=0}, "N"{inner sep=.8ex}, "\shortmid"{marking}, from=1-2, to=1-3] \arrow["g"{description}, from=1-2, to=2-2] \arrow["g", from=1-3, to=2-3] \arrow[""{name=2, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow["s"', from=2-1, to=3-1] \arrow[""{name=3, anchor=center, inner sep=0}, "Q"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-2, to=2-3] \arrow["t", from=2-3, to=3-3] \arrow[""{name=4, anchor=center, inner sep=0}, "R"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-3] \arrow["\alpha"{description}, draw=none, from=0, to=2] \arrow["\beta"{description}, draw=none, from=1, to=3] \arrow["\gamma"{description}, draw=none, from=2-2, to=4] \end{tikzcd} ``` . . . ...is represented by the proterm $$ \begin{aligned} x : X, y : Y, z : Z \vert m : M(x ; y), n : N(y; z) \vdash\\ \gamma (\alpha(m), \beta(n)): R(s(f(x)) ; t(g(z))) \end{aligned} $$ ## An internal logic of VDCs {#slide-12 data-menu-title="Proterm Restrictions (1)"} #### Restrictions For this type theory to model the internal language of **fibrational** VDCs it needs to capture restriction cells and their universal property. Given a proarrow $P : Y_0 \proto Y_1$ and tight morphisms $f_i : X_i \to Y_i$, the protype $$ x_0 : X_0 ; x_1 : X_1 \vdash P(f_0(x_0), f_1(x_1)) $$ represents the restriction of $P$ along $f_0$ and $f_1$. ## An internal logic of VDCs {#slide-13 data-menu-title="Proterm Restrictions (2)"} #### Restrictions We recover the corresponding restriction cell ```{.tikzcd} \begin{tikzcd} {X_0} & {X_1} \\ {Y_0} & {Y_1} \arrow[""{name=0, anchor=center, inner sep=0}, "{P(f_0,f_1)}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow["{f_0}"', from=1-1, to=2-1] \arrow["{f_1}", from=1-2, to=2-2] \arrow[""{name=1, anchor=center, inner sep=0}, "P"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow["{\mathrm{rest}}"{description}, draw=none, from=0, to=1] \end{tikzcd} ``` with the proterm $$ x_0 : X_0, x_1 : X_1 \vert p : P(f_0(x_0), f_1(x_1)) \vdash p : P(f_0(x_0), f_1(x_1)), $$ since the tight identity cell of a restriction proarrow corresponds uniquely with the restriction cell via the universal property. ## An internal logic of VDCs {#slide-14 data-menu-title="Loose Proterm Composition (1)"} #### (Loose) Composition The type theory can be extended with type formation, introduction, and elimination rules for loose composites. . . . The universal property for composites says that each cell $\mu$ induces a unique $\widetilde{\mu}$ such that ```{.tikzcd} \begin{tikzcd} {X_0} & {X_i} & {X_{i+1}} & {X_{i+2}} & {X_n} \\ {Y_0} &&&& {Y_n} \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow[from=1-1, to=2-1] \arrow["{P_1}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-2, to=1-3] \arrow["{P_2}", from=1-3, to=1-4] \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=1-4, to=1-5] \arrow[from=1-5, to=2-5] \arrow[""{name=0, anchor=center, inner sep=0}, "Q"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-5] \arrow["\mu"{description}, draw=none, from=1-3, to=0] \end{tikzcd} ``` ## An internal logic of VDCs {#slide-15 data-menu-title="Loose Proterm Composition (2)"} #### (Loose) Composition The type theory can be extended with type formation, introduction, and elimination rules for loose composites. ...is equal to the virtual composite ```{.tikzcd} \begin{tikzcd} {X_0} & {X_i} & {X_{i+1}} & {X_{i+2}} & {X_n} \\ {X_0} & {X_i} && {X_{i+2}} & {X_n} \\ {Y_0} &&&& {Y_n} \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow[equals, from=1-1, to=2-1] \arrow["{P_1}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-2, to=1-3] \arrow[equals, from=1-2, to=2-2] \arrow["{P_2}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-3, to=1-4] \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=1-4, to=1-5] \arrow[equals, from=1-4, to=2-4] \arrow[equals, from=1-5, to=2-5] \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-2] \arrow[from=2-1, to=3-1] \arrow[""{name=0, anchor=center, inner sep=0}, "{P_1\odot P_2}"{inner sep=.8ex}, "\shortmid"{marking}, from=2-2, to=2-4] \arrow["\dots"{inner sep=.8ex}, "\shortmid"{marking}, from=2-4, to=2-5] \arrow[from=2-5, to=3-5] \arrow[""{name=1, anchor=center, inner sep=0}, "Q"'{inner sep=.8ex}, "\shortmid"{marking}, from=3-1, to=3-5] \arrow["{\mathrm{comp}}"{description, pos=0.3}, draw=none, from=1-3, to=0] \arrow["{\widetilde{\mu}}"{description}, draw=none, from=0, to=1] \end{tikzcd} ``` ## An internal logic of VDCs {#slide-16 data-menu-title="Loose Proterm Composition (3)"} #### (Loose) Composition Like restriction, we encode the universal property in the internal language using a normal form. Namely, the $\beta$/$\eta$-reduction rules (judgments relating a type's constructor(s) and eliminator(s)) for composites precisely capture this universal property. ## An internal logic of VDCs {#slide-17 data-menu-title="Internal Logic Extensions"} #### Extensions Nasu's type theory offers a strong foundation, but it lacks some characteristics that are important to our use case: . . . 1. **Rigid signature:** generator cells cannot map into a restriction or unit proarrow, for instance. . . . 2. **Missing modalities:** virtual double monads are not supported by the type theory, which are essential for defining many important doctrines. . . . 3. **Challenging to implement:** the type theory is not designed with algorithmic typechecking in mind. # ModalTT DSL
## ModalTT {#slide-18 data-menu-title="ModalTT"} To address the problems outlined above, we have adapted Nasu's type theory in a number of ways: . . . 1. Our signatures stratify VDC constructs into different syntactic categories to get a more expressive range of legal generators. . . . 2. We introduce first class modality application into the syntax, without compromising the normal forms of (pro)terms. . . . 3. Our type theory uses an ordered linear logic [@type_for_mem_alloc; @ordered_linear_logic_and_apps] to describe the resource-sensitivity and order-sensitivity of proterms. Loose composition reduces to the fuse operator. ## ModalTT {#slide-19 data-menu-title="ModalTT: DSL (Signature)"} #### DSL for theory specification Users specify the generators (objects, tight/loose arrows, and cells) of their theory: . . . **Objects** ``` obj X obj [Y, Z] ``` . . . **Arrows and proarrows** ``` fun f : X -> Y pro P : X => Y ``` . . . **Cells** ``` cell α : [P, Q] => (List R) | f -> id Y ``` ## ModalTT {#slide-20 data-menu-title="ModalTT: DSL (Axioms)"} #### DSL for theory specification Users can declare equalities of proarrows and of proterms (virtual cells), which define the axioms of the theory: . . . **Proarrow Axioms** ``` pro_axiom P := P * P ``` . . . **Proterm Axioms** (this is where the magic happens) ``` -- Promonad axioms axiom [x0 : X, x1 : X] | [p : P[x0, x1]] |- θ (x0) * p := p axiom [x0 : X, x1 : X] | [p : P[x0, x1]] |- p := p * θ (x1) ``` . . . ``` -- Can apply the list monad or use its (primitive) structure proterms axiom [x : X, y : Y] | [p : (List P)[x, y]] |- μ List [(List (η List P)) [p]] := p ``` . . . ``` -- Loose composites are destructured via let binding (more on this soon) axiom [x0 : X, x1 : X] | [...] |- let ([p : P[x0, x1], q : Q[x1, x2]] = α [...] * β [...]) in γ[p, q] := ... ``` ## [demo · ModalTT]{.kicker}(This is where Bryce will do The Demo™) {.video-slide .center}
(if he is not already doing The Demo™ you should politely remind him to do The Demo™)
# ModalTT Type Theory## ModalTT {#slide-22 data-menu-title="ModalTT: Type Theory"} #### Type theory We adapt Nasu's type theory by introducing modalities and broadening the expressive power of the generator symbols. To match the implementation, we also rely less heavily on substitution (which is badly behaved in the presence of non-syntactic equalities.) ## ModalTT {#slide-23 data-menu-title="ModalTT: Signature (1)"} #### Signature The signature $\Sigma$ determines the structures of a theory $\mathbb{T}_\Sigma$ by specifying finite sets of generators: * Object symbols $\mathcal{T}_\Sigma$ * Arrow symbols $\mathcal{F}_\Sigma$ * Proarrow symbols $\mathcal{P}_\Sigma$ * Cell symbols $\mathcal{C}_\Sigma$ * Modality symbols $\mathcal{M}_\Sigma$ ## ModalTT {#slide-24 data-menu-title="ModalTT: Signature (2)"} #### Signature These generator symbols are closed under modal application (the sets of arrows and cells are also populated with the monad structure for each $L \in \mathcal{M}_\Sigma$). . . . The complete sets of arrows (resp. proarrows) are then generated from the modal closures by including identities (resp. loose units) and composites (resp. loose composites). ## ModalTT {#slide-25 data-menu-title="ModalTT: Typing Judgments"} #### Typing Judgments $$ \begin{aligned} \text{Type} & ::= X \text{ type}\\ \text{Context} & ::= \Gamma \text{ ctx}\\ \text{Term} & ::= \Gamma \vdash s : X\\ \text{Protype} & ::= \Gamma_0 ; \Gamma_1 \vdash P \text{ protype}\\ \text{Procontext} & ::= \Gamma_0 , \dots , \Gamma_n \vert \Omega \text{ proctx}\\ \text{Proterm} & ::= \Gamma_0, \dots, \Gamma_n \vert \Omega \vdash \mu : P \end{aligned} $$ ## ModalTT {#slide-26 data-menu-title="ModalTT: Types"} #### Types A type is (just) an object generated by the signature:
```{.mathpar .nostretch scale="3"} \inferrule* {X \in \widetilde{\mathcal{T}}_\Sigma} {X \text{ type}} ``` ## ModalTT {#slide-27 data-menu-title="ModalTT: Term Contexts (Grammar)"} #### Term Contexts: Grammar $$ \begin{aligned} x &\in \mathrm{Var}_{\mathrm{Type}}\\ X &\in \widetilde{\mathcal{T}}_\Sigma\\ \Gamma &\in \mathrm{Context} ::= (x : X) \end{aligned} $$ [Note:]{.define} our theories are not necessarily cartesian, so our (term) contexts are unary [@shulman], containing a single variable binding. ## ModalTT {#slide-28 data-menu-title="ModalTT: Term Contexts (Judgments)"} #### Term Contexts: Typing Judgment
```{.mathpar .nostretch scale="3"} \inferrule* {X \text{ type} \\ x \in \mathrm{Var}_\mathrm{Term}} {(x : X) \text{ ctx}} ``` ## ModalTT {#slide-29 data-menu-title="ModalTT: Terms (Grammar)"} #### Terms: Grammar $$ \begin{aligned} x &\in \mathrm{Var}_\mathrm{Term}\\ f &\in \widetilde{F}_\Sigma\\ s &\in \mathrm{Term} ::= x \vert f(s) \end{aligned} $$ ## ModalTT {#slide-30 data-menu-title="ModalTT: Terms (Judgments)"} #### Terms: Typing Judgments
```{.mathpar} \inferrule* {\strut} {(x : X) \vdash x : X} ```
```{.mathpar} \inferrule* {f \in \widetilde{\mathcal{F}}_\Sigma(X, Y) \\ \Gamma \vdash s : X} {\Gamma \vdash f(s) : Y} ``` ## ModalTT {#slide-31 data-menu-title="ModalTT: Term Substitution"} #### Terms: Substitution Terms are equipped with a meta-theoretic variable substitution, defined in the obvious way: $$ t[s/x] := \begin{cases} s & \text{if } t = x\\ f(t'[s/x]) & \text{if } t = f(t') \end{cases} $$ (As usual, we assume that $x$ is not a variable in $s$ to avoid variable capture.) ## ModalTT {#slide-32 data-menu-title="ModalTT: Protypes (Grammar)"} #### Protypes: Grammar $$ \begin{aligned} s_0, s_1 & \in \mathrm{Term}\\ P & \in \hat{\mathcal{P}}_\Sigma\\ \underline{P} &\in \mathrm{Protype} ::= P(s_0, s_1) \end{aligned} $$ ## ModalTT {#slide-33 data-menu-title="ModalTT: Protypes (Judgments)"} #### Protypes: Typing Judgments
```{.mathpar} \inferrule* {P \in \widetilde{\mathcal{P}}_\Sigma(X, Y) \\ \Gamma_0 \vdash s_0 : X \\ \Gamma_1 \vdash s_1 : Y} {\Gamma_0 ; \Gamma_1 \vdash P(s_0, s_1) \text{ protype}} ```
```{.mathpar} \inferrule* {\Gamma_0 \vdash s_0 : X \\ \Gamma_1 \vdash s_1 : X} {\Gamma_0 ; \Gamma_1 \vdash \mathrm{unit}_X(s_0, s_1) \text{ protype}} ```
```{.mathpar} \inferrule* {\Gamma_0 ; \Gamma_1 \vdash P(s_0, s_1) \text{ protype} \\ \Gamma_1 ; \Gamma_2 \vdash Q(s_1, s_2) \text{ protype} } {\Gamma_0 ; \Gamma_2 \vdash (P \odot Q)(s_0, s_2) \text{ protype}} ``` ## ModalTT {#slide-34 data-menu-title="ModalTT: Procontexts (Grammar)"} #### Procontexts: Grammar For $n \geq 0$: $$ \begin{aligned} \Gamma_i &\in \mathrm{Context}\\ \underline{P_i} &\in \mathrm{Protype}\\ p_i &\in \mathrm{Var}_\mathrm{Proterm}\\ \overline{\Gamma} \vert \Omega &\in \mathrm{Procontext} ::= \Gamma_0, \dots, \Gamma_n \vert p_1 : \underline{P_1}, \dots, p_n : \underline{P_n} \end{aligned} $$ [Note:]{.define} both components of our procontexts are *ordered* (in the sense of ordered linear^[The term context is *almost* linear, but bindings can be dup'ed until a proterm variable consumes a subsequent binding.] logic [@type_for_mem_alloc; @ordered_linear_logic_and_apps]). ## ModalTT {#slide-35 data-menu-title="ModalTT: Procontexts (Judgments)"} #### Procontexts: Typing Judgments
```{.mathpar} \inferrule* {\Gamma \text{ ctx}} {\Gamma \vert \cdot \text{ proctx}} ```
```{.mathpar} \inferrule* {\Gamma_0, \dots, \Gamma_n \vert p_1 : P_1(s_0, s_1), \dots, p_n : P_n(s_{n-1}, s_n) \text{ proctx} \\ \Gamma_n ; \Gamma_{n + 1} \vdash P_{n+1}(s_n, s_{n+1}) \text{ protype}} {\Gamma_0, \dots, \Gamma_{n+1} \vert p_1 : P_1(s_0, s_1), \dots, p_{n+1} : P_{n+1}(s_n, s_{n+1}) \text{ proctx}} ``` ## ModalTT {#slide-35 data-menu-title="ModalTT: Proterms (Grammar)"} #### Proterms: Grammar $$ \begin{aligned} p_i &\in \mathrm{Var}_\mathrm{Proterm}\\ f, g &\in \hat{\mathcal{F}}_\Sigma \\ s_i &\in \mathrm{Term} \\ \alpha &\in \hat{C}_\Sigma(P_1, \dots, P_n \Rightarrow Q \vert f \to g)\\ \mu &\in \mathrm{Proterm} \\ &::= p \\ &\hspace{0.5em}\vert \alpha \langle s_0, \dots, s_n \rangle (\mu_1, \dots, \mu_n) \\ &\hspace{0.5em}\vert \mu_1 \odot \mu_2\\ &\hspace{0.5em}\vert \text{let } [p_1 : \underline{P_1}, p_2 : \underline{P_2}] = \mu_1 \text{ in } \mu_2\\ \end{aligned} $$ ## ModalTT {#slide-36 data-menu-title="ModalTT: Proterms (Judgments, 1)"} #### Proterms: Typing Judgments
```{.mathpar} \inferrule* {\strut} {\overline{\Gamma} \vert p : \underline{P} \vdash p : \underline{P} } ```
```{.mathpar} \inferrule* {\overline{\Gamma}_i \vert \Omega_i \vdash \mu_i : P_i(s_{i-1}, s_i) \\ \alpha \in \widetilde{\mathcal{C}}_\Sigma(P_1, \dots, P_n \Rightarrow Q \vert f \to g) \\ i = 1, \dots, n} {\overline{\Gamma}_1, \dots, \overline{\Gamma}_n \vert \Omega_1, \dots, \Omega_n \vdash \alpha(s_0, \dots, s_n)\{\mu_1, \dots, \mu_n\} : Q(f [\![ s_0 ]\!], g [\![s_n]\!] )} ``` ## ModalTT {#slide-37 data-menu-title="ModalTT: Proterms (Judgments, 2)"} #### Proterms: Typing Judgments
```{.mathpar} \inferrule* {\overline{\Gamma}_1 \vert \Omega_1 \vdash \mu_1 : P_1(s_0, s_1) \\ \overline{\Gamma}_2 \vert \Omega_2 \vdash \mu_2 : P_2(s_1, s_2)} {\overline{\Gamma}_1, \overline{\Gamma}_2 \vert \Omega_1, \Omega_2 \vdash \mu_1 \odot \mu_2 : (P_1 \odot P_2)(s_0, s_2)} ```
```{.mathpar} \inferrule* {\overline{\Gamma} \vert \Omega \vdash \epsilon : (P_1 \odot P_2) (s_0, s_2) \\ \overline{\Gamma}_L, x_0 : X_0, x_1 : X_1, x_2 : X_2, \overline{\Gamma}_R \vert \Omega_L, p_1 : P_1(x_0, x_1), p_2 : P_2(x_1, x_2), \Omega_R \vdash \mu : Q(t_0, t_1)} {\overline{\Gamma}_L, \overline{\Gamma}, \overline{\Gamma}_R \vert \Omega_L, \Omega, \Omega_R \vdash \text{let } (p_1 : P_1(x_0, x_1), p_2 : P_2(x_1, x_2) = \epsilon) \text{ in } \mu : Q(t_0[s_0/x_0], t_1[s_2/x_2])} ``` ## ModalTT {#slide-38 data-menu-title="ModalTT: Semantics (1)"} #### VDC Semantics [Note:]{.define} the underlying VDC semantics of the type theory is still a work-in-progress. . . . We define a modal, fibrational VDC (with composites) $[\![ \mathbb{T}_\Sigma ]\!]$ as follows: . . . - Objects are term contexts $\Gamma = (x : X)$ (these are effectively just types annotated with a variable) modulo alpha equivalence of variables. . . . - Tight morphisms $(x : X) \to (y : Y)$ are terms $(x : X) \vdash s : Y.$ . . . - Proarrows $(x : X) \proto (y : Y)$ are protypes $$ (x : X) ; (y : Y) \vdash P(s, t). $$ ## ModalTT {#slide-39 data-menu-title="ModalTT: Semantics (2)"} #### VDC Semantics - Cells ```{.tikzcd} \begin{tikzcd} {\Gamma_0} & {\Gamma_1} & \cdots & {\Gamma_{n-1}} & {\Gamma_n} \\ {(y_0 : Y_0)} &&&& {(y_n : Y_n)} \arrow["{P_1(s_0,s_1)}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-1, to=1-2] \arrow["f_0"', from=1-1, to=2-1] \arrow["\shortmid"{marking}, from=1-2, to=1-3] \arrow["\shortmid"{marking}, from=1-3, to=1-4] \arrow["{P_n(s_{n-1},s_n)}"{inner sep=.8ex}, "\shortmid"{marking}, from=1-4, to=1-5] \arrow["f_n", from=1-5, to=2-5] \arrow[""{name=0, anchor=center, inner sep=0}, "{Q(t_0,t_n)}"'{inner sep=.8ex}, "\shortmid"{marking}, from=2-1, to=2-5] \arrow["\mu"{description}, draw=none, from=1-3, to=0] \end{tikzcd} ``` are proterms $$ \begin{aligned} \Gamma_0, \dots, \Gamma_n \vert p_1 : P_1(s_0, s_1), \dots, p_n : P_n(s_{n-1}, s_n) \vdash\\ \mu : Q(t_0[f_0(s_0)/y_0], t_n[f_n(s_n)/y_n]). \end{aligned} $$ ## ModalTT {#slide-40 data-menu-title="ModalTT: Semantics (3)"} #### VDC Semantics - Restriction cells are obtained via term substitution: $$ x_0 : X_0, x_1 : X_1 \vert p : P(f_0(x_0), f_1(x_1)) \vdash p : P(f_0(x_0), f_1(x_1)) $$ . . . - Loose composition is precisely $\odot$-introduction on protypes and proterms, with the universal property supplied by $\odot$-elimination along with the $\beta$/$\eta$-computation rules (not shown). . . . - Each modality symbol $L \in \mathcal{M}_\Sigma$ corresponds to a monad on $[\![\mathbb{T}_\Sigma]\!]$ via the derived form $L[-]$ and the primitive structure morphisms/cells $\eta$ and $\mu$. Functoriality is immediate from the normal form. ## Future work {#slide-41 data-menu-title="Future Work"} - Typing judgments for loose units are subtle and not fully developed (hence their omission). As currently implemented, they lack a normal form. . . . - The expected metatheorems (cut elimination, soundness of the VDC semantics, etc.) need to be checked more carefully. The semantics themselves are also not yet fully complete. . . . - The surface syntax is cumbersome and not especially user-friendly. . . . - The internal representation still needs to be hooked up to CatColab so that the DSL can actually be used alongside DoubleTT models. # Thanks for listening! {.close-slide}
{height=90 fig-align="center"} ::: notes (Leave this slide up during Q&A.) ::: ## References ::: notes Backup slide for Q&A. :::