Granule, a linear functional language with graded modal types

What graded modalities change about the type system

Granule is a functional programming language with a linear type system and fine-grained effects and coeffects via graded modal types, and the README's own framing of the field is quantitative program reasoning, with the introductory paper linked from the Kent research group.

The idea is best understood through the example the README gives. Linearity means this is ill-typed:

dupBroken : forall {a : Type} . a -> (a, a)
dupBroken x = (x, x)

The parameter is used twice, and a linear type system forbids that. But a graded modality can be employed to explain exactly how many times the parameter here can be used:

dup : forall {a : Type} . a [2] -> (a, a)
dup [x] = (x, x)

The 2 in brackets is the grade. Instead of saying this value is used zero or one times, the type says it is used exactly twice, and the pattern match in the definition has to consume it accordingly. The square brackets in the pattern are the matching side of the same idea, so the use count is checked in the definition rather than assumed.

The payoff comes when you combine that with indexed types, and the README works through the standard map on sized lists, vectors:

--- Map function
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 explains that the parameter function f is used exactly n times, where n is the size of the incoming list. Linearity ensures the entire list is consumed exactly once to produce the result. So the type is not just describing the input shape, it is stating a resource discipline, and the compiler will reject a map that ignores part of the list or uses the function one time too few.

That is the contribution. Linear types say used exactly once. Unbounded types say nothing. Graded modalities say exactly n, and because the grade is a semiring you can also add grades, so an effect of one and an effect of another combine into a total.

The same machinery carries effects and coeffects, which is what lets the language talk about not only how much of a value is consumed but what state is read and written, and the README points at the standard library documentation for the details of the implementation.

Installing and building it

The installation story is where the project shows its research character.

Binary releases are currently available for MacOS only, and if you need a newer release than is available you are asked to open an issue. That is an honest statement about the state of the tooling rather than a gap, but it does mean most people build from source.

To build from source you need Z3 and Stack on your system, and the README gives the sequence:

git clone https://github.com/granule-project/granule \
    && cd granule \
    && stack setup \
    && stack install

The Z3 dependency is the interesting one. A type system with graded modalities needs a solver to check the grade constraints, and Z3 is doing that work. That also means the type checker is not a simple syntactic pass, so a badly configured solver installation shows up as confusing type errors rather than a clear dependency message.

The stack install instantiates two executables, the main frontend gr and the interactive mode grepl, and there is a separate LLVM compiler in a separate repository, granule-compiler-llvm, installed with stack install :grlc and described as experimental and a work in progress.

The separation of the two back ends is worth noting. The primary route is Granule to Haskell, through a compiler called grc, which takes a .gr file and outputs a .hs file that imports the Language.Granule.Runtime module, and the README notes you need that module on your path if you want to compile the resulting Haskell. The LLVM route is the more ambitious one and is explicitly the less finished one.

More detail is on the project's wiki page for installing Granule.

The project is BSD-3-Clause licensed, implemented in Haskell, on the main branch, with the last push on 2026-07-21. The published releases are older: v0.9.4.1 as an ESOP2024 artefact in January 2024, v0.9.5.0 in March 2024 and v0.9.6.0 in November 2024. So the repository is being worked on ahead of the published versions.

Running the checker, the interpreter and the documentation generator

The toolchain is small, which is what a research language usually looks like.

Granule program files have the .gr extension, and the gr command runs the interpreter. The example in the README is a three-line transcript:

$ gr examples/NonEmpty.gr
Checking examples/NonEmpty.gr...
OK, evaluating...
1

The order of those lines is the point. Checking comes before evaluating, and it is the checker that consults the grades. So the interpreter is not a dynamic evaluator that discovers type errors at runtime, it type-checks first and refuses to run a program that does not satisfy its resource obligations.

The tutorial in examples/intro.gr.md is named as a good starting point for learning the language, which is a sensible choice given that the type system is the thing you need to understand before the syntax makes sense.

Documentation is generated from the source with a compiler flag rather than by a separate tool. The gr --grdoc filename command generates documentation into the docs directory of the compiler top level, and the README shows generating the whole standard library with:

gr --grdoc StdLib/*.gr
gr --grdoc StdLib/*.gr

The second run is not a mistake. The README notes that the second run stabilises the hyperlinks between modules for multi-file runs, which is a detail about incremental documentation generation rather than about the language, and it is a good illustration of the kind of thing a research project does not document everywhere.

Two platform caveats are in the README. On Windows you may have issues with unicode, with a work around of setting the code page to UTF-8 via chcp.com 65001. And you may want to run without colours with gr --no-color, which is the sort of thing that matters when output is piped into a file or a CI log.

The import system is described as very basic, and the behaviour is worth knowing: when gr encounters a line import A.B.C anywhere in the file it will first look for it in a specific place, which is a simpler scheme than the module systems of mature languages and means the import path is something you have to match by hand rather than infer.

Where Granule fits, and what it is really for

The honest framing is that Granule is a research vehicle for quantitative program reasoning, and the README's own description of the field says so. The paper is the primary output and the language is the instrument for it.

The comparison with the established alternatives in the type systems world is instructive. Linear type systems exist elsewhere, but linear is a special case of graded and the extra expressiveness is what the research is about, as is combining it with effects and coeffects in one type system.

What Granule offers over those is the combination in one language. Linear types, graded modalities for exact counts, effects and coeffects, and the addition of grades as a semiring, all in a single type system rather than layered features.

The practical limits are substantial and they are not hidden. The published releases are from 2024 while the repository keeps moving, the binary distributions are MacOS only, the LLVM backend is experimental, the import system is basic, and there is no package ecosystem to speak of. The standard library documentation exists and is generated from the source, which is the main way to learn the language beyond the paper and the tutorial.

For a team, the sensible way to approach this is as research to read and experiment with rather than as a language to adopt. If you are designing a type system with resource accounting, the implementation is a reference that shows how the grades are checked, with Z3 doing the constraint solving, and the examples in the repository are more instructive than a specification would be. If you want to ship software, the ecosystem is not there.

The one thing worth trying first is the graded map example from the README, because it is small, it demonstrates the entire thesis in a few lines, and it shows what the paper's claims mean in practice.

Editorial conclusion

Adopt Granule if you are working on quantitative program reasoning, verified resource usage or effect systems and want a type system that expresses bounded reuse rather than just linear or unbounded use. Skip it if you want a practical production language, since the releases are old and the project is a research one. Verify first by building it from source with Stack and Z3 present, since the binary releases are MacOS only, and by type-checking the intro example before assuming the tooling works on your platform.

Frequently asked questions

Official sources

1. granule-project/granule on GitHub
2. License: BSD-3-Clause
3. Project website
4. README
5. Releases