natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
= + +
/ | -/ | |
, | ||
of / of | ||
for | for hom-tensor adjunction | |
introduction rule for | for hom-tensor adjunction | |
( of) | ( of) | |
into | into | |
( of) | ( of) | |
, , | ||
higher | ||
/ | -// | |
/ | ||
, () | , | |
(, ) | / | |
(absence of) | (absence of) | |
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.
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).
Notice that the following relation between syntax and semantics are well established (see at relation between type theory and category theory for details):
syntax | semantics |
---|---|
multiplicative intuitionistic linear type theory | (symmetric closed) monoidal categories |
dependent type theory | locally cartesian closed categories |
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 theory | category 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$:
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
satisfying Frobenius reciprocity. These serve as the semantics for the 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:
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
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).
That $f^\ast$ is a morphism of monoidal categories means that it is a strong monoidal functor, preserving the tensor product
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
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
The statement of Frobenius reciprocity then equivalently reads like this:
For $f\colon X\to Y$ a morphism in $\mathcal{C}$, we write
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
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
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):
syntax | semantics |
---|---|
homotopy type theory | locally cartesian closed (∞,1)-categories |
homotopy type theory with univalent weak type universes | (∞,1)-toposes |
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$.
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 dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14).
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
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 are in
Matthijs Vákár, Syntax and Semantics of Linear Dependent Types (arXiv:1405.0033)
Matthijs Vákár, Splitting the Atom of Dependent Types… or Linear and Operational Dependent Type Theory, November 2014 (pdf slides)
Neelakantan Krishnaswami, Pierre Pradic, Nick Benton, Integrating Dependent and Linear Types, POPL 15 (pdf)
Martin Lundfall?, A diagram model of linear dependent type theory, (arXiv:1806.09593)
Semantics for dependent linear type theory and linear homotopy type theory are discussed in
Mike Shulman, Framed bicategories and monoidal fibrations, in Theory and Applications of Categories, Vol. 20, 2008, No. 18, pp 650-738. (TAC)
Kate Ponto, Mike Shulman, Duality and traces in indexed monoidal categories, (arXiv:1211.1555, blog)
Mike Shulman, Enriched indexed categories,(arXiv:1212.3914)
Urs Schreiber, Quantization via Linear Homotopy Types, (arXiv:1402.7041)
Last revised on October 14, 2018 at 15:23:09. See the history of this page for a list of all contributions to it.