A unification of graded and substructural logics
For researchers in type theory and programming languages, this provides a unifying framework that integrates two previously separate approaches to resource-sensitive computation.
The paper introduces GRASS, a type system that unifies graded and substructural logics to provide flexible control over variable usage, and shows that its categorical semantics subsumes established systems like LNL, Adjoint Logic, and mGL.
Type systems which account for resource sensitive computations can generally be split into two styles: First, substructural logics such as Linear Logic which seek to restrict weakening and contraction and reintroduce them in a controlled manner; And second, graded systems which allow weakening and contraction by default, but track the use of variables quantitatively in some algebraic structure -- usually a semiring. We present GRASS (Graded and substructural), a type system which incorporates mechanisms from both of these approaches, thus allowing maximally flexible control over variable usage. Furthermore, GRASS allows grades from an arbitrary collection of grade algebras to coexist in the same system, thus allowing different variables to be controlled with respect to different notions of resource within the same program. We develop the categorical semantics of \gyaru{}, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.