diff --git a/README.md b/README.md index e1285826..d2afb8fa 100644 --- a/README.md +++ b/README.md @@ -19,7 +19,7 @@ techniques for free generation of the foil. The details are presented in the pap In brief, following the paper: -1. We introduce [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil.html#t:CoSinkable) typeclass to generalize `NameBinder`s to more complex patterns. +1. We introduce [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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. @@ -41,33 +41,33 @@ 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.3/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 +- [`Control.Monad.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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.3/Control-Monad-Foil.html#t:CoSinkable) class (dual to [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil.html#t:Sinkable), for patterns that generalize `NameBinder`) - - a general total [`NameMap`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/Control-Monad-Foil.html#g:4) which is useful for some implementations (e.g. conversion functions) + - [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/Control-Monad-Foil.html#t:CoSinkable) class (dual to [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/Control-Monad-Foil.html#t:Sinkable), for patterns that generalize `NameBinder`) + - a general total [`NameMap`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/Control-Monad-Foil.html#g:4) which is useful for some implementations (e.g. conversion functions) - unification of binders, which is useful for efficient α-equivalence implementations -- [`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.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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 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.Foil.Relative`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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.1.0/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 +- [`Control.Monad.Free.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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. +- [`Control.Monad.Free.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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.3/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.Foil`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.1.0/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.3/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/lambda-pi-0.1.0/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.3/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/lambda-pi-0.1.0/Language-LambdaPi-Impl-FreeFoil.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.3/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. +- [`Language.LambdaPi.Impl.FreeFoilTH`](https://fizruk.github.io/free-foil/haddock/lambda-pi-0.1.0/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 @@ -83,8 +83,8 @@ In Haskell: 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`. -6. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.3/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. +5. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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`. +6. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.1.0/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. 7. 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. 8. Free foil should allow the same generic implementation of higher-order unification as free scope monads[^2]. In fact, the parametrized metavariables should be added in the same data types à la carte fashion. diff --git a/haskell/free-foil/ChangeLog.md b/haskell/free-foil/ChangeLog.md index f9088750..dad669b9 100644 --- a/haskell/free-foil/ChangeLog.md +++ b/haskell/free-foil/ChangeLog.md @@ -1,5 +1,33 @@ # CHANGELOG for `free-foil` +# 0.1.0 — 2024-08-18 + +- Generalize functions for binders, support general patterns (see [#16](https://github.com/fizruk/free-foil/pull/16)) + + - Add `withPattern` method to `CoSinkable`. It can be seen as a CPS-style traversal over binders in a pattern. + Our Template Haskell support covers generation of `withPattern`, + so normally the user does not have to think about it. + + - Generalize many functions to work with arbitrary patterns, not just `NameBinder`: + + - `withFreshPattern` — to + - `withRefreshedPattern` and `withRefreshedPattern'` + - `extendScopePattern` — extend a given scope with all binders in a given pattern + - `namesOfPattern` — collect all names from a pattern + - `unsinkNamePattern` — try to unsink names from a scope extended with binders from a given pattern + - `assertDistinctPattern` — establish that extended scope is distinct (if outer scope is) + - `assertDistinctExt` — establish that extended scope is distinct and indeed an extension + + - Implement unification for patterns in `unifyPatterns`. + This turns out to be one of the most difficult places, especially for compound patterns. + Implementing patterns properly on the user side not comfortable at all! + Luckily, we provide useful helpers like `andThenUnifyPatterns` and `andThenUnifyNameBinders`, + as well as Template Haskell support to derive `UnifiablePattern`. + + - Generalize Free Foil to support arbitrary patterns. + + - The `Foil` and `FreeFoilTH` implementations now make use of the generalized pattern support. + # 0.0.3 — 2024-06-20 - Add α-equivalence checks and α-normalization (see [#12](https://github.com/fizruk/free-foil/pull/12)): diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal index db82916b..361cbb94 100644 --- a/haskell/free-foil/free-foil.cabal +++ b/haskell/free-foil/free-foil.cabal @@ -5,7 +5,7 @@ cabal-version: 1.12 -- see: https://github.com/sol/hpack name: free-foil -version: 0.0.3 +version: 0.1.0 synopsis: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description: Please see the README on GitHub at category: Parsing diff --git a/haskell/free-foil/package.yaml b/haskell/free-foil/package.yaml index b29155fc..46ae648b 100644 --- a/haskell/free-foil/package.yaml +++ b/haskell/free-foil/package.yaml @@ -1,5 +1,5 @@ name: free-foil -version: 0.0.3 +version: 0.1.0 github: "fizruk/free-foil" license: BSD3 author: "Nikolai Kudasov" diff --git a/haskell/lambda-pi/lambda-pi.cabal b/haskell/lambda-pi/lambda-pi.cabal index 5aa9d9c0..473e2fc0 100644 --- a/haskell/lambda-pi/lambda-pi.cabal +++ b/haskell/lambda-pi/lambda-pi.cabal @@ -5,7 +5,7 @@ cabal-version: 1.24 -- see: https://github.com/sol/hpack name: lambda-pi -version: 0.0.3 +version: 0.1.0 synopsis: λΠ-calculus implemented in a few different ways. description: Please see the README on GitHub at category: Language @@ -60,7 +60,7 @@ library , bifunctors , containers , deepseq - , free-foil >=0.0.3 + , free-foil >=0.1.0 , template-haskell , text >=1.2.3.1 default-language: Haskell2010 @@ -83,7 +83,7 @@ executable lambda-pi , bifunctors , containers , deepseq - , free-foil >=0.0.3 + , free-foil >=0.1.0 , lambda-pi , template-haskell , text >=1.2.3.1 @@ -108,7 +108,7 @@ test-suite doctests , containers , deepseq , doctest-parallel - , free-foil >=0.0.3 + , free-foil >=0.1.0 , lambda-pi , template-haskell , text >=1.2.3.1 @@ -136,7 +136,7 @@ test-suite spec , bifunctors , containers , deepseq - , free-foil >=0.0.3 + , free-foil >=0.1.0 , hspec , hspec-discover , lambda-pi diff --git a/haskell/lambda-pi/package.yaml b/haskell/lambda-pi/package.yaml index 1b4be8b2..59b4741e 100644 --- a/haskell/lambda-pi/package.yaml +++ b/haskell/lambda-pi/package.yaml @@ -1,5 +1,5 @@ name: lambda-pi -version: 0.0.3 +version: 0.1.0 github: "fizruk/free-foil" license: BSD3 author: "Nikolai Kudasov" @@ -39,7 +39,7 @@ dependencies: bifunctors: template-haskell: deepseq: - free-foil: ">= 0.0.3" + free-foil: ">= 0.1.0" ghc-options: - -Wall