一句话：建立 graded-base 与 linear-base 两类分级 coeffect 系统之间保类型、grade 与操作语义的翻译。
过去十年出现了两条相互独立的分级 coeffect 类型系统路线：一条将 coeffect 注解普遍施加在函数类型上，作者称为 graded-base；另一条在线性类型之上引入分级模态类型算子来添加上下文依赖等 coeffect，称为 linear-base。二者分别源自线性逻辑传统与 QTT、Linear Haskell 等实践，但它们之间的关系一直未明。本文通过构造两类演算成对之间的翻译来回答该问题，并证明这些翻译保持类型、grade 以及操作语义。结果表明同一类上下文依赖与资源使用概念可以在任一种风格中表达，从而在两系之间架起桥梁，使结果与思想可以迁移，并帮助语言设计者更有依据地选择设计路线。评估以形式化翻译与保持性证明为主，而非实验基准。
Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects ). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call graded-base ) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call linear-base ). The latter has its origins in Girard’s Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LiepeltMO26,
title = {Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types},
author = {Vilem Liepelt and Danielle Marshall and Dominic Orchard},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828697}
}