| layout | mathjax | title |
|---|---|---|
page |
true |
Language |
Granule can be downloaded from Github and built and installed via stack. Please see the README for further instructions.
You can find a mini-tutorial on Granule here.
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 coeffects has been proposed as a unified 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 coeffect types can be integrated with effect types for resource reasoning with effects [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.. A full description of Granule can be found in our recent ICFP 2019 paper.
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
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 [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] -> a [2 * c] -> (b, b)
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 first 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 g uses 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 [_] Nil = Nil;
map [f] (Cons x xs) = Cons (f x) (map [f] xs)
The type parameter n is of type Nat which is the type of natural numbers and (a -> b) [n] is the type
of a function that must be used exactly n times.
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 map
to only the one above, modulo permutation of the elements. In other words: we get more theorems for free.
Example 2: Security Levels
Another modality available in Granule is indexed by a two-point security lattice with levels: Public and 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 secretHere 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 checkHowever, 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 [_] = [0]Example 3: Effects
A graded possibility modality provides tracking of side effects in the style of a graded monad and effect system. A type t <e> describes a computation returning a value of type t and producing side effects e.
In the following code, input (read) and output (write) operations to the stdio are tracked:
echo : () <{Stdin, Stdout}>
echo = let x <- fromStdin in toStdout x
Footnote: This page was adopted from this abstract Orchard and Liepelt.