nLab
dependent linear type theory

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

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).

What should be the categorical semantics of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14). Proposals for an actual syntax for dependent linear type theory appear in (Vákár 14, KPB 15).

Semantics

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):

syntaxsemantics
multiplicative intuitionistic linear type theory(symmetric closed) monoidal categories
dependent type theorylocally cartesian closed categories

Here the correspondence in the first line works by interpreting types XX in the linear type theory as objects [X][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:

{Γa:A}{(*[a][A])Mor(𝒞 /[Γ])}. \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]:[Γ 1][Γ 2][f] \colon [\Gamma_1]\to [\Gamma_2] in 𝒞\mathcal{C} there is an adjoint triple of functors

𝒞 [Γ 1][f] *[f] *[f] !𝒞 [Γ 2] \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 the context extension along a map f:Γ 1Γ 2f\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:

{f 1(),f,f 1()}{[f] ![f] *[f] *}. \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 (𝒞 Γ,,1)(\mathcal{C}_{\Gamma}, \otimes, 1) and for each homomorphism of contexts f:Γ 1Γ 2f \;\colon\; \Gamma_1 \longrightarrow \Gamma_2 functorially an adjoint triple of functors

(f !f *f *):𝒞 Γ 1f *f *f !𝒞 Γ 2. (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 *f^\ast is context extension and where the left adjoint f !f_! and right adjoint f *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 *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 *f^\ast is a morphism of monoidal categories means that it is a strong monoidal functor, preserving the tensor product

f *(XY)(f *X)(f *Y). 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 *f^\ast also being a strong closed functor in that it preserves the internal hom

f *[X,Y][f *X,f *Y]. 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

(ff *f):Mod(Γ 1)f *f *f !Mod(Γ 2). \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:

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

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

ϵ f:ff *()() \epsilon_f \colon \underset{f}{\sum}f^\ast (-) \longrightarrow (-)

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

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

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

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

Xp X. \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):

syntaxsemantics
homotopy type theorylocally 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 (XId X:Type)(X \vdash Id_X \colon Type) of a type XX has semantics given by the diagonal morphism Δ [X]𝒞 /[X]\Delta_{[X]} \in \mathcal{C}_{/{[X]}}, here in homotopy type theory it has semantics in the fibrant replacement Δ^ [X]𝒞 /X\hat \Delta_{[X]} \in \mathcal{C}_{/X}. Such a fibrant replacement of the diagonal is path space object of XX, reflecting the equivalences/homotopies “inside” the type XX.

Remark

Since the Grothendieck construction of the standard indexed monoidal (,1)(\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.

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 (,1,!,\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 are in

Revised on October 16, 2017 05:29:04 by Urs Schreiber (94.220.50.90)