Fix lambda-pi links in README

README.md

@@ -24,11 +24,13 @@ techniques for free generation of the foil. The details are presented in the pap
 In addition to this repository, we have benchmarks comparing foil and free foil against each other and other implementation of λ-calculus.
 See [KarinaTyulebaeva/lambda-n-ways](https://github.com/KarinaTyulebaeva/lambda-n-ways), a fork of Stephanie Weirich's benchmark suite ([sweirich/lambda-n-ways](https://github.com/sweirich/lambda-n-ways)).
 
-## Module structure
+## Project structure
 
 ### Haskell
 
-The Haskell code is organized into multiple modules as follows:
+The Haskell code is organized into two packages as follows:
+
+#### `free-foil` package
 
 - [`Control.Monad.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html) provides basic definitions for the foil[^1], including safe scopes, sinking, name maps, and scope constraints. In addition to the standard definitions, we contribute
 
@@ -45,11 +47,17 @@ The Haskell code is organized into multiple modules as follows:
   - generic substitution for this generic representation of syntax with binders
   - generic α-normalization and α-equivalence checks
 
-- [`Language.LambdaPi.Impl.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Language-LambdaPi-Impl-Foil.html) defines a simple interpreter for λΠ-calculus with pairs, using the manually constructed scope-safe representation and conversion to and from the raw representation generated by BNFC.
+- [`Control.Monad.Free.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil-TH.html) provides Template Haskell functions that generate helpers specifically for free foil, including the generation of the signature bifunctor, convenient pattern synonyms, conversion helpers, and instances needed to enable general α-equivalence.
+
+#### `lambda-pi` package
+
+- [`Language.LambdaPi.Impl.Foil`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.0.2/Language-LambdaPi-Impl-Foil.html) defines a simple interpreter for λΠ-calculus with pairs, using the manually constructed scope-safe representation and conversion to and from the raw representation generated by BNFC.
+
+- [`Language.LambdaPi.Impl.FoilTH`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.0.2/Language-LambdaPi-Impl-FoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using Template Haskell to generate a large portion of the code.
 
-- [`Language.LambdaPi.Impl.FoilTH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Language-LambdaPi-Impl-FoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using Template Haskell to generate a large portion of the code.
+- [`Language.LambdaPi.Impl.FreeFoil`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.0.2/Language-LambdaPi-Impl-FreeFoil.html) defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach.
 
-- [`Language.LambdaPi.Impl.FreeFoil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Language-LambdaPi-Impl-FoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach.
+- [`Language.LambdaPi.Impl.FreeFoilTH`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.0.2/Language-LambdaPi-Impl-FreeFoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach together with Template Haskell generation. This implementation has the most automation and generality.
 
 ### Scala
 
@@ -61,13 +69,12 @@ In Haskell:
 
 1. We do not (yet) generate α-equivalence via Template Haskell or `GHC.Generics`. We do provide a generic α-equivalence functions for `AST sig n`, and demonstrate how to implement the check manually for λΠ-terms using the foil, but in generating this from Template Haskell or using GHC.Generics is left for future work.
 2. We do not (yet) demonstrate an implementation of the typechecker for λΠ in these representations. While it is largely straightforward the main non-trivial part is the equality for the Π-types, which relies on the α-equivalence from the previous item.
-3. The free foil does not (yet) support patterns, only single-variable binders. While we think it should be sufficient to parametrize [`AST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:AST) and [`ScopedAST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:ScopedAST) with a `pattern` type constructor (e.g. literally the same [`Pattern`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Language-LambdaPi-Impl-Foil.html#t:Pattern) type used in the foil examples), we did not check if everything generalizes well enough.
-4. Template Haskell generates the foil, but not (yet) free foil. We believe there should be no problems in implementing TH-generation for the free foil, achieving the best of both worlds: generating the signature bifunctor together with conversion functions while getting [`substitute`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#v:substitute) (and, potentially, other useful algorithms[^3]) for free (except, as our benchmarks show, a moderate slowdown in performance should be expected compared to the foil).
-5. We do not (yet) provide strict versions of the foil and free foil here. The benchmarks, however, do implement these variations.
-6. We do not (yet) generate pattern synonyms for the foil with Template Haskell, however, this can be done easily, similarly to [this implementation](https://github.com/rzk-lang/rzk/blob/013b4126adeefe69dc757e38e18cd17a79b5a0fc/rzk/src/Free/Scoped/TH.hs) for free scoped monad.
-7. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:Sinkable) instances via Template Haskell at the moment. However, a safer and more flexible derivation should be possible via `GHC.Generics`.
-8. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil-Relative.html#v:rbind) take in an extra argument of type `Scope n`, which is meant to be the runtime counterpart of the (phantom) type parameter `n :: S`. It might be possible to use [`singletons`](https://hackage.haskell.org/package/singletons) or a similar technique to avoid explicit passing of this argument, making the interface somewhat cleaner. However, since this would change the interface a lot, we do not plan on implementing this approach here.
-9. Dealing with scopes generically might enable generic delayed substitution, which plays a big part in normalization by evaluation (NbE) algorithms (which outperform naïve substitution-based evaluation). It should be possible to provide a generic framework for closures of scoped terms and delayed substitutions, but we have not yet investigated that fully.
+3. The free foil does not (yet) support patterns, only single-variable binders. While we think it should be sufficient to parametrize [`AST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:AST) and [`ScopedAST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:ScopedAST) with a `pattern` type constructor (e.g. literally the same [`Pattern`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.0.2/Language-LambdaPi-Impl-Foil.html#t:Pattern) type used in the foil examples), we did not check if everything generalizes well enough.
+4. We do not (yet) provide strict versions of the foil and free foil here. The benchmarks, however, do implement these variations.
+5. We do not (yet) generate pattern synonyms for the foil with Template Haskell, however, this can be done easily, similarly to [this implementation](https://github.com/rzk-lang/rzk/blob/013b4126adeefe69dc757e38e18cd17a79b5a0fc/rzk/src/Free/Scoped/TH.hs) for free scoped monad.
+6. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:Sinkable) instances via Template Haskell at the moment. However, a safer and more flexible derivation should be possible via `GHC.Generics`.
+7. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil-Relative.html#v:rbind) take in an extra argument of type `Scope n`, which is meant to be the runtime counterpart of the (phantom) type parameter `n :: S`. It might be possible to use [`singletons`](https://hackage.haskell.org/package/singletons) or a similar technique to avoid explicit passing of this argument, making the interface somewhat cleaner. However, since this would change the interface a lot, we do not plan on implementing this approach here.
+8. Dealing with scopes generically might enable generic delayed substitution, which plays a big part in normalization by evaluation (NbE) algorithms (which outperform naïve substitution-based evaluation). It should be possible to provide a generic framework for closures of scoped terms and delayed substitutions, but we have not yet investigated that fully.
 
 [^1]: Dougal Maclaurin, Alexey Radul, and Adam Paszke. 2023. _The Foil: Capture-Avoiding Substitution With No Sharp Edges._ In Proceedings of the 34th Symposium on Implementation and Application of Functional Languages (IFL '22). Association for Computing Machinery, New York, NY, USA, Article 8, 1–10. <https://doi.org/10.1145/3587216.3587224>
 [^2]: Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. 2024. _Free Foil: Generating Efficient and Scope-Safe Abstract Syntax._ To appear in ICCQ 2024. <https://arxiv.org/abs/2405.16384>