diff --git a/README.md b/README.md index f21dace5..fbdec0f9 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,7 @@ # Free Foil +[![Haddock]()](https://fizruk.github.io/free-foil/haddock/) + Generating Efficient and Scope-Safe Abstract Syntax with Free (Scoped) Monads and Template Haskell. ## About @@ -9,10 +11,28 @@ 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]. In brief: -1. We introduce `CoSinkable` typeclass to generalize `NameBinder`s to more complex patterns. +1. We introduce [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Foil.html#t:CoSinkable) typeclass to generalize `NameBinder`s to more complex patterns. 2. We provide Template Haskell machinery to generate the proper scope-safe AST definitions as well as conversion functions, and helpers for patterns. This approach works particularly well with the code generated by tools like [BNFC](https://bnfc.digitalgrammars.com) or [`BNFC-meta`](https://hackage.haskell.org/package/BNFC-meta). 3. We define a variant of free scoped monads[^3] with the foil instead of nested data types of Bird and Paterson. This approach allows implementing certain functions once for a large class of languages with binders. Here we implement only substitution, but more involved algorithms, such as generic higher-order preunification[^3] should be possible. +## Module structure + +The code is organized into multiple modules as follows: + +- [`Control.Monad.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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 [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Foil.html#t:CoSinkable) class (dual to [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Foil.html#t:Sinkable), for patterns that generalize `NameBinder`) and a general total [`NameMap`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Foil.html#g:4) which is useful for some implementations (e.g. conversion functions). + + - [`Control.Monad.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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.1/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.1/Control-Monad-Foil-Internal.html#t:Name). + +- [`Control.Monad.Free.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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. + +- [`Language.LambdaPi.Impl.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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/free-foil-0.0.1/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/free-foil-0.0.1/Language-LambdaPi-Impl-FoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach. + [^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. [^3]: Nikolai Kudasov. _Free Monads, Intrinsic Scoping, and Higher-Order Preunification._ To appear in TFP 2024.