Deriving Distributive Laws for Graded Linear Types

Consider the situation of projecting the first element of a pair. In Granule, this first-projection is defined and typed as the following polymorphic function (whose syntax is reminiscent of Haskell or ML):

Linearity is the default, so this represents a linear function applied to linear values.²²2Granule uses $\rightarrow$ syntax rather than $\multimap$ for linear functions for the sake of familiarity with standard functional languages However, the second component of the pair has a graded modal type, written b [0], which means that we can use the value “inside” the graded modality $0$ times by first ‘unboxing’ this capability via the pattern match [y] which allows weakening to be applied in the body to discard y of type b. In calculus of Section 2, we denote ‘b [0]’ as the type $\Box_{0}b$ (Granule’s graded modalities are written postfix with the ‘grade’ inside the box).

The type for fst is however somewhat restrictive: what if we are trying to use such a function with a value (call it myPair) whose type is not of the form (a, b [0]) but rather (a, b) [r] for some grading term r which permits weakening? Such a situation readily arises when we are composing functional code, say between libraries or between a library and user code. In this situation, fst myPair is ill-typed. Instead, we could define a different first projection function for use with myPair : (a,b) [r] as:

This implementation uses various language features of Granule to make it as general as possible. Firstly, the function is polymorphic in the grade r and in the semiring s of which r is an element. Next, a refinement constraint 0 $\leqslant$ r specifies that by the preordering $\leqslant$ associated with the semiring s, that 0 is approximated by r (essentially, that r permits weakening). The rest of the type and implementation looks more familiar for computing a first projection, but now the graded modality is over the entire pair.

From a software engineering perspective, it is cumbersome to create alternate versions of generic combinators every time we are in a slightly different situation with regards the position of a graded modality. Fortunately, this is an example to which a general distributive law can be deployed. In this case, we could define the following distributive law of graded modalities over products, call it pushPair:

This ‘pushes’ the graded modality r into the pair (via pattern matching on the modality and the pair inside it, and then reintroducing the modality on the right hand side via [x] and [y]), distributing the graded modality to each component. Given this combinator, we can now apply fst (pushPair myPair) to yield a value of type a [r], on which we can then apply the Granule standard library function extract, defined:

to get the original a value we desired:

The pushPair function could be provided by the standard library, and thus we have not had to write any specialised combinators ourselves: we have applied supplied combinators to solve the problem.

Now imagine we have introduced some custom data type List on which we have a map function:

Note that, via a graded modality, the type of map specifies that the parameter function, of type a $\rightarrow$ b is non-linear, used between $0$ and $\infty$ times. Imagine now we have a value myPairList : (List (a, b)) [r] and we want to map first projection over it. But fst expects (a, b [0]) and even with pushPair we require (a, b) [r]. We need another distributive law, this time of the graded modality over the List data type. Since List was user-defined, we now have to roll our own pushList operation, and so we are back to having to make specialised combinators for our data types.

The crux of this paper is that such distributive laws can be automatically calculated given the definition of a type. With our Granule implementation of this approach (Section 4), we can then solve this combination problem via the following composition of combinators:

where the push operations are written with their base type via @ (a type application) and whose definitions and types are automatically generated during type checking. Thus the push operation is a data-type generic function [15]. This generic function is defined inductively over the structure of types, thus a programmer can introduce a new user-defined algebraic data type and have the implementation of the generic distributive law derived automatically. This reduces both the initial and future effort (e.g., if an ADT definition changes or new ADTs are introduced).

Dual to the above, there are situations where a programmer may wish to pull a graded modality out of a structure. This is possible with a dual distributive law, which could be written by hand as:

Note that the resulting grade is defined by the greatest-lower bound (meet) of n and m, if it exists as defined by a preorder for semiring s (that is, $\sqcap$ is not a total operation). This allows some flexibility in the use of the pull operation when grades differ in different components but have a greatest-lower bound which can be ‘pulled out’. Our approach also allows such operations to be generically derived.

Typing is via judgments of the form $\Gamma\vdash\mathit{t}:\mathit{A}$, assigning a type $A$ to term $t$ under the context $\Gamma$. Typing contexts $\Gamma$ contain linear or graded assumptions given by the grammar:

$$\Gamma::=\emptyset\mid\Gamma,\mathit{x}:\mathit{A}\mid\Gamma,\mathit{y}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}}}$$

where $x$ is a linear assumption and where $y$ is an assumption graded by ${\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}}$ drawn from the preordered semiring (called a graded assumption). This delineation of linear and graded assumptions avoids issues with substitution under a promotion, following the technique of Terui’s discharged assumptions [29]. Linear assumptions (including those of a graded modal type $\Box_{r}A$) must therefore be used exactly once, whilst graded assumptions may be used non-linearly subject to the constraint of $r$.

Figure 1 gives the typing rules. We briefly explain each rule in turn.

The var, abs and app rules follow the standard rules for the linear $\lambda$-calculus, modulo the context addition operation $\Gamma+\Gamma^{\prime}$ which is used in the rules any time the contexts of two subterms need to be combined. Context addition acts as union on disjoint linear and graded assumptions but is defined via semiring addition when a graded assumption appears in both contexts:

