💻 computer science

A unification of graded and substructural logics

This paper introduces GRASS, a unified type system that integrates the resource restriction mechanisms of substructural logics with the quantitative tracking of graded systems, enabling flexible, heterogeneous control over variable usage within a single framework and subsuming established models like LNL, Adjoint Logic, and mGL through its categorical semantics.

Original authors: Peter Hanukaev, Harley Eades III

Published 2026-05-19

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Peter Hanukaev, Harley Eades III

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a chef running a busy kitchen. In a traditional kitchen (standard programming), if you need an egg, you can grab one, use it, and then grab another one from the same carton without worrying about how many are left. You can also throw an egg away if you don't need it. This is like treating variables as "propositions" that can be reused or discarded freely.

But in a high-stakes kitchen (resource-sensitive computing), ingredients are precious. You can't use the same egg twice in two different ovens at once, and you can't throw away a rare spice you might need later. This is the world of Grass, a new system created by Peter Hanukaev and Harley Eades III to help programmers manage these "ingredients" (variables) perfectly.

Here is how the paper breaks it down, using simple analogies:

1. The Two Old Ways of Managing Ingredients

Before Grass, there were two main ways chefs tried to manage their resources:

The "Strict Rules" Approach (Substructural Logics): Imagine a kitchen where the rules are rigid. You are forbidden from using an ingredient twice or throwing it away unless you have a special "magic pass" (a modality). This is great for preventing waste, but it's hard to use for things that should be reusable, like a salt shaker.
The "Scorecard" Approach (Graded Systems): Imagine a kitchen where you can use ingredients freely, but every time you grab one, you have to write down a number on a scorecard. If you grab a "1," you used it once. If you grab a "2," you used it twice. This is flexible, but it treats everything as a number, which can be too rigid for things that need strict "no reuse" rules.

2. The New Solution: Grass

The authors created Grass (Graded and Substructural). Think of Grass as a universal kitchen manager that combines the best of both worlds.

It's a Hybrid: Grass allows you to have some ingredients that follow strict "no reuse" rules (like a linear logic) and others that follow flexible "scorecard" rules (like a graded system), all in the same recipe.
The "Modes" Concept: This is the paper's big innovation. Imagine the kitchen has different "zones" or Modes.
- Zone A (Strict): In this zone, you can't reuse ingredients.
- Zone B (Flexible): In this zone, you can reuse ingredients, but you must track how many times.
- Zone C (Secure): In this zone, you might track security clearance levels.
Grass lets you move ingredients between these zones. You can take a "secure key" from the Secure Zone and use it to unlock a file in the Flexible Zone, but the system ensures the key is handled correctly according to the rules of both zones.

3. How It Controls Usage (The "Ideal" Concept)

The paper introduces a mathematical concept called an "Ideal" to control how ingredients can be combined.

The Analogy: Imagine you have a bucket of "contractible" items (things you can merge). If you have two "1s" (one use each), can you merge them into a "2" (two uses)?
- In some zones, Yes: You can merge two single-use items into a double-use item.
- In other zones, No: You cannot merge two single-use items. If you try to use a file handle twice, the system stops you because two "1s" cannot become a "2" in that specific zone.
This prevents dangerous errors, like trying to use two separate file handles as if they were one giant handle that can be used twice.

4. The "Translation" System

The paper also describes how to move between these different zones using morphisms (translation functions).

The Analogy: Imagine a translator who speaks "Strict Zone" and "Flexible Zone." If you have a rule in the Strict Zone that says "Do not reuse," the translator knows how to convert that into the Flexible Zone's language (perhaps by saying "Reuse is allowed, but only if you mark it with a high score").
The authors prove that this translation is safe. If a recipe works in the Strict Zone, the translated version will work correctly in the Flexible Zone without breaking the rules.

5. The Mathematical "Blueprint" (Categorical Semantics)

Finally, the authors built a mathematical "blueprint" (categorical semantics) to prove their system works.

The Analogy: They didn't just build the kitchen; they drew up the architectural plans using advanced geometry (category theory). They showed that their new system (Grass) is actually a "super-system" that contains all the old systems (Linear Logic, Adjoint Logic, etc.) as special cases.
They proved that if you take their complex blueprint and simplify it, you get the exact same results as the older, simpler blueprints. This means Grass is a true unification, not just a patchwork.

Summary

In short, this paper presents Grass, a new way to write computer code that treats variables like physical resources. It allows programmers to mix different rules for different variables within the same program.

It uses Modes to define different rule sets (strict vs. flexible).
It uses Ideals to decide when resources can be merged or split.
It uses Mathematical Proofs to ensure that moving between these different rule sets never causes the program to crash or behave incorrectly.

The result is a system that gives programmers the maximum possible control over how their code uses memory, files, and data, preventing leaks and errors while remaining flexible enough for complex tasks.

Technical Summary: A Unification of Graded and Substructural Logics (Grass)

Problem Statement

The treatment of program variables as resources has become central to verifying correctness properties such as memory safety and information flow. Two distinct approaches dominate the literature:

Substructural Logics: Systems like Linear Logic restrict structural rules (weakening and contraction) by default, reintroducing them selectively via modalities (e.g., the "of-course" modality $!$ ). While powerful, these systems often struggle to combine different logics with varying structural rules within a single framework without complex adjunctions.
Graded Systems: These systems allow structural rules by default but annotate assumptions with "grades" drawn from an algebraic structure (typically a semiring). Grades track resource usage quantitatively (e.g., via addition for contraction and a zero element for weakening). While flexible, standard graded systems typically assume a single grade algebra and may lack the fine-grained control over which specific variables can be contracted or weakened, often treating all variables uniformly under one algebraic regime.

