<p>I'm referring to these papers:</p>
<ul>
<li><a href="https://arxiv.org/abs/2010.13163" rel="noreferrer"><em>Graded Modal Dependent Type Theory</em></a> (<a href="https://github.com/granule-project/gerty" rel="noreferrer">The Gerty Language</a>)</li>
<li><a href="https://www.cs.kent.ac.uk/people/staff/dao7/publ/granule-icfp19.pdf" rel="noreferrer"><em>Quantitative program reasoning with graded modal types</em></a> (<a href="https://granule-project.github.io/granule.html" rel="noreferrer">The Granule Language</a>)</li>
</ul>
<p>At first glance, it seems graded modal types are just a generalization of linear types that can enforce that a term is used exactly <em>n</em> times (where <em>n</em> is arbitrary and can even be polymorphic), whereas linear types only enforce that a term is used exactly once. However, graded modality is also cited in <a href="https://granule-project.github.io/granule.html#:%7E:text=Example%202" rel="noreferrer">Example 2 of the Granule overview</a> to enforce public/private terms, and Example 3 to track side effects. So it seems to be more general.</p>
<p>The terminology &quot;graded modality&quot; seems to come from philosophy. My understanding is that modal logic encodes statements that are &quot;possibly true&quot; and &quot;necessarily true&quot;, while graded modal logic quantifies (&quot;grades&quot;) the possibility by encoding that a statement is true in exactly <em>n</em> possible situations out of some finite total (e.g. a relation only holds for <em>n</em> terms in a set).</p>
<p>This is similar to the question <a href="https://langdev.stackexchange.com/questions/412/what-are-the-advantages-of-using-dependent-modal-types-in-a-language">What are the advantages of using Dependent Modal Types in a language?</a> But I'm not sure where the &quot;graded&quot; refers to; is it just the &quot;modality&quot; that enforces a type can be used exactly <em>n</em> times? Also, how are modalities different than refinements, coeffects, and other &quot;attributes&quot; that can be on types and functions which restrict the usage of their terms?</p>

<types><terminology><substructural-types>
What is "graded modality" in type theory?
<p>The term “graded” could just as well be replaced with “indexed”. Graded possibility is an indexed monad and graded necessity is an indexed comonad.</p>
<p>I believe the reason for using the word “grade” instead of “index” is just to be more specific about what the index is for, and in this context it’s an umbrella term that includes both “effect” and “coeffect”. In the Granule paper, a grade represents the set of ways in which a resource can be used, and can be any type that supports the “resource algebras” they describe.</p>
<p>Their necessity modality is graded by a coeffect that must be an element of some preordered semiring (R, +, 0, ·, 1, ⊑). The additive (+) and multiplicative (·) operations are similar to those in linear logic: additives keep track of resource requirements from different possible branches of a computation, and multiplicatives describe how resources are split between separate computations. Essentially any coeffect algebra is going to need similar operations to these.</p>
<p>Their possibility modality is indexed by a preordered monoid (E, ⭑, 1, ≤), where the unit (1) is the effect that’s always allowed, and the monoid operation (⭑) is a way of combining the effects of multiple subcomputations.</p>
<p>The preorders (⊑) and (≤) provide “approximation” whereby you can always <em>weaken a precondition</em> or <em>strengthen a postcondition</em>, respectively. This isn’t strictly necessary, but it serves to make the resulting type system a bit easier to use. A few examples they give are:</p>
<ul>
<li><p>Private ⊑ Public: a public value can be used wherever a private value can, but not the other way around</p>
</li>
<li><p>(1..2) ⊑ (0..3): using a variable 1 or 2 times is perfectly fine in a context that allows it to be used anywhere from 0 to 3 times</p>
</li>
<li><p>1 ≤ <em>e</em> for all <em>e</em> in E: you can always use pure code even though effects are allowed</p>
</li>
</ul>

