The Granule Language
Many modern programs are resource sensitive, that is, the amount of resources (e.g., energy, bandwidth, time, memory), and their rate of consumption, must be carefully managed. Furthermore, many programs handle sensitive resources, such as passwords, location data, photos, and banking information. Ensuring that private data is not inadvertently leaked is as important as the functional input-output behaviour of a program.
Various type-based solutions have been provided for reasoning about and controlling resources. A general class of program behaviours called coeﬀects has been proposed as a uniﬁed framework for capturing different kinds of resource analysis in a single type theory [Petricek et al., Petricek et al., Brunel et al., Gaboardi et al., Ghica et al., Breuvart et al.]. Recently it has been shown how coeﬀect types can be integrated with eﬀect types for resource reasoning with eﬀects [Gaboardi et al.].
To gain experience with such type systems for real-world programming tasks, and as a vehicle for further research, we are developing Granule, a functional programming language based on the linear λ-calculus augmented with graded modal types, inspired by the coeffect-effect calculus of Gaboardi et al..
Graded Modal Type Theory
A graded modality is an indexed family of modalities with some additional structure on the indices which mirrors the structure of the axioms/proof rules. For example, the exponential modality of linear logic has a graded counterpart in Bounded Linear Logic [Girard et al.], where is replaced with a family of modalities indexed by the natural numbers (the reuse bound). The operations of the usual natural number semiring are then used in the axioms/rules of the logic e.g., the transitivity axiom is . There are various different examples in the literature under the name of coeffects which provide ﬁne-grained analysis of resources and context-dependence via graded necessity modalities.
The goal with Granule is to support arbitrary, user-customisable graded modalities to enable fine-grained, quantitative program reasoning. At the moment, there are three built-in modalities: BLL-style resource-bounded graded necessity, a security-lattice graded necessity, and an effect-graded possibility modality for I/O. Type checking is based on a bidirectional algorithm, interfacing with the Z3 SMT solver to discharge constraints.
Example 1: Reuse Bounds
The following is a valid Granule program:
dup : forall (a : Type) . a |2| -> (a, a) dup |x| = (x, x)
This specifies the function
dup which takes a value and turns it into a pair by duplicating it. The
first parameter is therefore used non-linearly. If we were to try to give this the type
a -> (a, a) then
the type checker would complain of a linearity violation. Instead, since we are using the parameter
non-linearly, the type above describes this non-linear use via the resource bound
2 attached via
a graded modal type. The type
a |n| can be read as a boxed value of type
a which, when unboxed,
can be used
n times. This type is equivalent to in Girard et al.’s notation. The pattern match
|x| discharges the incoming modality and binds
x as a non-linear variable.
Let’s see a bit more of Granule, where the grading is made polymorphic:
twice : forall (a : Type, b : Type, c : Nat) . (a |c| -> b) |2| -> (b, b) |(2 * c)| -> Int twice |g| |x| = (g |x|, g |x|) main : ((Int, Int), (Int, Int)) main = twice |dup| |1|
Looking at the type signature for twice, we can deduce that it is a higher-order function: its ﬁrst parameter is a unary function whose parameter is used non-linearly exactly
c times and which returns a
b. The second parameter of
twice is used non-linearly exactly
2 * c times, since
c copies of its first parameter and is applied twice. This example shows Granule’s support of coeffect polymorphism.
So far these examples have been a little trivial. Let’s see something more interesting that mixes
the linearity + graded modality idea with indexed types. Granule provides indexed types such as
sized-indexed vectors. This enables the following definition for
map on vectors:
map : forall (a : Type, b : Type, n : Nat=) . (a -> b) |n| -> Vec n a -> Vec n b map |f| ys = case ys of Nil -> Nil; (Cons x xs) -> Cons (f x) (map |f| xs)
The type paraemter
n is of type
Nat= which is the type of natural numbers which are discretely ordered.
This means that the type
(a -> b) |n| is the type of a function that must be used exactly
Thus, this type says that we must use the parameter function exactly the number of times as the length
of the incoming vector. This significantly cuts down the number of possible implementation of
to only the one above, or with permutations of constant-sized sublists whilst applying the map.
Example 2: Security Levels
Another modality available in Granule is indexed by a two-point security lattice with levels:
Private. For example:
secret : Int |Private| secret = |42| -- specified as private dub : forall (l : Level) . Int |l| -> Int |l| -- at any level dub |x| = |(x + x)| -- ...double an int main : Int |Private| main = dub secret -- double the secret
main is marked as a high-security value (private) via its modal type. The
dub function appears doubles the integer parameter and its type tracks security levels and is level-polymorphic. It takes an integer at any level
l, returning a value at the same level. Crucially, the following program is ill-typed:
leak : Int |Private| -> Int |Public| leak |x| = |x| -- fails to type check
However, we can define a well-typed constant function that discards its high-security value to produce a low-security value by combining resource bounds with security levels:
notALeak : Int |Private| |0| -> Int |Public| notALeak x = |0|
Example 3: Eﬀects
A graded possibility modality provides tracking of side eﬀects in the style of a graded monad and eﬀect system. A type
<t> f describes a computation returning a value of type
t and producing side eﬀects
In the following code, input (
read) and output (
write) operations to the stdio are tracked:
echo : Int <[R, W]> echo = let x <- read in write x
The following shows both reuse bound coeffects and I/O effects coming together, explaining the side-effects of twice applying some integer function which has a read eﬀect:
doTwice : (Int -> Int <[R]>) |2| -> Int |2| -> Int <[R, R]> doTwice |f| |x| = let a <- f x in let b <- f x in pure (a + b)
Footnote: This page was adopted from this abstract Orchard and Liepelt.