Merge branch 'release-v0.4.0'

* release-v0.4.0: Bump version and update changelog Add documentation for sections and variables Make implicit use of variables an error Check that "used" vars are defined and used Fix warning in recId example Add "uses(...)" annotation Add anonymous sections Issue a warning for implicit assumptions Issue an error for unused variables Correctly collect free variables for a typed term Change recId example to use sections and variables Add Coq-style sections and variables add flake with cabal, hls, ghcjs, set up caching Apply stylish-haskell
rzk-lang · May 18, 2023 · f5dbfe3 · f5dbfe3
2 parents e31c70a + 5b1f8ac
commit f5dbfe3
Show file tree

Hide file tree

Showing 32 changed files with 7,992 additions and 6,718 deletions.
diff --git a/.envrc b/.envrc
@@ -0,0 +1,2 @@
+use flake
+eval "$shellHook"
diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
@@ -18,24 +18,35 @@ on:
 
   workflow_dispatch:  # allow triggering this workflow manually
 
+env:
+  store: /home/runner/nix
+
+permissions:
+  contents: write
+
 jobs:
   build-and-deploy:
     runs-on: ubuntu-latest
     steps:
       - name: 📥 Checkout repository
         uses: actions/checkout@v3
 
-      - name: 🧰 Setup nix (cache)
-        uses: cachix/install-nix-action@v13
+      - name: 🧰 Setup nix
+        uses: cachix/install-nix-action@v20
         with:
-          nix_path: nixpkgs=channel:nixos-unstable
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+          extra_nix_config: "store = ${{ env.store }}\nsubstituters = https://cache.nixos.org/ https://cache.iog.io https://nix-community.cachix.org https://miso-haskell.cachix.org \ntrusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= nix-community.cachix.org-1:mB9FSh9qf2dCimDSUo8Zy7bkq5CX+/rkCWyvRCYg3Fs= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= miso-haskell.cachix.org-1:6N2DooyFlZOHUfJtAx1Q09H0P5XXYzoxxQYiwn6W1e8="
           # pinning Nix version
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-
-      - name: 💾 Setup cachix (miso-haskell)
-        uses: cachix/cachix-action@v10
+          install_url: https://releases.nixos.org/nix/nix-2.14.1/install
+      
+      - name: Restore and cache Nix store
+        uses: actions/[email protected]
         with:
-          name: miso-haskell
+          key: ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock') }}
+          path: ${{ env.store }}
+          restore-keys: |
+            ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock') }}
+            ${{ runner.os }}-nix-
 
       - name: 🔨 Remove rzk.cabal, lexer and parser generator files
         run: |
@@ -45,20 +56,20 @@ jobs:
 
       - name: 🔨 Build GHCJS version with Nix
         run: |
-          nix-build try-rzk/
+          nix build .#try-rzk
 
       - name: 🔨 Collect build artifacts
         run: |
           mkdir -p dist/result/bin
-          cp -r ./result/bin/try-rzk.jsexe/ dist/result/bin/.
+          cp -r ${{ env.store }}$(realpath result)/bin/try-rzk.jsexe/ dist/result/bin/.
           chmod -R +w dist/
           cp try-rzk/playground.html dist/.
 
       - name: "📘 Publish JS \"binaries\" (${{ github.ref_name }})"
         if: ${{ github.ref_name != 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}
+          token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           target-folder: ${{ github.ref_name }}
           clean: false
@@ -67,6 +78,6 @@ jobs:
         if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}
+          token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           clean: false
diff --git a/.gitignore b/.gitignore
@@ -24,3 +24,5 @@ cabal.project.local~
 .HTF/
 .ghc.environment.*
 docs/site
