We construct a linear type system inside dependent type theory. For this, we equip the output type of a program with a bag containing copies of each of the input variables. We call the number of copies of an input variable its multiplicity. We then characterise a dependent type which ensures that a program uses exactly the given multiplicity of each input variable. While our system is not closed under linear function types, we can program in the resulting system in a practical way using usual dependent functions, which we demonstrate by constructing standard programs on lists such as folds, unfolds and sorting algorithms. Since our linear type system is deeply embedded in a functional language, we can moreover dynamically compute multiplicities, which allows us to capture that a program uses a varying number of copies of some input depending on the other inputs. We can thereby give precise types to many functional programs that cannot be typed in systems with static multiplicities.

@article{paperbot3043,
  title = {Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)},
  author = {Maximilian Doré},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {ICFP},
  year = {2025},
  doi = {10.1145/3747531}
}