The core problem addressed is the lack of a unified type system that can simultaneously support:

Multiple, distinct notions of resource usage (different grade algebras) within the same program.
Fine-grained control over structural rules (weakening and contraction) that goes beyond simple boolean toggles, allowing specific grades to be contractible while others are not.
A seamless integration of these features into a single categorical semantics.

Methodology

The authors present Grass (Graded and substructural), a type system that unifies these approaches through the following mechanisms:

1. Modes and Grade Algebras

Grass is parameterized by a collection of modes. Each mode $m$ is a triple $(R_m, \text{Cont}(m), \text{Weak}(m))$ , where:

$R_m$ is a grade algebra (a preordered semiring).
$\text{Cont}(m) \subseteq R_m$ is an ideal within the semiring. This ideal defines the set of grades that are mutually contractible.
$\text{Weak}(m) \in \{\text{true}, \text{false}\}$ is a boolean flag indicating whether weakening is permitted for the mode.

This structure allows for granular control: contraction is not a global property of the system but is restricted to grades within the specific ideal of the mode. Weakening is similarly controlled, but the authors note that due to subsumption rules, enabling weakening allows unused variables to be introduced at any grade $q \geq 0$ .

2. Syntax and Typing Rules

The syntax extends standard graded modal types with:

Heterogeneous Contexts: A typing judgment $\rho \mid M \odot \Gamma \vdash_m t : T$ includes a grade vector $\rho$ and a mode vector $M$ . Variables in the context $\Gamma$ can belong to different modes, provided the structural rules of the current mode $m$ are respected.
Modalities for Mode Shifting:
- Drop ( $\downarrow^q_{n \leq m}$ ): Promotes a term from a mode $m$ to a "stricter" mode $n$ (where $n \leq m$ ), enforcing a specific usage grade $q$ . This generalizes the graded modality $\Box_q A$ .
- Raise ( $\uparrow^{m \leq n}$ ): Lifts a term from a stricter mode $n$ to a more permissive mode $m$ .
Structural Rules:
- Contraction: Allowed only if the grades of the variables being contracted are elements of $\text{Cont}(m)$ .
- Weakening: Allowed only if $\text{Weak}(m)$ is true.
- Substitution: Defined to handle the interaction between different modes and grade multiplications, ensuring that the "independence" property (terms from stricter modes cannot depend on variables from looser modes) is maintained.

3. Categorical Semantics

The authors develop a categorical semantics based on graded linear exponential comonads.

Exponential Actions: For each mode $m$ , the semantics defines an exponential action on a symmetric monoidal closed category (SMCC). This involves a functor $D: R_m^{op} \to \text{SMC}(C, C)$ equipped with natural transformations for contraction ( $c$ ) and weakening ( $w$ ), satisfying coherence conditions.
Morphisms of Actions: To connect different modes, the authors introduce a novel notion of morphisms between exponential actions. These are symmetric lax monoidal adjunctions $F \dashv G$ equipped with a "lineator" natural transformation $\ell$ . This structure mirrors the syntactic modalities $\downarrow$ and $\uparrow$ .
Models: The semantics demonstrates that known models of intuitionistic, linear, relevant, and affine logics can be recovered as specific instantiations of Grass modes. Furthermore, the semantics subsumes established systems like Linear-Non-Linear Logic (LNL), Adjoint Logic, and mGL.

Key Contributions and Results

Unification of Logics: Grass provides a single framework where variables can be controlled by different grade algebras simultaneously. For example, a function can accept a key graded by a "security" algebra (where $High$ implies secure context) and a file handle graded by a "usage" algebra (where $1$ implies linear usage).
Granular Structural Control: By defining contraction via ideals rather than global rules, Grass allows for resource-sensitive distinctions that previous graded systems could not easily express. For instance, two linearly used file handles (grade 1) cannot be contracted into a single unrestricted handle (grade $\omega$ ), preventing unsafe resource merging.
Recovery of Existing Systems: The paper demonstrates that by instantiating specific modes, Grass recovers:
- Intuitionistic Logic: Mode $U = (\top, \top, \text{true})$ .
- Linear Logic: Mode $L = (\mathbb{N}, \{0\}, \text{false})$ (with discrete ordering).
- Relevant Logic: Mode $R = (\top, \top, \text{false})$ .
- Affine Logic: Mode $A = (\{0, 1\}, \{0\}, \text{true})$ .
- LNL and Adjoint Logic: By combining modes with appropriate morphisms.
Categorical Soundness: The authors prove that the $\beta$ - and $\eta$ -conversions are sound with respect to the categorical semantics. The interpretation of terms into the categorical model preserves typing and grading.

Significance and Claims

The paper claims that Grass offers a "maximally flexible control over variable usage" by incorporating mechanisms from both substructural and graded logics. Its primary significance lies in:

Expressiveness: It allows different variables in the same program to be governed by different notions of resource usage (e.g., security vs. memory usage) without requiring a monolithic grade algebra.
Theoretical Unification: It shows that on the level of categorical semantics, Grass subsumes multiple established systems (LNL, Adjoint Logic, mGL) by viewing them as specific configurations of modes and morphisms.
Novel Semantics: The introduction of morphisms between graded comonads (based on actegories) provides a new tool for reasoning about the interaction between different resource logics.

The authors remain modest regarding practical implementation, noting that while the system recovers known logics and generalizes them, the immediate focus is on the theoretical unification and categorical foundations. They suggest future work could explore the application of these lessons to graded dependent types, specifically addressing the challenge of treating types as intuitionistic (ungraded) while keeping terms graded.