# nLab dependent linear type theory

Dependent linear type theory

# Dependent linear type theory

## Idea

Dependent linear type theory should be some kind of combination of dependent type theory and linear type theory. Dependent linear homotopy type theory should additionally combine this with homotopy type theory. But there are various things that such combinations might mean, and various attempts to make it precise.

One of the most important is a theory that includes both “linear types” and “nonlinear types”, where the linear types may be dependent on the nonlinear types. The nonlinear types might also be allowed to depend on each other, but in this theory the linear types are not allowed to depend on each other.

There are other approaches to dependent linear type theory that do allow some sort of dependence between linear types, but we will not (yet) discuss them on this page.

## Syntax

Details are still somewhat in the making: An extension of the LF syntax by dependent linear types appears in (Pfenning 96, WCFW 03) and a dependent linear extension of system L in (Spiwack 14, section 5).

Proposals for an actual syntax for dependent linear type theory appear in (Vákár 14, KPB 15).

## Semantics

One sort of dependent linear type theory should have categorical semantics in indexed monoidal (∞,1)-categories – see there for detailed discussion.

### Non-homotopy version

Notice that the following relation between syntax and semantics are well established (see at relation between type theory and category theory for details):

Here the correspondence in the first line works by interpreting types $X$ in the linear type theory as objects $[X]$ in a monoidal category $\mathcal{C}^{\otimes}$ and by interpreting the conjunctions (as far as they exist) as follows:

type theorycategory theory
$\otimes$ multiplicative conjunction$\otimes$ tensor product
$\multimap$ linear implication$[-,-]$ internal hom
$(-)^\bot$ linear negation$(-)^\ast$ dual object

The correspondence in the second line works by forming for any locally cartesian closed category $\mathcal{C}$ its system of slice categories $[\Gamma] \mapsto \mathcal{C}_{/[\Gamma]}$, each of which is a cartesian closed monoidal category, and then interpreting that as the semantics for dependent type theory in the context $\Gamma$:

$\left\{ \Gamma \vdash a \colon A \right\} \leftrightarrow \left\{ (\ast \stackrel{[a]}{\longrightarrow} [A]) \in Mor(\mathcal{C}_{/[\Gamma]}) \right\} \,.$

Moreover, the system of slice categories has good base change in that for every morphism $[f] \colon [\Gamma_1]\to [\Gamma_2]$ in $\mathcal{C}$ there is an adjoint triple of functors

$\mathcal{C}_{[\Gamma_1]} \stackrel{\stackrel{[f]_!}{\longrightarrow}}{\stackrel{\overset{[f]^\ast}{\longleftarrow}}{\underset{[f]_\ast}{\longrightarrow}}} \mathcal{C}_{[\Gamma_2]}$

satisfying Frobenius reciprocity. These serve as the semantics for the context extension along a map $f\colon \Gamma_1 \to \Gamma_2$ of contexts, and for the dependent sum $\sum$, and the dependent product of the dependent type theory syntax, respectively:

$\left\{ \underset{f^{-1}(-)}{\sum} , \; f \;, \underset{f^{-1}(-)}{\prod} \right\} \leftrightarrow \left\{ [f]_! \dashv [f]^\ast \dashv [f]_\ast \right\} \,.$

Now since a cartesian monoidal category is in particular a (symmetric closed) monoidal category, this immediately suggest to generalize the assignments $[\Gamma] \mapsto (\mathcal{C}_{/[\Gamma]})^\times$ to assignments $[\Gamma] \mapsto (\mathcal{C}_{[\Gamma]})^\otimes$ of (symmetric closed) monoidal categories (possibly but not necessarily the slice categories of $\mathcal{C}$) such that there still is good base change in the above way.

More explicitly, following the notion of hyperdoctrine, the categorical semantics of dependent linear type theory should have for each context $\Gamma$ a linear type theory/possibly-non-cartesian symmetric closed monoidal category $(\mathcal{C}_{\Gamma}, \otimes, 1)$ and for each homomorphism of contexts $f \;\colon\; \Gamma_1 \longrightarrow \Gamma_2$ functorially an adjoint triple of functors

$(f_! \dashv f^\ast \dashv f_\ast) \;\colon\; \mathcal{C}_{\Gamma_1} \stackrel{\stackrel{f_!}{\longrightarrow}}{\stackrel{\overset{f^\ast}{\longleftarrow}}{\underset{f_\ast}{\rightarrow}}} \mathcal{C}_{\Gamma_2} \,.$

where $f^\ast$ is context extension and where the left adjoint $f_!$ and right adjoint $f_\ast$ are to be thought of as linear analogs of dependent sum and dependent product, respectively. Moreover this should satisfy Frobenius reciprocity, hence $f^\ast$ should be a strong closed monoidal functor. Typically one would in addition demand the Beck-Chevalley condition for consecutive such adjoint triples.

Equivalently this is an indexed closed monoidal category; in the homotopical version, it would be an indexed monoidal (∞,1)-category. See those pages for more extensive discussion of the mathematics that takes place in such models that should be internalizable in dependent linear (homotopy) type theory once it exists.

