一句话：在依赖类型论内嵌线性类型系统，支持动态重数，为更多函数式程序给出精确类型。
本文在依赖类型论内部构造线性类型系统，以解决线性与依赖类型结合时难以精确刻画输入使用次数的问题。核心做法是让程序输出类型携带一个 bag，其中包含各输入变量的若干副本，副本数量称为重数；再定义依赖类型，确保程序恰好按给定重数使用每个输入。由于系统深度嵌入函数式语言，重数可动态计算，从而表达某输入的使用次数随其他输入变化的情形。作者用列表上的 fold、unfold 和排序等标准程序展示实用性。关键结果是：系统虽不封闭于线性函数类型，仍可用普通依赖函数实用编程，并为静态重数系统无法类型化的许多程序给出精确类型。
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}
}