Abstract
Dependent type theories enable us to reason about properties of our programs, while substructural type theories enable us to reason about their resource use. Quantitative type theory seamlessly combines dependent and substructural types by employing positive semirings to keep track of variable usage and computational contexts.
Existing treatments of this theory typically focus on multiplicative connectives such as functions or multiplicative pairs. In this work, we extend quantitative type theory with additive zero, unit, unions and dependent pairs, as well as annotated eliminators for various types.
We then explain how these additive types can be used to better describe resource use and how they integrate with existing programming techniques. Finally, we implement an interpreter for a language based on these extensions.