In geometry/topos theory such a “linear hyperdoctrine” is known as six operations yoga in Wirtmüller flavor. In fact there this appears in geometric homotopy theory (“derived functors on quasicoherent sheaves”) hence as dependent linear homotopy type theory.

Details (of what?) are written out in (Vakar 14).

###### Remark

That $f^\ast$ is a morphism of monoidal categories means that it is a strong monoidal functor, preserving the tensor product

$f^\ast(X\otimes Y)\simeq (f^\ast X)\otimes (f^\ast Y) \,.$

If monoidal categories involved are closed monoidal categories then the condition of Frobenius reciprocity is equivalent to $f^\ast$ also being a strong closed functor in that it preserves the internal hom

$f^\ast [X,Y] \simeq [f^\ast X, f^\ast Y] \,.$
###### Definition (Notation)

In view of the perspective of semantics for type theory, we may omit the notational distinction between contexts and the objects that interpret them, and between dependent sum/product and the functors that interpret them. We will write the base change as

$\left( \underset{f}{\sum} \dashv f^\ast \dashv \underset{f}{\prod} \right) \;\colon\; Mod(\Gamma_1) \stackrel{\stackrel{f_!}{\longrightarrow}}{\stackrel{\overset{f^\ast}{\longleftarrow}}{\underset{f_\ast}{\longrightarrow}}} Mod(\Gamma_2) \,.$

The statement of Frobenius reciprocity then equivalently reads like this:

$\underset{f}{\sum} \left( X \otimes f^\ast Y \right) \simeq \left( \underset{f}{\sum} X \right) \otimes Y \,.$

For $f\colon X\to Y$ a morphism in $\mathcal{C}$, we write

$\epsilon_f \colon \underset{f}{\sum}f^\ast (-) \longrightarrow (-)$

for the adjunction counit of $(\sum_f \dashv f^\ast)$.

Notice that $\underset{f}{\sum}$ has the interpretation of summing over all the fibers of the morphism $f$, as the elements in its codomain vary. Therefore it is sometime suggestive to use the notation

$\underset{f^{-1}(-)}{\sum} \coloneqq \underset{f}{\sum} \,.$

In this vein, for $X \in \mathcal{C}$ any object and $p_X \colon X \to \ast$ the canonical morphism to the terminal object, we abbreviate as

$\underset{X}{\sum} \coloneqq \underset{p_X}{\sum} \,.$

### Homotopy version

This discussion of dependent linear type theory above has an evident straightforward refinement to homotopy theory. To appreciate this, notice that the following relation is well established (see again at relation between type theory and category theory for details):

This works very much along the lines of the above relation between dependent type theory and locally cartesian closed categories. The central new ingredient is that one requires the locally cartesian closed category $\mathcal{C}$ to be equipped with a suitable structure of a model category. Using this there is then a notation of fibrant replacement of morphisms. The key point is that where in extensional type theory the identity type $(X \vdash Id_X \colon Type)$ of a type $X$ has semantics given by the diagonal morphism $\Delta_{[X]} \in \mathcal{C}_{/{[X]}}$, here in homotopy type theory it has semantics in the fibrant replacement $\hat \Delta_{[X]} \in \mathcal{C}_{/X}$. Such a fibrant replacement of the diagonal is path space object of $X$, reflecting the equivalences/homotopies “inside” the type $X$.

###### Remark

Since the Grothendieck construction of the standard indexed monoidal $(\infty,1)$-category of parametrized spectra is a tangent (∞,1)-toposes, one model for linear types depending on other linear types might be higher jet (∞,1)-topos. This remains to be thought about.

What should be the categorical semantics of one kind of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14).

## References

A syntax extending LF with linear dependent types was first published in

Note that this framework was restricted to the negative fragment of intuitionistic linear logic and dependent type theory (i.e., $\multimap$, $\&$ and $\Pi$). The problem of extending LF to positive connectives ($\otimes,1,!,\exists$) while retaining a reasonable notion of canonical form was later addressed by

• Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker, A concurrent logical framework I: Judgments and properties, CMU technical report CMU-CS-02-101, revised May 2003 (web)

A dependent linear version of system L is considered in

More recent work in the type-theoretic literature includes:

• Ugo Dal Lago, Linear Dependent Types in a Subrecursive Setting, in Bounded Linear Logic Workshop Fontainebleau, 2013.

• Ugo Dal Lago, M. Gaboardi, Linear Dependent Types and Relative Completeness-, inLogical Methods in Computer Science_ Vol. 8(4:11), 2012.

• Ugo Dal Lago and B. Petit, Linear dependent types in a call-by-value scenario, in Science of Computer Programming 84, 2014.

• F.N. Forsberg, Restricted linear dependent types for resource allocation, in Bounded Linear Logic Workshop, Fontainebleau, 2013.

• M. Gaboardi et al., Linear Dependent Types for Differential Privacy, in POPL ‘13, 2013.

Proposals for a genuine syntax for dependent linear type theory (some of which use ideas from bunched logic) are in

Potential semantics for dependent linear type theory and linear homotopy type theory are discussed in

specifically implemented for Quipper:

Last revised on June 4, 2022 at 07:20:06. See the history of this page for a list of all contributions to it.