Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads).
BSD-3-CLAUSE License
Generating Efficient and Scope-Safe Abstract Syntax with Free (Scoped) Monads and Template Haskell (with a partial port to Scala).
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»[^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»[^2]. Also see the slides from the ICCQ 2024 presentation (also video).
In brief, following the paper:
CoSinkable
typeclass to generalize NameBinder
s to more complex patterns.BNFC-meta
.Additionally, we implement:
withPattern
method (currently in CoSinkable
).UnifiablePattern
typeclass.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, a fork of Stephanie Weirich's benchmark suite (sweirich/lambda-n-ways).
The Haskell code is organized into two packages as follows:
free-foil
packageControl.Monad.Foil
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
class (dual to Sinkable
, for patterns that generalize NameBinder
)NameMap
which is useful for some implementations (e.g. conversion functions)Control.Monad.Foil.TH
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
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
.
Control.Monad.Free.Foil
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
Control.Monad.Free.Foil.TH
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
packageLanguage.LambdaPi.Impl.Foil
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
defines a simple interpreter for λΠ-calculus with pairs, using Template Haskell to generate a large portion of the code.
Language.LambdaPi.Impl.FreeFoil
defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach.
Language.LambdaPi.Impl.FreeFoilTH
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 implementation is not documented yet.
In Haskell:
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.ViewPatterns
in Haskell.CoSinkable
and Sinkable
instances via Template Haskell at the moment. However, a safer and more flexible derivation should be possible via GHC.Generics
.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
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.[^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. 4th International Conference on Code Quality (ICCQ), Innopolis, Russian Federation, 2024, pp. 1-16 http://doi.org/10.1109/ICCQ60895.2024.10576867 (arXiv version at https://arxiv.org/abs/2405.16384) [^3]: Nikolai Kudasov. Free Monads, Intrinsic Scoping, and Higher-Order Preunification. To appear in TFP 2024. https://arxiv.org/abs/2204.05653