# What is "graded modality" in type theory?

I'm referring to these papers:

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 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? 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?

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

• 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. Commented May 17 at 4:46
• As I've always said, most type theorists are mathematicians, just that some of their work happen to be of relevance in computer science :-) Commented May 17 at 4:47