SPLV’23 Material

Getting Granule

You have a few options:

• Local install: The latest release is v0.9.4.0. There are binaries for Mac OSX (arm64) and Linux, and you will also need to install Z3. However, you may need to build yourself if your platform isn’t provided for.

• Docker: Official Docker image of v0.9.4.0. The following command puts you into grepl with the local directory mounted as /host

   docker run -v $(pwd):/host --interactive docker.io/raehik/granule-repl:dev-minor
  

• Online (old version): There is an online version although it is running an older version of Granule and won’t work for all examples.

Materials

• Library documentation
• Exercises (solutions for Sections 1-4, solutions for Section 5)
• Slides
  • Part 1 - Theory and practice of linear types
  • Part 2 - Extending from linear types to graded types
    • Code demos from Parts 1 & 2
  • Part 3 - Communication, uniqueness, and mutation
    • Code from part 3
  • Part 4 - Grades in the wild via “graded base” and graded monads
    • Code from part 4
    • Effect code from part 4
    • Linear Haskell code from part 4
• Bonus session: Programming for the Future

Granule Language Server and VSCode Extension

There is an extension for VSCode that you can get in the usual way from inside VSCode:

This uses the Granule Language Server (grls) if you want to get support in any other editor that support the LSP.

Additional key bindings in vscode:

• Ctrl-e Ctrl-e: attempts to synthesis a goal in a hole (written either ? or {! !}.
• Ctrl-e Ctrl-h: attempts to rewrite the non-empty hole under the cursor (if there is one)
• Ctrl-e Ctrl-u: converts ASCII characters to their Unicode equivalents in the whole file.
• Ctrl-e Ctrl-a: converts Unicode characters to their ASCII equivalents in the whole file.