nLab dependent linear type theory

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

Quantum systems

quantum logic


quantum physics


quantum probability theoryobservables and states


quantum information


quantum computation

qbit

quantum algorithms:


quantum sensing


quantum communication

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 (Schreiber 2014, Riley 2022) should additionally combine this with homotopy type theory. There are various things that such combinations might mean, and various approaches to making 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):

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

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 (,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, slides.

  • 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, slides.

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

Proposals for a genuine syntax for dependent linear type theory:

(Detailed critical discussion of most of these previous proposals is given in Riley 2022, §1.7 p. 90, see also brief comments in Riley 2022b, p. 22).

A satisfactory dependent linear homotopy type theory is given in

based on

Exposition:

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

As a quantum programming language:

specifically implemented for Quipper:

and in view of linear homotopy type theory:

Last revised on January 20, 2024 at 12:01:52. See the history of this page for a list of all contributions to it.