Linearity and dependency analyses are key to several applications in computer science, especially, in resource management and information flow control. What connects these analyses is that both of them need to model at least two different worlds with constrained mutual interaction. Though linearity and dependency analyses address similar problems, the analyses are carried out by employing different methods. For linearity analysis, type systems employ the comonadic exponential modality from Girard's linear logic. For dependency analysis, type systems employ the monadic modality from Moggi's computational metalanguage. Owing to this methodical difference, a unification of the two analyses, though theoretically and practically desirable, is not straightforward. Fortunately, with recent advances in graded-context type systems, it has been realized that linearity and dependency analyses can be viewed through the same lens. However, existing graded-context type systems fall short of a unification of linearity and dependency analyses. The problem with existing graded-context type systems is that though their linearity analysis is general, their dependency analysis is limited, primarily because the graded modality they employ is comonadic and not monadic. In this paper, we address this limitation by systematically extending existing graded-context type systems so that the graded modality is both comonadic and monadic. This extension enables us to unify linearity analysis with a general dependency analysis. We present a unified Linear Dependency Calculus, LDC, which analyses linearity and dependency using the same mechanism in an arbitrary Pure Type System. We show that LDC is a general linear and dependency calculus by subsuming into it the standard calculi for the individual analyses.

翻译：线性度分析与依赖性分析是计算机科学中多项应用的关键，尤其在资源管理与信息流控制领域。这两类分析的共同点在于，它们都需要建模至少两个具有受限交互的不同世界。尽管线性度分析与依赖性分析解决的问题相似，但二者采用的方法不同。在线性度分析中，类型系统使用了吉拉尔线性逻辑中的余单子指数模态；而在依赖性分析中，类型系统则采用了莫吉计算元语言中的单子模态。由于这种方法论上的差异，尽管在理论和实践上都希望将两种分析统一，但实现起来并不简单。幸运的是，随着分级上下文类型系统的最新进展，人们意识到线性度分析与依赖性分析可以通过同一视角来审视。然而，现有的分级上下文类型系统未能实现线性度分析与依赖性分析的统一。其问题在于，尽管这些系统对线性度分析具有一般性，但对依赖性分析能力有限，主要原因是它们采用的分级模态是余单子形式而非单子形式。本文通过系统性地扩展现有分级上下文类型系统来克服这一局限，使得分级模态同时具备余单子与单子特性。这一扩展使我们能够将线性度分析统一到一般性的依赖性分析中。我们提出统一的线性依赖性演算LDC，该演算在任意纯类型系统中使用同一机制分析线性度和依赖性。通过将标准单项分析演算纳入LDC，我们证明LDC是一个通用的线性与依赖性演算。