CC BY-SA 4.0
2024-05-05T04:07:03.983Z
2024-05-05T04:07:03.983Z
Jon Purdy
CC BY-SA 4.0
2024-05-17T04:46:58.757Z
The terminology "graded" is mathematical in nature: a graded modality corresponds to a graded monad, which is in turn a graded monoid in an endofunctor category. cf. mathematical objects like graded rings.
xuq01
CC BY-SA 4.0
2024-05-17T04:47:51.247Z
As I've always said, most type theorists are mathematicians, just that some of their work happen to be of relevance in computer science :-)
xuq01
# What is "graded modality" in type theory?
Posted by: username_0 on 2024-05-05
I'm referring to these papers:

* [*Graded Modal Dependent Type Theory*](https://arxiv.org/abs/2010.13163) ([The Gerty Language](https://github.com/granule-project/gerty))
* [*Quantitative program reasoning with graded modal types*](https://www.cs.kent.ac.uk/people/staff/dao7/publ/granule-icfp19.pdf) ([The Granule Language](https://granule-project.github.io/granule.html))

At first glance, it seems graded modal types are just a generalization of linear types that can enforce that a term is used exactly *n* times (where *n* is arbitrary and can even be polymorphic), whereas linear types only enforce that a term is used exactly once. However, graded modality is also cited in [Example 2 of the Granule overview](https://granule-project.github.io/granule.html#:%7E:text=Example%202) to enforce public/private terms, and Example 3 to track side effects. So it seems to be more general.

The terminology "graded modality" seems to come from philosophy. My understanding is that modal logic encodes statements that are "possibly true" and "necessarily true", while graded modal logic quantifies ("grades") the possibility by encoding that a statement is true in exactly *n* possible situations out of some finite total (e.g. a relation only holds for *n* terms in a set).

This is similar to the question [What are the advantages of using Dependent Modal Types in a language?](https://langdev.stackexchange.com/questions/412/what-are-the-advantages-of-using-dependent-modal-types-in-a-language) But I'm not sure where the "graded" refers to; is it just the "modality" that enforces a type can be used exactly *n* times? Also, how are modalities different than refinements, coeffects, and other "attributes" that can be on types and functions which restrict the usage of their terms?
**Tags:** types terminology substructural-types
---
## 1 answers
### Answer by username_1 on 2024-05-05. Score: 7 | Accepted answer
The term “graded” could just as well be replaced with “indexed”. Graded possibility is an indexed monad and graded necessity is an indexed comonad.

I believe the reason for using the word “grade” instead of “index” is just to be more specific about what the index is for, and in this context it’s an umbrella term that includes both “effect” and “coeffect”. In the Granule paper, a grade represents the set of ways in which a resource can be used, and can be any type that supports the “resource algebras” they describe.

Their necessity modality is graded by a coeffect that must be an element of some preordered semiring (R, +, 0, ·, 1, ⊑). The additive (+) and multiplicative (·) operations are similar to those in linear logic: additives keep track of resource requirements from different possible branches of a computation, and multiplicatives describe how resources are split between separate computations. Essentially any coeffect algebra is going to need similar operations to these.

Their possibility modality is indexed by a preordered monoid (E, ⭑, 1, ≤), where the unit (1) is the effect that’s always allowed, and the monoid operation (⭑) is a way of combining the effects of multiple subcomputations.

The preorders (⊑) and (≤) provide “approximation” whereby you can always *weaken a precondition* or *strengthen a postcondition*, respectively. This isn’t strictly necessary, but it serves to make the resulting type system a bit easier to use. A few examples they give are:

* Private ⊑ Public: a public value can be used wherever a private value can, but not the other way around
* (1..2) ⊑ (0..3): using a variable 1 or 2 times is perfectly fine in a context that allows it to be used anywhere from 0 to 3 times
* 1 ≤ *e* for all *e* in E: you can always use pure code even though effects are allowed
> **Comments:**
> **username_2** (2024-05-17): The terminology "graded" is mathematical in nature: a graded modality corresponds to a graded monad, which is in turn a graded monoid in an endofunctor category. cf. mathematical objects like graded rings.  
> **username_2** (2024-05-17): As I've always said, most type theorists are mathematicians, just that some of their work happen to be of relevance in computer science :-)  
---