$\displaystyle(\Gamma,\mathit{x}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}}})+(\Gamma^{\prime},\mathit{x}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{s}}})=(\Gamma+\Gamma^{\prime}),\mathit{x}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}+\mathit{s}}}$

Context addition $+$ is undefined in the case of contexts whose linear assumptions are not-disjoint, enforcing the lack of contraction on linear assumptions.

The next rules relate to grading. Structural weakening is provided by (weak) for assumptions graded by 0 and ‘dereliction’ (der) converts a linear assumption to a graded assumption, graded by 1. Graded modalities are introduced by ‘promotion’ (pr), scaling graded assumptions in $\Gamma$ via semiring multiplication defined on contexts containing only graded assumptions as:

$\displaystyle{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\,*\,}}\emptyset=\emptyset\qquad\qquad{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\,*\,}}(\Gamma,\mathit{x}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{s}}})=({\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\,*\,}}\Gamma),\mathit{x}:[\mathit{A}]_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}(\mathit{r}{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\,*\,}\mathit{s})}}$

In the (pr) rule, $[\Gamma]$ denotes contexts with only graded assumptions. The approx rule captures grade approximation, allowing a grade $r$ in an assumption to be converted to another grade $s$, on the condition that $r$ is approximated by $s$, via the relation $\sqsubseteq$ as provided by the semiring’s preorder.

The letrec rule provides recursive bindings in the standard way.

The rules of pattern typing are given in Figure 2. The rule (PBox) provides graded modal elimination (an ‘unboxing’ pattern), propagating grade information into the typing of the sub-pattern. Thus $\textbf{case}\ \mathit{t}\ \textbf{of}\ [\mathit{p}]\rightarrow\mathit{t^{\prime}}$ can be used to eliminate a graded modal value. Variable patterns are typed via two rules depending on whether the variable occurs inside an unbox pattern ([Pvar]) or not (Pvar), with the [Pvar] rule producing a binding with the grade of the enclosing box’s grade $\mathit{r}$. As with variable patterns, constructor patterns are split between rules for patterns which either occur inside an unboxing pattern or not. In the former case, the grade information is propagated to the subpattern(s), with the additional constraint that if there is more than one data constructor for the type $\mathit{A}$ (written $|A|>1$), then the grade $r$ must approximate 1 (written ${\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}1}\,{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\sqsubseteq}\,\mathit{r}$) as pattern matching incurs a usage to inspect the constructor (discussed further in Section 6). The operation $|\mathit{A}|$ counts the number of data constructors for a type:

$\displaystyle|\mathbf{1}|=1\;\;\;\;|\mathit{A}\multimap\mathit{B}|=1\;\;\;\,|\square_{{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\mathit{r}}}\mathit{A}|=|\mathit{A}|\;\;\;\;|\mathit{A}\,\oplus\,\mathit{B}|=2(|A|+|B|)\;\;\;\;|\mathit{A}\,\otimes\,\mathit{B}|=|A||B|\;\;\;\;|\mu{X}.\mathit{A}|=|A[\mu{X}.\mathit{A}/X]|$

and $|{X}|$ is undefined (or effectively 0) since we do not allow unguarded recursion variables in types. A type $A$ must therefore involve a sum type for $|A|>1$.

Since a wildcard pattern $\_\,$ discards a value, this is only allowed inside an unboxing pattern where the enclosing grade permits weakening, captured via ${\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}0}\,{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\sqsubseteq}\,\mathit{r}$ in rule [Pwild].

We now provide two examples of graded modalities. In addition to those shown here, Granule provides various other graded modalities, including grading by semirings of security-level lattices and “sensitivities” akin to DFuzz [10].

Figure 3 defines an equational theory for GrMini^P. The equational theory is typed, but for brevity we elide the typing for most cases since it follows exactly from the structure of the terms. The fully typed rules are provided in the appendix [18]. For those rules which are type restricted, we include the full typed-equality judgment here. The typability of these equations relies on previous work on the Granule language which proves that pattern matching and substitution are well typed [23].

The $\beta$ and $\eta$ rules follow the standard rules from the $\lambda$-calculus, where $\#$ is a freshness predicate, denoting that variable $x$ does not appear inside term $t$.

For recursive letrec bindings, the $\beta_{letrec}$ rule substitutes any occurrence of the bound variable $x$ in $\mathit{t_{{\mathrm{2}}}}$ with $\textbf{letrec}\ \mathit{x}\ =\ \mathit{t_{{\mathrm{1}}}}\ \textbf{in}\ \mathit{t_{{\mathrm{1}}}}$, ensuring that recursive uses of $x$ inside $\mathit{t_{{\mathrm{1}}}}$ can be substituted with $\mathit{t_{{\mathrm{1}}}}$ through subsequent $\beta_{letrec}$ reduction. The LetRecDistrib rule allows distributivity of functions over letrec expressions, stating that if a function $f$ can be applied to the entire letrec expression, then this is equivalent to applying $f$ to just the body term $\mathit{t_{{\mathrm{2}}}}$.

