dependent linear type theory (changes) in nLab

Showing changes from revision #38 to #39: Added | Removed | Changed

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

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

{Γ⊢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 *):𝒞 Γ 1→f *⟵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).

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

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

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

• dependent type theory, linear type theory

• quantum set

• classical modality

• categorical semantics:

  indexed monoidal (∞,1)-categories,

  tangent (∞,1)-toposes

• quantum logic, quantum programming

• parameterized quantum system

References

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

• Iliano Cervesato, Frank Pfenning, A Linear Logical Framework, 1996, (web)

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

• Arnaud Spiwack, section 5 of: A dissection of L (2014) [[pdf](http://assert-false.science/arnaud/papers/A%20dissection%20of%20L.pdf)]

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:

• Ulrich Schöpp, Ian Stark, A Dependent Type Theory with Names and Binding, in Computer Science Logic. CSL 2004, Lecture Notes in Computer Science 3210 (2004) 235–249 [[doi:10.1007/978-3-540-30124-0_20](https://doi.org/10.1007/978-3-540-30124-0_20), web]

• 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, talk at Oxford, November 2014 (pdf)

• Matthijs Vákár, A Categorical Semantics for Linear Logical Frameworks, In: A. Pitts (ed.), Foundations of Software Science and Computation Structures FoSSaCS 2015. Lecture Notes in Computer Science, vol 9034. Springer 2015 (arXiv:1501.05016, doi:10.1007/978-3-662-46678-0_7)

• Matthijs Vákár, Section 3 of: In Search of Effectful Dependent Types (arXiv:1706.07997, uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)

• Neelakantan Krishnaswami, Pierre Pradic, Nick Benton, Integrating Dependent and Linear Types, ACM SIGPLAN Notices 50 1 (2015) 17–30 [[pdf](https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf), doi:10.1145/2775051.2676969]

• Martin Lundfall, Models of linear dependent type theory, 2017 (pdf)

• Martin Lundfall, A diagram model of linear dependent type theory [[arXiv:1806.09593](https://arxiv.org/abs/1806.09593)]

  (with homotopy type theory-aspects)

• Conor McBride, I Got Plenty o’ Nuttin’, in: A List of Successes That Can Change the World, Lecture Notes in Computer Science 9600, Springer (2016) [[doi:10.1007/978-3-319-30936-1_12](https://doi.org/10.1007/978-3-319-30936-1_12)]

• Robert Atkey, Syntax and semantics of quantitative type theory, in 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS (2018) 56–65 [[doi:10.1145/3209108.3209189](https://dl.acm.org/doi/10.1145/3209108.3209189)]

• Mike Shulman, A type theory for fibred functors and polynomials, unfinished note (2018) [[pdf](http://home.sandiego.edu/~shulman/papers/functors.pdf)]

• Benjamin Moon, Harley Eades III, Dominic Orchard, Graded Modal Dependent Type Theory. In: N. Yoshida (ed.) Programming Languages and Systems ESOP 2021, Lecture Notes in Computer Science 12648, Springer (2021) 462-490 [[doi:10.1007/978-3-030-72019-3_17](https://doi.org/10.1007/978-3-030-72019-3_17), arxiv:2010.13163]

(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

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [[doi:10.14418/wes01.3.139](https://doi.org/10.14418/wes01.3.139), ir:3269, pdf]

  (using ideas from bunched logic)

based on

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality (arXiv:2102.04099)

Exposition:

• Mitchell Riley, Extending Homotopy Type Theory with Linear Type Formers, talk at The ForML Lab (2021) [[web](https://the-au-forml-lab.github.io/colloquium_talks/Riley.html), video]

• Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, pdf, video: YT]

  Abstract. Some ∞-toposes support constructions that are inherently ‘linear’, such as the external smash product of parameterised spectra. These cannot be added axiomatically to ordinary HoTT, because there is no way to enforce this linearity: there are no restrictions on variable uses. This talk describes an extension of HoTT with linear tensor and hom type formers, as a kind of ‘binary modality’ and its right adjoint. Trying to stay compatible with existing results in HoTT naturally leads us to a novel kind of bunched dependent type theory. Our type theory is intended to be as human-usable as possible, with an eye towards synthetic stable homotopy theory.

• Mitchell Riley, Dependent Type Theories à la Carte, talk at CQTS Initial Researcher’s Meeting (Sep 2022) [pdf]

• Mitchell Riley, A Linear Dependent Type Theory with Identity Types as a Quantum Verification Language (2023) [[pdf](https://mvr.hosting.nyu.edu/pubs/translation.pdf), pdf]

  (translation between LHoTT and the proto-`Quipper` of Fu, Kishida & Selinger 2020)

See also:

• C.B. Aberlé, Foundations of Substructural Dependent Type Theory [[arXiv:2401.15258](https://arxiv.org/abs/2401.15258)]

Potential 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](http://arxiv.org/abs/1402.7041)]

• Hisham Sati, Urs Schreiber, Entanglement of Sections [[arXiv:2309.07245](https://arxiv.org/abs/2309.07245)]

As a quantum programming language:

• Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)

specifically implemented for Quipper:

• Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper, in I. Lanese, M. Rawski (eds.) Reversible Computation RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

and in view of linear homotopy type theory:

• Hisham Sati, Urs Schreiber, The Quantum Monadology [[arXiv:2310.15735](https://arxiv.org/abs/2310.15735)]