+result
+.direnv
diff --git a/README.md b/README.md
@@ -132,7 +132,73 @@ nix-build
 
 Now open `playground.html` to see the result. Note that if local GHCJS build is unavailable, `playground.html` will use the [JS file from GitHub Pages](https://fizruk.github.io/rzk/v0.1.0/result/bin/try-rzk.jsexe/all.js) as a fallback.
 
-# References
+##### Flake
+
+The flake in this repository allows to build `try-rzk` incrementally and reproducibly.
+
+1. Install `Nix` via single-user [installation](https://nixos.org/download.html#download-nix):
+
+   1. Run script
+
+     ```sh
+     sh <(curl -L https://nixos.org/nix/install) --no-daemon
+     ```
+
+   1. Permanently [enable](https://nixos.wiki/wiki/Flakes#Permanent) flakes
+
+1. Enter the `devShell` with `GHC` (not `GHCJS`). Answer `y` to `Nix` prompts to use binary caches.
+
+    ```sh
+    nix develop
+    ```
+
+1. The shell provides `ghc`, `haskell-language-server`, `cabal-install`, `hpack`.
+
+1. (Optionally) Install [direnv](https://direnv.net/) to start the `devShell` when you enter the repository directory.
+
+1. Build `rzk`.
+
+    ```sh
+    cabal build
+    ```
+
+1. Enter the `devShell` with `GHCJS`.
+
+    ```sh
+    nix develop .#ghcjs
+    ```
+
+1. Build `try-rzk`. This may require ~10 GB of RAM.
+
+    ```sh
+    cabal build --ghcjs
+    ```
+
+1. (Optionally) Build `rzk` via `Nix`. The resulting executable will be in `result/bin/rzk`.
+
+    ```sh
+    nix build .#rzk
+    ```
+
+1. (Optionally) Run `rzk` via `Nix`.
+
+    ```sh
+    nix run .#rzk
+    ```
+
+1. (Optionally) Build `try-rzk` via `Nix`. This may require ~10 GB of RAM. The resulting executable will be in `try-rzk/result/bin/try-rzk.jsexe`.
+
+    ```sh
+    nix build .#try-rzk --out-link try-rzk/result
+    ```
+
+1. Open the app in a browser.
+
+    ```sh
+    firefox try-rzk/playground.html
+    ```
+
+## References
 
 1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442
 2. Nikolai Kudasov. E-unification for Second-Order Abstract Syntax. 2023. https://arxiv.org/abs/2302.05815

diff --git a/cabal.project b/cabal.project
@@ -0,0 +1 @@
+packages: rzk try-rzk
diff --git a/docs/docs/rzk-1/recId.md b/docs/docs/rzk-1/recId.md
@@ -84,12 +84,21 @@ The idea is straightforward. We ask for a proof that `a = b` for all points in `
 First, we define how to restrict an extension type to a subshape:
 
 ```rzk
+#section construction-of-recId
+
+#variable r : relfunext2
+#variable I : CUBE
+#variables psi phi : I -> TOPE
+#variable A : {t : I | psi t \/ phi t} -> U
+
 -- Restrict extension type to a subshape.
-#def restrict
-    (I : CUBE)
-    (psi : I -> TOPE)
-    (phi : I -> TOPE)
-    (A : {t : I | psi t \/ phi t} -> U)
+#def restrict_phi
+    (a : {t : I | phi t} -> A t)
+  : {t : I | psi t /\ phi t} -> A t
+  := \t -> a t
+
+-- Restrict extension type to a subshape.
+#def restrict_psi
     (a : {t : I | psi t} -> A t)
   : {t : I | psi t /\ phi t} -> A t
   := \t -> a t
@@ -99,13 +108,15 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
-#def ext-of-restrict
-    (I : CUBE)
-    (psi : I -> TOPE)
-    (phi : I -> TOPE)
-    (A : {t : I | psi t \/ phi t} -> U)
+#def ext-of-restrict_psi
     (a : {t : I | psi t} -> A t)
-  : (t : psi) -> A t [ psi t /\ phi t |-> restrict I psi phi A a t ]
+  : (t : psi) -> A t [ psi t /\ phi t |-> restrict_psi a t ]
+  := a  -- type is coerced automatically here
+
+-- Reformulate extension type as an extension of a restriction.
+#def ext-of-restrict_phi
+    (a : {t : I | phi t} -> A t)
+  : (t : phi) -> A t [ psi t /\ phi t |-> restrict_phi a t ]
   := a  -- type is coerced automatically here
 ```
 
@@ -114,15 +125,10 @@ Now, assuming relative function extensionality, we construct a path between rest
 ```rzk
 -- Transform extension of an identity into an identity of restrictions.
 #def restricts-path
-    (r : relfunext2)
-    (I : CUBE)
-    (psi : I -> TOPE)
-    (phi : I -> TOPE)
-    (A : {t : I | psi t \/ phi t} -> U)
     (a_psi : (t : psi) -> A t)
     (a_phi : (t : phi) -> A t)
     (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
-  : restrict I psi phi A a_psi = restrict I phi psi A a_phi
+  : restrict_psi a_psi = restrict_phi a_phi
   := (first (second (r I
       (\t -> psi t /\ phi t)
       (\t -> BOT)
@@ -138,12 +144,7 @@ Finally, we bring everything together into `recId`:
 -- A weaker version of recOR, demanding only a path between a and b:
 -- recOR(psi, phi, a, b) demands that for psi /\ phi we have a == b (definitionally)
 -- (recId psi phi a b e) demands that e is the proof that a = b (intensionally) for psi /\ phi
-#def recId
-    (r : relfunext2)
-    (I : CUBE)
-    (psi : I -> TOPE)
-    (phi : I -> TOPE)
-    (A : {t : I | psi t \/ phi t} -> U)
+#def recId uses (r) -- we declare that recId is using r on purpose
     (a_psi : (t : psi) -> A t)
     (a_phi : (t : phi) -> A t)
     (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
@@ -152,13 +153,15 @@ Finally, we bring everything together into `recId`:
         psi t |-> transport
           ({s : I | psi s /\ phi s} -> A s)
           (\ra -> (s : psi) -> A s [ psi s /\ phi s |-> ra s ])
-          (restrict I psi phi A a_psi)
-          (restrict I phi psi A a_phi)
-          (restricts-path r I psi phi A a_psi a_phi e)
-          (ext-of-restrict I psi phi A a_psi)
+          (restrict_psi a_psi)
+          (restrict_phi a_phi)
+          (restricts-path a_psi a_phi e)
+          (ext-of-restrict_psi a_psi)
           t,
-        phi t |-> ext-of-restrict I phi psi A a_phi t
+        phi t |-> ext-of-restrict_phi a_phi t
       )
+
+#end construction-of-recId
 ```
 
 ## Gluing extension types

diff --git a/docs/docs/rzk-1/sections.md b/docs/docs/rzk-1/sections.md
@@ -0,0 +1,126 @@
+# Sections and Variables
+
+Sections and variables allow to simplify definitions by factoring out common assumptions.
+
+!!! hint "Coq-style variables"
+    `rzk` implements variables similarly to
+    <a href="https://coq.inria.fr/refman/language/core/assumptions.html#coq:cmd.Variable" target="_blank">`Variable` command in Coq</a>.
+    An important difference is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
+    This is, perhaps, somewhat related to <a href="https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:exn.Section-variable-‘ident’-occurs-implicitly-in-global-declaration-‘qualid’-present-in-hypothesis-‘ident’" target="_blank">this error message in Coq</a>.
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+## Variables
+
+Consider the following definitions:
+
+```rzk
+#def compose₁
+  (A B C : U)
+  (g : B -> C)
+  (f : A -> B)
+  : A -> C
+  := \x -> g (f x)
+
+#def twice₁
+  (A : U)
+  (h : A -> A)
+  : A -> A
+  := \x -> h (h x)
+```
+
+Since it might be common to introduce types `A`, `B`, and `C`, we can declare these are variables:
+
+```rzk
+#variables A B C : U
+
+#def compose₂
+  (g : B -> C)
+  (f : A -> B)
+  : A -> C
+  := \x -> g (f x)
+
+#def twice₂
+  (h : A -> A)
+  : A -> A
+  := \x -> h (h x)
+```
+
+The `#variables` command here introduces assumptions, which can be used in the following definitions. Importantly, after checking a file (module), all definitions will have the assumptions used (explicitly or implicitly) attached as bound variables.
+
+### Implicitly used variables (and `uses`)
+
+We can try going even further and declare variables `f`, `g`, `h`, and `x`:
+
+```rzk
+#variable g : B -> C
+#variable f : A -> B
+#variable h : A -> A
+#variable x : A
+
+-- #def bad-compose₃ : C := g (f x)  -- ERROR: implicit assumptions A and B
+#def twice₃ : A := h (h x)
+```
+
+Note how this definition of `bad-compose₃` is implicitly dependent on the types `A` and `B`, which is promptly noted by `rzk`, which issues an error (if we uncomment the corresponding line):
+
+```text
+implicit assumption
+  B : U
+used in definition of
+  bad-compose₃
+```
+
+To let `rzk` know that this is not accidental, we can add `uses (...)` annotation to specify a list of variables implicitly used in the definition:
+
+```rzk
+#def compose₃ uses (A B) : C := g (f x)
+```
+
+## Sections
+
+To introduce assumption variables temporarily inside of one file, you can use sections:
+
+```rzk
+#section example-1
+
+#variables X Y Z : U
+#variable k : X -> X
+#variable x' : X
+
+#def compose₄
+  (g : Y -> Z)
+  (f : X -> Y)
+  : X -> Z
+  := \x -> g (f x)
+
+#def twice₄ : X := k (k x')
+
+#end example-1
+```
+
+Now, once outside of the section, `compose₄` and `twice₄` obtain corresponding parameters
+(only those used, explicitly or implicitly):
+
+```rzk
+-- compose₄ : (X : U) -> (Y : U) -> (Z : U) -> (g : Y -> Z) -> (f : X -> Y) -> (X -> Z)
+-- twice₄ : (X : U) -> (k : X -> X) -> (x' : X) -> X
+
+#def twice₅
+  (T : U)
+  (e : T -> T)
+  : T -> T
+  := compose₄ T T T e e
+
+#def identity
+  (T : U)
+  : T -> T
+  := twice₄ T (\t -> t)
+```
+
+!!! warning "Lack of indentation"
+    `rzk` currently does not support indentation, so all definitions and commands inside a section (including nested sections) have to start at the beginning of a line.
-Original file line number
+Diff line change
@@ Expand Up / @@ -24,3 +24,5 @@ cabal.project.local~ @@
     .HTF/
     .ghc.environment.*
     docs/site
+    result
+    .direnv