Term elimination is via case, requiring rules for both $\beta$- and $\eta$-equality on case expressions, as well as rules for associativity and distributivity. In $\beta_{case}$, a term $t$ is matched against a pattern $\mathit{p_{\mathit{j}}}$ in the context of the term $\mathit{t_{\mathit{j}}}$ through the use of the partial function $(t\ \rhd\ \mathit{p_{\mathit{j}}})\mathit{t_{\mathit{j}}}=t^{\prime}$ which may substitute terms bound in $\mathit{p_{\mathit{j}}}$ into $\mathit{t_{\mathit{j}}}$ to yield $t^{\prime}$ if the match is successful. This partial function is defined inductively:

$\displaystyle\begin{array}[]{cccc}\inferrule*[right=$\rhd_{-}$]{\quad}{(\mathit{t}\rhd\_)\mathit{t^{\prime}}=\mathit{t^{\prime}}}&\inferrule*[right=$\rhd_{var}$]{\quad}{(\mathit{t}\rhd\mathit{x})\mathit{t^{\prime}}=[\mathit{t}/\mathit{x}]\mathit{t^{\prime}}}&\inferrule*[right=$\rhd_{\Box}$]{(\mathit{t}\rhd\mathit{p})\mathit{t^{\prime}}=\mathit{t^{\prime\prime}}}{([\mathit{t}]\rhd[\mathit{p}])\mathit{t^{\prime}}=\mathit{t^{\prime\prime}}}&\inferrule*[right=$\rhd_{C}$]{(\mathit{t_{\mathit{i}}}\rhd\mathit{p_{\mathit{i}}})\mathit{t}^{\prime}_{i}=\mathit{t}^{\prime}_{i+1}}{(C{t_{1},..,t_{n}}\rhd C\,\mathit{p_{{\mathrm{1}}}}\,...\,\mathit{p_{\mathit{n}}})\mathit{t}^{\prime}_{1}=\mathit{t}^{\prime}_{n+1}}\end{array}$

As a predicate to the $\beta_{case}$ rule, we require that $j$ be minimal, i.e. the first pattern $\mathit{p_{\mathit{j}}}$ in $\mathit{p_{{\mathrm{1}}}}...\mathit{p_{\mathit{n}}}$ for which $(t\ \rhd\ \mathit{p_{\mathit{j}}})\mathit{t_{\mathit{j}}}=t^{\prime}$ is defined. Rule $\eta_{case}$ states that if all branches of the case expression share a common term $t_{2}$ which differs between branches only in the occurrences of terms that match the pattern used, then we can substitute $t_{1}$ for the pattern inside $t_{2}$.

Associativity of case expressions is provided by the CaseAssoc rule. This rule allows us to restructure nested case expressions such that the output terms $\mathit{t_{\mathit{i}}}$ of the inner case may be matched against the patterns of the outer case, to achieve the same resulting output terms $\mathit{t^{\prime}_{\mathit{i}}}$. The [CaseAssoc] rule provides a graded alternative to the CaseAssoc rule, where the nested case expression is graded, provided that the patterns $\mathit{p^{\prime}_{\mathit{i}}}$ of the outer case expression are also graded. Notably, this rule only holds when the patterns of the inner case expression are linear (i.e., variable or constant) so that there are no nested box patterns, represented via the $\textsf{lin}(\mathit{p_{\mathit{i}}})$ predicate. As with letrec, distributivity of functions over a case expression is given by CaseDistrib.

Lastly generalisation of an arbitrary boxed pattern to a variable is permitted through the CaseGen rule. Here, a boxed pattern $[\mathit{p_{\mathit{i}}}]$ and the output term of the case may be converted to a variable if the output term is equivalent to the pattern inside the box. The term $\mathit{t}$ being matched against must therefore have a grade approximatable by 1, as witnessed by the predicate ${\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}1}\,{\color[rgb]{0.0390625,0.25,0.6328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.25,0.6328125}\sqsubseteq}\,\mathit{r}$ in the typing derivation.

We consider here the properties of these derived operations. Prima facie, the above push and pull operations are simply distributive laws between two (parametric) type constructors $\mathsf{F}$ and $\Box_{r}$, the latter being the graded modality. However, both $\mathsf{F}$ and $\Box_{r}$ have additional structure. If the mathematical terminology of ‘distributive laws’ is warranted, then such additional structure should be preserved by push and pull (e.g., as in how a distributive law between a monad and a comonad must preserve the behaviour of the monad and comonad operations after applying the distributive law [26]); we explain here the relevant additional structure and verify the distributive law properties.

Firstly, we note that these distributive laws are mutually inverse:

Applying a mathematical perspective, $\Box_{r}$ is also an endofunctor with its object mapping provided by the type constructor itself and its morphism mapping behaviour defined as follows:

Not only is $\Box_{r}$ an endofunctor but it also has the structure of a graded comonad [11, 21, 24, 25].