After a decade of separate evolution, the two dominant approaches to graded types—graded-base and linear-base—turn out to be two sides of the same coin. The authors prove translations that preserve type, grade, and operational semantics, meaning any analysis expressible in one system can be mapped to the other.
Two Lineages, One Root
Graded-base systems, originating in the mid-2010s, tack coeffect annotations directly onto function types. You see this in QTT and Linear Haskell. Linear-base systems, descending from Girard's Linear Logic, wrap a graded modal type operator around linear types. Granule and Idris use this style. Researchers have long wondered whether the two express the same underlying structure. Now we have a definitive answer.
What the Translation Actually Proves
The paper gives explicit translations between a pair of calculi from each lineage. Every term in a graded-base calculus maps to a term in the linear-base calculus and vice versa. Crucially, the translations are type-, grade-, and operational-semantics preserving—if two terms step to the same result in one system, their images step to corresponding results in the other. That is not just a theoretical curiosity; it means compiler optimizations, type inference algorithms, and resource analyses proven for one style automatically carry over to the other.
What This Means for Language Designers
If you are building a language with coeffect tracking—for side effects, resource usage, or context dependence—you no longer have to bet on one lineage. The two styles are not competing; they are notational variants. Designers can pick the syntax that fits their language's philosophy and still borrow results from the other camp. Idris and Granule users, for instance, can now directly apply insights from QTT and Linear Haskell without reinventing the wheel. The bridge is built—the rest is engineering.
Source: Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Domain: arxiv.org
Comments load interactively on the live page.