Merge branch 'release-v0.1.0'

* release-v0.1.0:
  Bump version and update changelog

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.

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)):

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 <https://github.com/fizruk/free-foil#readme>
 category:       Parsing

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"

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 <https://github.com/fizruk/free-foil#readme>
 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

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