From f28def3912c2b5c3caf6a6b344ebd61e1c7656f0 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 17 Aug 2024 23:45:02 +0300 Subject: [PATCH] Update README --- README.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index cf173c6f..e1285826 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ Generating Efficient and Scope-Safe Abstract Syntax with Free (Scoped) Monads an This project provides an implementation of the efficient scope-safe representation for syntax with binders (think λ-abstraction, let-binding, for-loop, etc.). The underlying representation is based on the IFL 2022 paper by Maclaurin, Radul, and Paszke [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224)[^1]. This project extends the foil with patterns, as well as two -techniques for free generation of the foil. The details are presented in the paper [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384)[^2]. Also see the [slides from the ICCQ 2024 presentation](https://fizruk.github.io/files/iccq-2024-free-foil-slides.pdf). +techniques for free generation of the foil. The details are presented in the paper [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384)[^2]. Also see the [slides from the ICCQ 2024 presentation](https://fizruk.github.io/files/iccq-2024-free-foil-slides.pdf) (also [video](https://youtu.be/06gudJKXpkk?si=FbR03r-bngdZUdlf)). In brief, following the paper: @@ -25,12 +25,12 @@ In brief, following the paper: Additionally, we implement: -1. Tempalte Haskell generation for the free foil. +1. Template Haskell generation for the free foil. 2. Generalized support for patterns using `withPattern` method (currently in `CoSinkable`). 3. Generic α-equivalence for the free foil and α-equivalence support for patterns using `UnifiablePattern` typeclass. 4. Generic conversion functions for the free foil. -In addition to this repository, we have benchmarks the foil and the free foil against each other and other implementation of λ-calculus. +In addition to this repository, we have benchmarks for the foil and the 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)). ## Project structure @@ -49,12 +49,13 @@ The Haskell code is organized into two packages as follows: - [`Control.Monad.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil-TH.html) provides Template Haskell functions that generate scope-safe representation types together with some conversion functions and helpers for patterns. All of this is generated from a raw recursive representation of syntax, that has to be split into 4 types: type of variable identifiers, type of terms, type of scoped terms (to clearly understand which parts get under binders), and type of patterns. -- [`Control.Monad.Foil.Relative`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil-Relative.html) defines a variation of a relative monad typeclass specifcially indexed by scope type variables of kind `S`. This is merely for the demonstration that term type constructors are monads relative to [`Name`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil-Internal.html#t:Name). +- [`Control.Monad.Foil.Relative`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil-Relative.html) defines a variation of a relative monad typeclass specifically indexed by scope type variables of kind `S`. This is merely for the demonstration that term type constructors are monads relative to [`Name`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil-Internal.html#t:Name). - [`Control.Monad.Free.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Free-Foil.html) defines a variation of free scoped (relative) monads relying on the foil for the scope-safe efficient handling of the binders. This module also defines - generic substitution for this generic representation of syntax with binders - generic α-normalization and α-equivalence checks + - generic conversion helpers - [`Control.Monad.Free.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/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. @@ -76,9 +77,10 @@ Scala implementation is not documented yet. 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. We provide general support for patterns, but at the moment it does not allow terms or scoped terms inside patterns. +1. We do not (yet) generate α-equivalence via Template Haskell or `GHC.Generics`. However, we do provide generic α-equivalence functions for `AST sig n`, and demonstrate how to implement the check manually for λΠ-terms using the foil. +2. We do not (yet) demonstrate an implementation of the typechecker for λΠ in these representations. It should be largely straightforward, since the main non-trivial part is probably the equality for the Π-types, which relies on the α-equivalence from the previous item. +3. We provide general support for patterns, but at the moment it feels somewhat ad hoc (pending proper generalization of patterns) + and also does not allow terms or scoped terms inside patterns. Supporting terms in patterns would be desirable to enable type annotations in patterns or things like `ViewPatterns` in Haskell. 4. We do not (yet) provide strict versions of the foil and free foil here. The benchmarks, however, do implement these variations. 5. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/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`. @@ -90,5 +92,5 @@ In Haskell: 9. We do not (yet) provide a Church-encoded version of the free foil, which should improve its performance. [^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. -[^2]: Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. 2024. _Free Foil: Generating Efficient and Scope-Safe Abstract Syntax._ To appear in ICCQ 2024. +[^2]: Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. 2024. _Free Foil: Generating Efficient and Scope-Safe Abstract Syntax._ 4th International Conference on Code Quality (ICCQ), Innopolis, Russian Federation, 2024, pp. 1-16 (arXiv version at ) [^3]: Nikolai Kudasov. _Free Monads, Intrinsic Scoping, and Higher-Order Preunification._ To appear in TFP 2024.