___
/\_ \
__ _ _ __ ___ __ __\//\ \ __
/ _ \/\`'__\/ __ \ /' _ `\/\ \/\ \ \ \ \ /'__`\
/\ \_\ \ \ \//\ \_\ \_/\ \/\ \ \ \_\ \ \_\ \_/\ __/
\ \____ \ \_\\ \__/ \_\ \_\ \_\ \____/ /\____\ \____\
\/___/\ \/_/ \/__/\/_/\/_/\/_/\/___/ \/____/\/____/
/\____/
\_/__/
Granule is a functional programming language with a linear type system and fine-grained effects and coeffects via graded modal types.
An introduction to Granule can be found in our paper Quantitative program reasoning with graded modal types. More details of the project can be found on the project website.
Linearity means that the following is ill-typed:
dupBroken : forall {a : Type} . a -> (a, a)
dupBroken x = (x, x)However, 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)Combining indexed types and bounded reuse in Granule leads to an interesting type
for the standard map function 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)This type explains that the parameter function f is used exactly n times,
where n is the size of the incoming list. Linearity ensures that the entire
list is consumed exactly once to the produce the result.
Binary releases are currently available for MacOS only. If you need a newer release than is available then please open an issue.
To build Granule from source, make sure you have Z3 and Stack on your system.
Now run
git clone https://github.com/granule-project/granule \
&& cd granule \
&& stack setup \
&& stack install
This will instance the main frontend gr and the interactive mode
grepl.
More details about how to install can be found on the wiki page.
If you would also like to install the LLVM compiler (experimental and a work in progress) you can get this from its separate repo and install it via:
stack install :grc
Granule program files have file extension .gr. Use the gr command to run the interpreter:
$ gr examples/NonEmpty.gr
Checking examples/NonEmpty.gr...
OK, evaluating...
1
A good starting point for learning about Granule is the tutorial given in examples/intro.gr.md.
On Windows, you may have issues with unicode, for which there is a work around by
setting the code page to UTF-8 (via chcp.com 65001 https://stackoverflow.com/questions/25373116/how-can-i-set-my-ghci-prompt-to-a-lambda-character-on-windows). You may also want to run without colours
gr --no-color.
Granule has a very basic import system. When gr encounters a line import A.B.C anywhere in the file it will attempt to load the file located at
$GRANULE_PATH/A/B/C.gr, where $GRANULE_PATH defaults to StdLib, i.e. it
should work when you are running gr from within this project. For a more
stable setup which lets you run gr from any directory you can set the path
with the --include-path flag (see below).
Run gr with the --help flag for an overview of flags. Flags can be set
- in
~/.granule(the same way as on the command line) - on the command line
- at the top of the file (prepended with
-- gr)
and have precedence in that order, e.g. flags set on the command line will override flags in the config.
Example .granule file:
$ cat ~/.granule
--include-path /Users/alice/granule/StdLib
--solver-timeout 2000See here
for how to install completion scripts for your shell, although we recommend
dynamically loading the completions in your shell's startup script to account
for changes in gr's interface; e.g. for fish on MacOS:
echo "#granule
gr --fish-completion-script (which gr) | source" >> ~/.config/fish/config.fishWe aim to make Granule as inclusive as possible. If you experience any accessibility hurdles, please open an issue.
The --alternative-colors/--alternative-colours flag will cause success
messages to be printed in blue instead of green, which may help with colour
blindness.
The --no-color/--no-colour flag will turn off colours altogether.
The following symbols are interchangeable. You can destructively rewrite all
occurrences in your source file by passing
--ascii-to-unicode/--unicode-to-ascii. --keep-backup will save a backup of
the most recent copy of the input file with .bak appended.
| ASCII | Unicode |
|---|---|
forall |
∀ |
Inf |
∞ |
-> |
→ |
=> |
⇒ |
<- |
← |
/\ |
∧ |
\/ |
∨ |
<= |
≤ |
>= |
≥ |
== |
≡ |
\ |
λ |
Usages of the operator ∘ get parsed as an application of compose.
Granule has some basic support for literate programs with Markdown and TeX.
By default code in granule code environments will be run. This can be
overridden with the flag --literate-env-name.
The interpreter also takes markdown files with the extension .md, in which
case all fenced code blocks labelled with granule will get parsed as the input
source code. All other lines are ignored, but counted as whitespace to retain
line numbers for error messages.
# Example literate granule (markdown) file
Code blocks can be fenced with twiddles...
~~~ granule
a : Int
a = 1
~~~
... or backticks.
```granule
b : Int
b = 2
```
The following code blocks will get ignored.
~~~
int c = 3;
~~~
```haskell
d :: Int
d = 4
```You can run Granule on the TeX file below with gr --literate-env-name verbatim.
You can use XeLaTeX to properly display multi-byte Unicode characters.
\documentclass{article}
\title{Literate Granule (\TeX{}) Example}
\begin{document}
\author{Grampy Granule}
\maketitle
Writing things here.
\begin{verbatim}
import Prelude
foo : String
foo = "running code here"
\end{verbatim}
\end{document}Granule is a research project to help us gain intuitions about using linearity and graded modalities in programming. It is licensed under a permissive licence, so you can use it for whatever, but please don't write your next spaceship controller in Granule just yet. The interface is not stable (and nor is the code). You have been warned...
( All contributions are welcome! )
__// /
/.__.\
\ \/ /
'__/ \
\- )
\_____/
_____|_|______________________________________
" "