Dependent Multiplicities in Dependent Linear Type Theory

TL;DR

This paper introduces a new dependent linear type theory that allows resource usage to depend on program variables, enabling precise resource annotations for complex programs involving recursion and branching.

Contribution

It embeds linear logic into dependent type theory to create a system with dependent multiplicities, supporting inductive types and extending dependently typed languages.

Findings

Supports precise resource annotations in programs with recursion and branching

Provides a semantics framework as Categories with Families in symmetric monoidal categories

Demonstrates implementation in Agda for practical use

Abstract

We present a novel dependent linear type theory in which the multiplicity of some variable-i.e., the number of times the variable can be used in a program-can depend on other variables. This allows us to give precise resource annotations to programs involving branching and recursion that cannot be adequately typed in other theories. Our type system is obtained by embedding linear logic into dependent type theory and specifying how the embedded logic interacts with the host theory. We can then use the natural numbers of the dependent type theory to derive a quantitative typing system with dependent multiplicities. Our theory supports W-types, thereby giving a principled resource-aware treatment of a large class of inductive types. We characterise the semantics as Categories with Families indexed in symmetric monoidal categories, thereby generalising Quantitative Categories with Families. Existing dependently typed languages can easily be extended with our system, which we demonstrate with an implementation in Agda.