Merge pull request #12 from fizruk/alpha-equiv

Add alpha equivalence

README.md

@@ -17,7 +17,7 @@ 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`](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.
+1. We introduce [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.
 
@@ -30,19 +30,26 @@ See [KarinaTyulebaeva/lambda-n-ways](https://github.com/KarinaTyulebaeva/lambda-
 
 The Haskell 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`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.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.
+  - [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:CoSinkable) class (dual to [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.2/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.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.Foil.TH`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.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.
+- [`Control.Monad.Foil.Relative`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.2/Control-Monad-Foil-Internal.html#t:Name).
 
-- [`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.
+- [`Control.Monad.Free.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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
 
-- [`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.
+  - generic substitution for this generic representation of syntax with binders
+  - generic α-normalization and α-equivalence checks
 
-- [`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.
+- [`Language.LambdaPi.Impl.Foil`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.2/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.2/Language-LambdaPi-Impl-FoilTH.html) defines a simple interpreter for λΠ-calculus with pairs, using the free foil approach.
 
 ### Scala
 
@@ -52,14 +59,14 @@ Scala implementation is not documented yet.
 
 In Haskell:
 
-1. We do not (yet) provide α-equivalence for scopes. That said, we do have a tested (but undocumented) implementation for the foil in the benchmarks (see [`unsafeAeq`](https://github.com/KarinaTyulebaeva/lambda-n-ways/blob/09a995f9644f6bf29db1803eef004ddd382b823d/lib/FreeScoped/Foil.hs#L336-L401)).
+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. The free foil does not (yet) support patterns, only single-variable binders. While we think it should be sufficient to parametrize [`AST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Free-Foil.html#t:AST) and [`ScopedAST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Free-Foil.html#t:ScopedAST) with a `pattern` type constructor (e.g. literally the same [`Pattern`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Language-LambdaPi-Impl-Foil.html#t:Pattern) type used in the foil examples), we did not check if everything generalizes well enough.
-4. Template Haskell generates the foil, but not (yet) free foil. We believe there should be no problems in implementing TH-generation for the free foil, achieving the best of both worlds: generating the signature bifunctor together with conversion functions while getting [`substitute`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Free-Foil.html#v:substitute) (and, potentially, other useful algorithms[^3]) for free (except, as our benchmarks show, a moderate slowdown in performance should be expected compared to the foil).
+3. The free foil does not (yet) support patterns, only single-variable binders. While we think it should be sufficient to parametrize [`AST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:AST) and [`ScopedAST`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#t:ScopedAST) with a `pattern` type constructor (e.g. literally the same [`Pattern`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Language-LambdaPi-Impl-Foil.html#t:Pattern) type used in the foil examples), we did not check if everything generalizes well enough.
+4. Template Haskell generates the foil, but not (yet) free foil. We believe there should be no problems in implementing TH-generation for the free foil, achieving the best of both worlds: generating the signature bifunctor together with conversion functions while getting [`substitute`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Free-Foil.html#v:substitute) (and, potentially, other useful algorithms[^3]) for free (except, as our benchmarks show, a moderate slowdown in performance should be expected compared to the foil).
 5. We do not (yet) provide strict versions of the foil and free foil here. The benchmarks, however, do implement these variations.
 6. We do not (yet) generate pattern synonyms for the foil with Template Haskell, however, this can be done easily, similarly to [this implementation](https://github.com/rzk-lang/rzk/blob/013b4126adeefe69dc757e38e18cd17a79b5a0fc/rzk/src/Free/Scoped/TH.hs) for free scoped monad.
-7. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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`.
-8. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.1/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. We derive [`CoSinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/Control-Monad-Foil.html#t:CoSinkable) and [`Sinkable`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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`.
+8. Many functions, including [`rbind`](https://fizruk.github.io/free-foil/haddock/free-foil-0.0.2/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.
 9. 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.
 
 [^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>

haskell/free-foil/free-foil.cabal

@@ -19,6 +19,7 @@ license-file:   LICENSE
 build-type:     Simple
 extra-source-files:
     README.md
+    ChangeLog.md
     LICENSE
 
 source-repository head

haskell/free-foil/src/Control/Monad/Foil.hs

@@ -28,18 +28,24 @@ module Control.Monad.Foil (
   withFresh,
   withRefreshed,
   unsinkName,
-  -- * Safe (co)sinking
+  -- * Safe (co)sinking and renaming
   Sinkable(..),
   CoSinkable(..),
   sink,
   extendRenaming,
+  extendNameBinderRenaming,
+  composeNameBinderRenamings,
+  fromNameBinderRenaming,
   extendRenamingNameBinder,
   -- * Safe substitutions
   Substitution,
   lookupSubst,
   identitySubst,
   addSubst,
   addRename,
+  -- * Unification of binders
+  UnifyNameBinders(..),
+  unifyNameBinders,
   -- * Name maps
   NameMap,
   emptyNameMap,
@@ -51,6 +57,7 @@ module Control.Monad.Foil (
   Distinct,
   DistinctEvidence(..),
   assertDistinct,
+  assertExt,
   DExt,
   InjectName(..),
 ) where

haskell/free-foil/src/Control/Monad/Foil/Internal.hs

@@ -40,6 +40,7 @@ import           Data.IntSet
 import qualified Data.IntSet     as IntSet
 import           Data.Kind       (Type)
 import           Unsafe.Coerce
+import Data.Coerce (coerce)
 
 -- * Safe types and operations
 
@@ -134,6 +135,10 @@ unsafeAssertFresh binder cont =
 assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l
 assertDistinct _ = unsafeDistinct
 
+-- | A distinct scope extended with a 'NameBinder' is also distinct.
+assertExt :: NameBinder n l -> ExtEvidence n l
+assertExt _ = unsafeExt
+
 -- | Safely rename (if necessary) a given name to extend a given scope.
 -- This is similar to 'withFresh', except if the name does not clash with
 -- the scope, it can be used immediately, without renaming.
@@ -155,6 +160,37 @@ unsinkName binder name@(UnsafeName raw)
   | nameOf binder == name = Nothing
   | otherwise = Just (UnsafeName raw)
 
+-- * Unification of binders
+
+-- | Unification result for two binders,
+-- extending some common scope to scopes @l@ and @r@ respectively.
+--
+-- Due to the implementation of the foil,
+data UnifyNameBinders n l r where
+  -- | Binders are the same, proving that type parameters @l@ and @r@
+  -- are in fact equivalent.
+  SameNameBinders :: UnifyNameBinders n l l
+  -- | It is possible to safely rename the left binder
+  -- to match the right one.
+  RenameLeftNameBinder :: (NameBinder n l -> NameBinder n r) -> UnifyNameBinders n l r
+  -- | It is possible to safely rename the right binder
+  -- to match the left one.
+  RenameRightNameBinder :: (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r
+
+-- | Unify binders either by asserting that they are the same,
+-- or by providing a /safe/ renaming function to convert one binder to another.
+unifyNameBinders
+  :: forall i l r.
+     NameBinder i l
+  -> NameBinder i r
+  -> UnifyNameBinders i l r
+unifyNameBinders (UnsafeNameBinder (UnsafeName i1)) (UnsafeNameBinder (UnsafeName i2))
+  | i1 == i2  = unsafeCoerce (SameNameBinders @l)  -- equal names extend scopes equally
+  | i1 < i2   = RenameRightNameBinder $ \(UnsafeNameBinder (UnsafeName i'')) ->
+      if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')
+  | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->
+      if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')
+
 -- * Safe sinking
 
 -- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,
@@ -196,6 +232,31 @@ extendRenaming
 extendRenaming _ pattern cont =
   cont unsafeCoerce (unsafeCoerce pattern)
 
+-- | Extend renaming of binders when going under a 'CoSinkable' pattern (generalized binder).
+-- Note that the scope under pattern is independent of the codomain of the renaming.
+extendNameBinderRenaming
+  :: CoSinkable pattern
+  => (NameBinder i n -> NameBinder i n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
+  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.
+  -> (forall l'. (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r )
+  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
+  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
+  -> r
+extendNameBinderRenaming _ pattern cont =
+  cont unsafeCoerce (unsafeCoerce pattern)
+
+-- | Safely compose renamings of name binders.
+-- The underlying implementation is
+composeNameBinderRenamings
+  :: (NameBinder n i -> NameBinder n i')    -- ^ Rename binders extending scope @n@ from @i@ to @i'@.
+  -> (NameBinder i' l -> NameBinder i' l')  -- ^ Rename binders extending scope @i'@ from @l@ to @l'@.
+  -> (NameBinder n l -> NameBinder n l')
+composeNameBinderRenamings = unsafeCoerce (flip (.))
+
+-- | Convert renaming of name binders into renaming of names in the inner scopes.
+fromNameBinderRenaming :: (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
+fromNameBinderRenaming = coerce
+
 -- | Extend renaming when going under a 'NameBinder'.
 -- Note that the scope under binder is independent of the codomain of the renaming.
 --

haskell/free-foil/src/Control/Monad/Foil/Relative.hs

@@ -21,3 +21,7 @@ class RelMonad (f :: S -> Type) (m :: S -> Type) where
   -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,
   -- preserving the more general type signature for 'rbind'.
   rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b
+
+-- | Relative version of 'liftM' (an 'fmap' restricted to 'Monad').
+liftRM :: (RelMonad f m, Distinct b) => Scope b -> (f a -> f b) -> m a -> m b
+liftRM scope f m = rbind scope m (rreturn . f)