diff --git a/README.md b/README.md index f447c922..cd475b41 100644 --- a/README.md +++ b/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. diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal index 8777ab77..df726bef 100644 --- a/haskell/free-foil/free-foil.cabal +++ b/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 diff --git a/haskell/free-foil/src/Control/Monad/Foil.hs b/haskell/free-foil/src/Control/Monad/Foil.hs index e53593cd..4288d015 100644 --- a/haskell/free-foil/src/Control/Monad/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Foil.hs @@ -28,11 +28,14 @@ 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, @@ -40,6 +43,9 @@ module Control.Monad.Foil ( 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 diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs index f0961948..420bc51e 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs +++ b/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. -- diff --git a/haskell/free-foil/src/Control/Monad/Foil/Relative.hs b/haskell/free-foil/src/Control/Monad/Foil/Relative.hs index 93a0119e..33c564e9 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Relative.hs +++ b/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) diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs index 40789965..8754339c 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs @@ -8,6 +8,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} -- | This module defines a variation of @@ -20,7 +21,11 @@ module Control.Monad.Free.Foil where import Control.DeepSeq import qualified Control.Monad.Foil.Internal as Foil import qualified Control.Monad.Foil.Relative as Foil +import Data.Bifoldable +import Data.Bifunctor.Sum import Data.Bifunctor +import Data.Coerce (coerce) +import Data.Monoid (All (..)) import GHC.Generics (Generic) -- | Scoped term under a (single) name binder. @@ -53,6 +58,8 @@ instance Bifunctor sig => Foil.Sinkable (AST sig) where instance Foil.InjectName (AST sig) where injectName = Var +-- * Substitution + -- | Substitution for free (scoped monads). substitute :: (Bifunctor sig, Foil.Distinct o) @@ -71,6 +78,31 @@ substitute scope subst = \case body' = substitute scope' subst' body in ScopedAST binder' body' +-- | Substitution for free (scoped monads). +-- +-- This is a version of 'substitute' that forces refreshing of all name binders, +-- resulting in a term with normalized binders: +-- +-- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst +-- +-- In general, 'substitute' is more efficient since it does not always refresh binders. +substituteRefreshed + :: (Bifunctor sig, Foil.Distinct o) + => Foil.Scope o + -> Foil.Substitution (AST sig) i o + -> AST sig i + -> AST sig o +substituteRefreshed scope subst = \case + Var name -> Foil.lookupSubst subst name + Node node -> Node (bimap f (substituteRefreshed scope subst) node) + where + f (ScopedAST binder body) = + Foil.withFresh scope $ \binder' -> + let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder') + scope' = Foil.extendScope binder' scope + body' = substituteRefreshed scope' subst' body + in ScopedAST binder' body' + -- | @'AST' sig@ is a monad relative to 'Foil.Name'. instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where rreturn = Var @@ -87,3 +119,130 @@ instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where Nothing -> Foil.rreturn (Foil.nameOf binder') Just n -> Foil.sink (subst n) in ScopedAST binder' (Foil.rbind scope' body subst') + +-- * \(\alpha\)-equivalence + +-- | Refresh (force) all binders in a term, minimizing the used indices. +refreshAST + :: (Bifunctor sig, Foil.Distinct n) + => Foil.Scope n + -> AST sig n + -> AST sig n +refreshAST scope = \case + t@Var{} -> t + Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t) + +-- | Similar to `refreshAST`, but for scoped terms. +refreshScopedAST :: (Bifunctor sig, Foil.Distinct n) + => Foil.Scope n + -> ScopedAST sig n + -> ScopedAST sig n +refreshScopedAST scope (ScopedAST binder body) = + Foil.withFresh scope $ \binder' -> + let scope' = Foil.extendScope binder' scope + subst = Foil.addRename (Foil.sink Foil.identitySubst) binder (Foil.nameOf binder') + in ScopedAST binder' (substituteRefreshed scope' subst body) + +-- | \(\alpha\)-equivalence check for two terms in one scope +-- via normalization of bound identifiers (via 'refreshAST'). +-- +-- Compared to 'alphaEquiv', this function may perform some unnecessary +-- changes of bound variables when the binders are the same on both sides. +alphaEquivRefreshed + :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n) + => Foil.Scope n + -> AST sig n + -> AST sig n + -> Bool +alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2 + +-- | \(\alpha\)-equivalence check for two terms in one scope +-- via unification of bound variables (via 'unifyNameBinders'). +-- +-- Compared to 'alphaEquivRefreshed', this function might skip unnecessary +-- changes of bound variables when both binders in two matching scoped terms coincide. +alphaEquiv + :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n) + => Foil.Scope n + -> AST sig n + -> AST sig n + -> Bool +alphaEquiv _scope (Var x) (Var y) = x == coerce y +alphaEquiv scope (Node l) (Node r) = + case zipMatch l r of + Nothing -> False + Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt) +alphaEquiv _ _ _ = False + +-- | Same as 'alphaEquiv' but for scoped terms. +alphaEquivScoped + :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n) + => Foil.Scope n + -> ScopedAST sig n + -> ScopedAST sig n + -> Bool +alphaEquivScoped scope + (ScopedAST binder1 body1) + (ScopedAST binder2 body2) = + case Foil.unifyNameBinders binder1 binder2 of + -- if binders are the same, then we can safely compare bodies + Foil.SameNameBinders -> -- after seeing this we know that body scopes are the same + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope1 = Foil.extendScope binder1 scope + in alphaEquiv scope1 body1 body2 + -- if we can safely rename first binder into second + Foil.RenameLeftNameBinder rename1to2 -> + case Foil.assertDistinct binder2 of + Foil.Distinct -> + let scope2 = Foil.extendScope binder2 scope + in alphaEquiv scope2 (Foil.liftRM scope2 (Foil.fromNameBinderRenaming rename1to2) body1) body2 + -- if we can safely rename second binder into first + Foil.RenameRightNameBinder rename2to1 -> + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope1 = Foil.extendScope binder1 scope + in alphaEquiv scope1 body1 (Foil.liftRM scope1 (Foil.fromNameBinderRenaming rename2to1) body2) + +-- ** Unsafe equality checks + +-- | /Unsafe/ equality check for two terms. +-- This check ignores the possibility that two terms might have different +-- scope extensions under binders (which might happen due to substitution +-- under a binder in absence of name conflicts). +unsafeEqAST + :: (Bifoldable sig, ZipMatch sig) + => AST sig n + -> AST sig l + -> Bool +unsafeEqAST (Var x) (Var y) = x == coerce y +unsafeEqAST (Node t1) (Node t2) = + case zipMatch t1 t2 of + Nothing -> False + Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt) +unsafeEqAST _ _ = False + +-- | A version of 'unsafeEqAST' for scoped terms. +unsafeEqScopedAST + :: (Bifoldable sig, ZipMatch sig) + => ScopedAST sig n + -> ScopedAST sig l + -> Bool +unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and + [ binder1 == coerce binder2 + , body1 `unsafeEqAST` body2 + ] + +-- ** Syntactic matching (unification) + +-- | Perform one-level matching for the two (non-variable) terms. +class ZipMatch sig where + zipMatch + :: sig scope term -- ^ Left non-variable term. + -> sig scope' term' -- ^ Right non-variable term. + -> Maybe (sig (scope, scope') (term, term')) + +instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where + zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f' + zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g' + zipMatch _ _ = Nothing diff --git a/haskell/lambda-pi/lambda-pi.cabal b/haskell/lambda-pi/lambda-pi.cabal index 390fb467..73f362a5 100644 --- a/haskell/lambda-pi/lambda-pi.cabal +++ b/haskell/lambda-pi/lambda-pi.cabal @@ -117,6 +117,8 @@ test-suite spec type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: + Language.LambdaPi.Impl.FoilSpec + Language.LambdaPi.Impl.FreeFoilSpec Paths_lambda_pi hs-source-dirs: test @@ -127,13 +129,17 @@ test-suite spec build-tool-depends: BNFC:bnfc >=2.9.4.1 build-depends: - array >=0.5.3.0 + QuickCheck + , array >=0.5.3.0 , base >=4.7 && <5 , bifunctors , containers , deepseq , free-foil >=0.0.2 + , hspec + , hspec-discover , lambda-pi + , mtl , template-haskell , text >=1.2.3.1 default-language: Haskell2010 diff --git a/haskell/lambda-pi/package.yaml b/haskell/lambda-pi/package.yaml index e5b0a828..2bf9b107 100644 --- a/haskell/lambda-pi/package.yaml +++ b/haskell/lambda-pi/package.yaml @@ -83,6 +83,10 @@ tests: - -with-rtsopts=-N dependencies: - lambda-pi + - QuickCheck + - hspec + - hspec-discover + - mtl doctests: source-dirs: diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs index e68b58b8..2ff23239 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs @@ -9,6 +9,7 @@ {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE UndecidableInstances #-} -- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs). -- @@ -17,7 +18,7 @@ -- 1. Scope-safe AST for \(\lambda\Pi\)-terms. -- 2. Correct capture-avoiding substitution (see 'substitute'). -- 3. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm' and 'fromFoilTerm'. --- 4. Helper functions for patterns. See 'extendScopeFoilPattern' and 'withRefreshedFoilPattern'. +-- 4. Helper functions for patterns. See 'extendScopePattern' and 'withRefreshedPattern'. -- 5. Computation of weak head normal form (WHNF) and normal form (NF), see 'whnf' and 'nf'. -- 6. Entry point, gluing everything together. See 'defaultMain'. -- @@ -31,15 +32,25 @@ module Language.LambdaPi.Impl.Foil where import Control.Monad.Foil +import Control.Monad (join) +import Control.Monad.Foil.Relative +import Data.Coerce (coerce) import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe (fromMaybe) +import Data.String import qualified Language.LambdaPi.Syntax.Abs as Raw import Language.LambdaPi.Syntax.Layout (resolveLayout) import Language.LambdaPi.Syntax.Lex (tokens) -import Language.LambdaPi.Syntax.Par (pProgram) +import Language.LambdaPi.Syntax.Par (pProgram, pTerm) import Language.LambdaPi.Syntax.Print (printTree) import System.Exit (exitFailure) +-- $setup +-- >>> :set -XOverloadedStrings +-- >>> :set -XDataKinds +-- >>> import Control.Monad.Foil + -- | Type of scope-safe \(\lambda\Pi\)-terms with pairs. data Expr n where -- | Variables: \(x\) @@ -65,7 +76,13 @@ data Expr n where UniverseE :: Expr n instance Show (Expr VoidS) where - show = ppExpr + show = printTree . fromFoilTerm' + +instance IsString (Expr VoidS) where + fromString input = + case pTerm (tokens input) of + Left err -> error ("could not parse λΠ-term: " <> input <> "\n " <> err) + Right term -> toFoilTermClosed term -- | Patterns. data Pattern n l where @@ -92,6 +109,40 @@ instance CoSinkable Pattern where instance InjectName Expr where injectName = VarE +-- | Check if a name in the extended context +-- is introduced in a pattern or comes from the outer scope @n@. +-- +-- This is a generalization of 'unsinkName' to 'Pattern'. +unsinkNamePattern + :: Pattern n l -> Name l -> Maybe (Name n) +unsinkNamePattern pattern name = + case pattern of + PatternWildcard -> Just (coerce name) + PatternVar binder -> unsinkName binder name + PatternPair l r -> unsinkNamePattern r name >>= unsinkNamePattern l + +instance RelMonad Name Expr where + rreturn = VarE + rbind scope e subst = case e of + VarE name -> subst name + AppE f x -> AppE (rbind scope f subst) (rbind scope x subst) + LamE pattern body -> withRefreshedPattern' scope pattern $ \extendSubst pattern' -> + let subst' = extendSubst subst + scope' = extendScopePattern pattern' scope + body' = rbind scope' body subst' + in LamE pattern' body' + PiE pattern a b -> withRefreshedPattern' scope pattern $ \extendSubst pattern' -> + let subst' = extendSubst subst + scope' = extendScopePattern pattern' scope + a' = rbind scope a subst + b' = rbind scope' b subst' + in PiE pattern' a' b' + PairE l r -> PairE (rbind scope l subst) (rbind scope r subst) + FirstE t -> FirstE (rbind scope t subst) + SecondE t -> SecondE (rbind scope t subst) + ProductE l r -> ProductE (rbind scope l subst) (rbind scope r subst) + UniverseE -> UniverseE + -- | Default way to print a name using its internal 'Id'. ppName :: Name n -> String ppName name = "x" <> show (nameId name) @@ -141,6 +192,32 @@ instance Sinkable Expr where sinkabilityProof rename (ProductE l r) = ProductE (sinkabilityProof rename l) (sinkabilityProof rename r) sinkabilityProof _ UniverseE = UniverseE +assertExtPattern :: Pattern n l -> ExtEvidence n l +assertExtPattern = \case + PatternWildcard -> Ext + PatternVar x -> assertExt x + PatternPair l r -> + case assertExtPattern l of + Ext -> case assertExtPattern r of + Ext -> Ext + +assertDistinctPattern :: Distinct n => Pattern n l -> DistinctEvidence l +assertDistinctPattern = \case + PatternWildcard -> Distinct + PatternVar x -> assertDistinct x + PatternPair l r -> + case assertDistinctPattern l of + Distinct -> case assertDistinctPattern r of + Distinct -> Distinct + +namesOfPattern :: Distinct n => Pattern n l -> [Name l] +namesOfPattern PatternWildcard = [] +namesOfPattern (PatternVar x) = [nameOf x] +namesOfPattern (PatternPair l r) = + case (assertExtPattern l, assertDistinctPattern l) of + (Ext, Distinct) -> case (assertExtPattern r, assertDistinctPattern r) of + (Ext, Distinct) -> map sink (namesOfPattern l) ++ namesOfPattern r + -- | Extend scope with variables inside a pattern. -- This is a more flexible version of 'extendScope'. extendScopePattern :: Pattern n l -> Scope n -> Scope l @@ -149,6 +226,23 @@ extendScopePattern = \case PatternVar binder -> extendScope binder PatternPair l r -> extendScopePattern r . extendScopePattern l +-- | Refresh (if needed) bound variables introduced in a pattern. +-- This is a more flexible version of 'withRefreshed'. +withFreshPattern + :: (Distinct o, InjectName e, Sinkable e) + => Scope o + -> Pattern n l + -> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> Pattern o o' -> r) -> r +withFreshPattern scope pattern cont = + case pattern of + PatternWildcard -> cont sink PatternWildcard + PatternVar x -> withFresh scope $ \x' -> + cont (\subst -> addRename (sink subst) x (nameOf x')) (PatternVar x') + PatternPair l r -> withFreshPattern scope l $ \lsubst l' -> + let scope' = extendScopePattern l' scope + in withFreshPattern scope' r $ \rsubst r' -> + cont (rsubst . lsubst) (PatternPair l' r') + -- | Refresh (if needed) bound variables introduced in a pattern. -- This is a more flexible version of 'withRefreshed'. withRefreshedPattern @@ -166,6 +260,27 @@ withRefreshedPattern scope pattern cont = in withRefreshedPattern scope' r $ \rsubst r' -> cont (rsubst . lsubst) (PatternPair l' r') +-- | Refresh (if needed) bound variables introduced in a pattern. +-- +-- This is a version of 'withRefreshedPattern' that uses functional renamings instead of 'Substitution'. +withRefreshedPattern' + :: (Distinct o, InjectName e, Sinkable e) + => Scope o + -> Pattern n l + -> (forall o'. DExt o o' => ((Name n -> e o) -> Name l -> e o') -> Pattern o o' -> r) -> r +withRefreshedPattern' scope pattern cont = + case pattern of + PatternWildcard -> cont id PatternWildcard + PatternVar x -> withRefreshed scope (nameOf x) $ \x' -> + let k subst name = case unsinkName x name of + Nothing -> injectName (nameOf x') + Just name' -> sink (subst name') + in cont k (PatternVar x') + PatternPair l r -> withRefreshedPattern' scope l $ \lsubst l' -> + let scope' = extendScopePattern l' scope + in withRefreshedPattern' scope' r $ \rsubst r' -> + cont (rsubst . lsubst) (PatternPair l' r') + -- | Perform substitution in a \(\lambda\Pi\)-term. substitute :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o substitute scope subst = \case @@ -188,6 +303,29 @@ substitute scope subst = \case ProductE l r -> ProductE (substitute scope subst l) (substitute scope subst r) UniverseE -> UniverseE +-- | Perform substitution in a \(\lambda\Pi\)-term +-- and normalize binders in the process. +substituteRefresh :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o +substituteRefresh scope subst = \case + VarE name -> lookupSubst subst name + AppE f x -> AppE (substituteRefresh scope subst f) (substituteRefresh scope subst x) + LamE pattern body -> withFreshPattern scope pattern $ \extendSubst pattern' -> + let subst' = extendSubst subst + scope' = extendScopePattern pattern' scope + body' = substituteRefresh scope' subst' body + in LamE pattern' body' + PiE pattern a b -> withFreshPattern scope pattern $ \extendSubst pattern' -> + let subst' = extendSubst subst + scope' = extendScopePattern pattern' scope + a' = substituteRefresh scope subst a + b' = substituteRefresh scope' subst' b + in PiE pattern' a' b' + PairE l r -> PairE (substituteRefresh scope subst l) (substituteRefresh scope subst r) + FirstE t -> FirstE (substituteRefresh scope subst t) + SecondE t -> SecondE (substituteRefresh scope subst t) + ProductE l r -> ProductE (substituteRefresh scope subst l) (substituteRefresh scope subst r) + UniverseE -> UniverseE + -- | Convert a raw pattern into a scope-safe one. toFoilPattern :: Distinct n @@ -260,6 +398,44 @@ fromFoilTermClosed -> Raw.Term fromFoilTermClosed freshVars = fromFoilTerm freshVars emptyNameMap +-- | Convert a scope-safe pattern into a raw pattern converting raw +-- identifiers directly into 'Raw.VarIdent' +fromFoilPattern' + :: Pattern n l -- ^ A scope-safe pattern that extends scope @n@ into scope @l@. + -> Raw.Pattern +fromFoilPattern' pattern = + case pattern of + PatternWildcard -> Raw.PatternWildcard loc + PatternVar z -> Raw.PatternVar loc (binderToVarIdent z) + PatternPair l r -> + let l' = fromFoilPattern' l + r' = fromFoilPattern' r + in Raw.PatternPair loc l' r' + where + loc = error "location information is lost when converting from AST" + binderToVarIdent binder = Raw.VarIdent ("x" ++ show (nameId (nameOf binder))) + +-- | Convert a scope-safe term into a raw term converting raw +-- identifiers directly into 'Raw.VarIdent'. +fromFoilTerm' + :: Expr n -- ^ A scope safe term in scope @n@. + -> Raw.Term +fromFoilTerm' = \case + VarE name -> Raw.Var loc (nameToVarIdent name) + AppE t1 t2 -> Raw.App loc (fromFoilTerm' t1) (fromFoilTerm' t2) + LamE pattern body -> + Raw.Lam loc (fromFoilPattern' pattern) (Raw.AScopedTerm loc (fromFoilTerm' body)) + PiE pattern a b -> + Raw.Pi loc (fromFoilPattern' pattern) (fromFoilTerm' a) (Raw.AScopedTerm loc (fromFoilTerm' b)) + PairE t1 t2 -> Raw.Pair loc (fromFoilTerm' t1) (fromFoilTerm' t2) + FirstE t -> Raw.First loc (fromFoilTerm' t) + SecondE t -> Raw.Second loc (fromFoilTerm' t) + ProductE t1 t2 -> Raw.Product loc (fromFoilTerm' t1) (fromFoilTerm' t2) + UniverseE -> Raw.Universe loc + where + loc = error "location information is lost when converting from AST" + nameToVarIdent name = Raw.VarIdent ("x" ++ show (nameId name)) + -- | Convert a raw term into a scope-safe \(\lambda\Pi\)-term. toFoilTerm :: Distinct n @@ -298,6 +474,10 @@ toFoilTerm scope env = \case Raw.Universe _loc -> UniverseE +-- | Convert a raw term into a closed scope-safe term. +toFoilTermClosed :: Raw.Term -> Expr VoidS +toFoilTermClosed = toFoilTerm emptyScope Map.empty + -- | Match a pattern against an expression. matchPattern :: Pattern n l -> Expr n -> Substitution Expr l n matchPattern pattern expr = go pattern expr identitySubst @@ -308,6 +488,34 @@ matchPattern pattern expr = go pattern expr identitySubst go (PatternPair l r) e = go r (SecondE e) . go l (FirstE e) -- | Compute weak head normal form (WHNF). +-- +-- >>> whnf emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)" +-- λ x0 . λ x1 . x1 +-- +-- >>> whnf emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))" +-- λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1) +-- +-- Note that during computation bound variables can become unordered +-- in the sense that binders may easily repeat or decrease. For example, +-- in the following expression, inner binder has lower index that the outer one: +-- +-- >>> whnf emptyScope "(λx.λy.x)(λx.x)" +-- λ x1 . λ x0 . x0 +-- +-- At the same time, without substitution, we get regular, increasing binder indices: +-- +-- >>> "λx.λy.y" :: Expr VoidS +-- λ x0 . λ x1 . x1 +-- +-- To compare terms for \(\alpha\)-equivalence, we may use 'alphaEquiv': +-- +-- >>> alphaEquiv emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y" +-- True +-- +-- We may also normalize binders using 'refreshExpr': +-- +-- >>> refreshExpr emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)") +-- λ x0 . λ x1 . x1 whnf :: Distinct n => Scope n -> Expr n -> Expr n whnf scope = \case AppE f arg -> @@ -326,6 +534,92 @@ whnf scope = \case t' -> SecondE t' t -> t +-- | Normalize all binder identifiers in an expression. +refreshExpr :: Distinct n => Scope n -> Expr n -> Expr n +refreshExpr scope = substituteRefresh scope identitySubst + +-- | \(\alpha\)-equivalence check for two terms in one scope +-- via normalization of bound identifiers (via 'refreshExpr'). +-- +-- This function may perform some unnecessary +-- changes of bound variables when the binders are the same on both sides. +alphaEquivRefreshed :: Distinct n => Scope n -> Expr n -> Expr n -> Bool +alphaEquivRefreshed scope e1 e2 = + refreshExpr scope e1 `unsafeEqExpr` refreshExpr scope e2 + +-- | Unsafely check for equality of two 'Pattern's. +-- +-- This __does not__ include \(\alpha\)-equivalence! +unsafeEqPattern :: Pattern n l -> Pattern n' l' -> Bool +unsafeEqPattern PatternWildcard PatternWildcard = True +unsafeEqPattern (PatternVar x) (PatternVar x') = x == coerce x' +unsafeEqPattern (PatternPair l r) (PatternPair l' r') = + unsafeEqPattern l l' && unsafeEqPattern r r' +unsafeEqPattern _ _ = False + +-- | Unsafely check for equality of two 'Expr's. +-- +-- This __does not__ include \(\alpha\)-equivalence! +unsafeEqExpr :: Expr n -> Expr l -> Bool +unsafeEqExpr e1 e2 = case (e1, e2) of + (VarE x, VarE x') -> x == coerce x' + (AppE t1 t2, AppE t1' t2') -> unsafeEqExpr t1 t1' && unsafeEqExpr t2 t2' + (LamE x body, LamE x' body') -> unsafeEqPattern x x' && unsafeEqExpr body body' + (PiE x a b, PiE x' a' b') -> unsafeEqPattern x x' && unsafeEqExpr a a' && unsafeEqExpr b b' + (PairE l r, PairE l' r') -> unsafeEqExpr l l' && unsafeEqExpr r r' + (FirstE t, FirstE t') -> unsafeEqExpr t t' + (SecondE t, SecondE t') -> unsafeEqExpr t t' + (ProductE l r, ProductE l' r') -> unsafeEqExpr l l' && unsafeEqExpr r r' + (UniverseE, UniverseE) -> True + _ -> False + +unifyPatterns + :: Distinct n + => Pattern n l + -> Pattern n r + -> (forall lr. DExt n lr => (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> Pattern n lr -> result) + -> Maybe result +unifyPatterns PatternWildcard PatternWildcard cont = + Just (cont id id PatternWildcard) +unifyPatterns (PatternVar x) (PatternVar x') cont = + case unifyNameBinders x x' of + SameNameBinders -> + case assertDistinct x of + Distinct -> case assertExt x of + Ext -> Just (cont id id (PatternVar x)) + RenameLeftNameBinder renameL -> + case (assertExt x', assertDistinct x') of + (Ext, Distinct) -> Just (cont renameL id (PatternVar x')) + RenameRightNameBinder renameR -> + case (assertExt x, assertDistinct x) of + (Ext, Distinct) -> Just (cont id renameR (PatternVar x)) +unifyPatterns (PatternPair l r) (PatternPair l' r') cont = join $ + unifyPatterns l l' $ \renameL renameL' l'' -> + extendNameBinderRenaming renameL r $ \renameLext rext -> + extendNameBinderRenaming renameL' r' $ \renameL'ext r'ext -> + unifyPatterns rext r'ext $ \renameR renameR' r'' -> + let rename = renameL `composeNameBinderRenamings` (renameR . renameLext) + rename' = renameL' `composeNameBinderRenamings` (renameR' . renameL'ext) + in cont rename rename' (PatternPair l'' r'') +unifyPatterns _ _ _ = Nothing + +alphaEquiv :: Distinct n => Scope n -> Expr n -> Expr n -> Bool +alphaEquiv scope e1 e2 = case (e1, e2) of + (VarE x, VarE x') -> x == coerce x' + (AppE t1 t2, AppE t1' t2') -> alphaEquiv scope t1 t1' && alphaEquiv scope t2 t2' + (LamE x body, LamE x' body') -> fromMaybe False $ unifyPatterns x x' $ \renameL renameR x'' -> + let scope' = extendScopePattern x'' scope + in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) body) (liftRM scope' (fromNameBinderRenaming renameR) body') + (PiE x a b, PiE x' a' b') -> fromMaybe False $ unifyPatterns x x' $ \renameL renameR x'' -> + let scope' = extendScopePattern x'' scope + in alphaEquiv scope a a' && alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) b) (liftRM scope' (fromNameBinderRenaming renameR) b') + (PairE l r, PairE l' r') -> alphaEquiv scope l l' && alphaEquiv scope r r' + (FirstE t, FirstE t') -> alphaEquiv scope t t' + (SecondE t, SecondE t') -> alphaEquiv scope t t' + (ProductE l r, ProductE l' r') -> alphaEquiv scope l l' && alphaEquiv scope r r' + (UniverseE, UniverseE) -> True + _ -> False + -- | Interpret a λΠ command. interpretCommand :: Raw.Command -> IO () interpretCommand (Raw.CommandCompute _loc term _type) = @@ -358,7 +652,7 @@ lam scope mkBody = withFresh scope $ \x -> -- | An identity function as a \(\lambda\)-term: -- -- >>> identity --- λx0. x0 +-- λ x0 . x0 identity :: Expr VoidS identity = lam emptyScope $ \_ nx -> VarE (nameOf nx) @@ -366,10 +660,10 @@ identity = lam emptyScope $ \_ nx -> -- | Church-encoding of a natural number \(n\). -- -- >>> churchN 0 --- λx0. λx1. x1 +-- λ x0 . λ x1 . x1 -- -- >>> churchN 3 --- λx0. λx1. x0 (x0 (x0 (x1))) +-- λ x0 . λ x1 . x0 (x0 (x0 x1)) churchN :: Int -> Expr VoidS churchN n = lam emptyScope $ \sx nx -> diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs index 89de91f7..66ae8dbf 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs @@ -1,12 +1,11 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeOperators #-} -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs). -- -- Free foil provides the following: @@ -28,6 +27,7 @@ module Language.LambdaPi.Impl.FreeFoil where import qualified Control.Monad.Foil as Foil import Control.Monad.Free.Foil import Data.Bifunctor.TH +import Data.Bifunctor.Sum import Data.Map (Map) import qualified Data.Map as Map import Data.String (IsString (..)) @@ -40,7 +40,9 @@ import System.Exit (exitFailure) -- $setup -- >>> import qualified Control.Monad.Foil as Foil +-- >>> import Control.Monad.Free.Foil -- >>> :set -XOverloadedStrings +-- >>> :set -XDataKinds -- | The signature 'Bifunctor' for the \(\lambda\Pi\). data LambdaPiF scope term @@ -48,8 +50,17 @@ data LambdaPiF scope term | LamF scope -- ^ Abstraction: \(\lambda x. t\) | PiF term scope -- ^ Dependent function type: \(\prod_{x : T_1} T_2\) | UniverseF -- ^ Universe (type of types): \(\mathcal{U}\) - deriving (Eq, Show, Functor) + deriving (Eq, Show, Functor, Foldable, Traversable) deriveBifunctor ''LambdaPiF +deriveBifoldable ''LambdaPiF +deriveBitraversable ''LambdaPiF + +instance ZipMatch LambdaPiF where + zipMatch (AppF l r) (AppF l' r') = Just (AppF (l, l') (r, r')) + zipMatch (LamF t) (LamF t') = Just (LamF (t, t')) + zipMatch (PiF l r) (PiF l' r') = Just (PiF (l, l') (r, r')) + zipMatch UniverseF UniverseF = Just UniverseF + zipMatch _ _ = Nothing -- | The signature 'Bifunctor' for pairs. data PairF scope term @@ -57,42 +68,47 @@ data PairF scope term | FirstF term -- ^ First projection: \(\pi_1(t)\) | SecondF term -- ^ Second projection: \(\pi_2(t)\) | ProductF term term -- ^ Product type (non-dependent): \(T_1 \times T_2\) - deriving (Eq, Show, Functor) + deriving (Eq, Show, Functor, Foldable, Traversable) deriveBifunctor ''PairF +deriveBifoldable ''PairF +deriveBitraversable ''PairF + +instance ZipMatch PairF where + zipMatch (PairF l r) (PairF l' r') = Just (PairF (l, l') (r, r')) + zipMatch (FirstF t) (FirstF t') = Just (FirstF (t, t')) + zipMatch (SecondF t) (SecondF t') = Just (SecondF (t, t')) + zipMatch (ProductF l r) (ProductF l' r') = Just (ProductF (l, l') (r, r')) + zipMatch _ _ = Nothing -- | Sum of signature bifunctors. -data (f :+: g) scope term - = InL (f scope term) - | InR (g scope term) - deriving (Eq, Show, Functor) -deriveBifunctor ''(:+:) +type (:+:) = Sum -- | \(\lambda\Pi\)-terms in scope @n@, freely generated from the sum of signatures 'LambdaPiF' and 'PairF'. type LambdaPi n = AST (LambdaPiF :+: PairF) n pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n -pattern App fun arg = Node (InL (AppF fun arg)) +pattern App fun arg = Node (L2 (AppF fun arg)) pattern Lam :: Foil.NameBinder n l -> LambdaPi l -> LambdaPi n -pattern Lam binder body = Node (InL (LamF (ScopedAST binder body))) +pattern Lam binder body = Node (L2 (LamF (ScopedAST binder body))) pattern Pi :: Foil.NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n -pattern Pi binder a b = Node (InL (PiF a (ScopedAST binder b))) +pattern Pi binder a b = Node (L2 (PiF a (ScopedAST binder b))) pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n -pattern Pair l r = Node (InR (PairF l r)) +pattern Pair l r = Node (R2 (PairF l r)) pattern First :: LambdaPi n -> LambdaPi n -pattern First t = Node (InR (FirstF t)) +pattern First t = Node (R2 (FirstF t)) pattern Second :: LambdaPi n -> LambdaPi n -pattern Second t = Node (InR (SecondF t)) +pattern Second t = Node (R2 (SecondF t)) pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n -pattern Product l r = Node (InR (ProductF l r)) +pattern Product l r = Node (R2 (ProductF l r)) pattern Universe :: LambdaPi n -pattern Universe = Node (InL UniverseF) +pattern Universe = Node (L2 UniverseF) {-# COMPLETE Var, App, Lam, Pi, Pair, First, Second, Product, Universe #-} @@ -110,10 +126,32 @@ instance IsString (LambdaPi Foil.VoidS) where -- | Compute weak head normal form (WHNF) of a \(\lambda\Pi\)-term. -- -- >>> whnf Foil.emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)" --- λ x1 . λ x2 . x2 +-- λ x0 . λ x1 . x1 -- -- >>> whnf Foil.emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))" --- λ x1 . (λ x2 . λ x3 . x2 (x2 x3)) ((λ x2 . λ x3 . x2 (x2 x3)) x1) +-- λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1) +-- +-- Note that during computation bound variables can become unordered +-- in the sense that binders may easily repeat or decrease. For example, +-- in the following expression, inner binder has lower index that the outer one: +-- +-- >>> whnf Foil.emptyScope "(λx.λy.x)(λx.x)" +-- λ x1 . λ x0 . x0 +-- +-- At the same time, without substitution, we get regular, increasing binder indices: +-- +-- >>> "λx.λy.y" :: LambdaPi Foil.VoidS +-- λ x0 . λ x1 . x1 +-- +-- To compare terms for \(\alpha\)-equivalence, we may use 'alphaEquiv': +-- +-- >>> alphaEquiv Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y" +-- True +-- +-- We may also normalize binders using 'refreshAST': +-- +-- >>> refreshAST Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)") +-- λ x0 . λ x1 . x1 whnf :: Foil.Distinct n => Foil.Scope n -> LambdaPi n -> LambdaPi n whnf scope = \case App fun arg -> @@ -234,9 +272,34 @@ fromLambdaPi freshVars env = \case where loc = error "no location info available when converting from an AST" +-- | Convert back from a scope-safe \(\lambda\Pi\)-term into a raw expression or type. +-- +-- In contrast to 'fromLambdaPi', this function uses the raw foil identifiers (integers) +-- to generate names for the variables. This makes them transparent when printing. +fromLambdaPi' + :: LambdaPi n -- ^ A scope-safe \(\lambda\Pi\)-term. + -> Raw.Term +fromLambdaPi' = \case + Var name -> Raw.Var loc (ppName name) + App fun arg -> Raw.App loc (fromLambdaPi' fun) (fromLambdaPi' arg) + Lam binder body -> + let x = ppName (Foil.nameOf binder) + in Raw.Lam loc (Raw.PatternVar loc x) (Raw.AScopedTerm loc (fromLambdaPi' body)) + Pi binder a b -> + let x = ppName (Foil.nameOf binder) + in Raw.Pi loc (Raw.PatternVar loc x) (fromLambdaPi' a) (Raw.AScopedTerm loc (fromLambdaPi' b)) + Pair l r -> Raw.Pair loc (fromLambdaPi' l) (fromLambdaPi' r) + First t -> Raw.First loc (fromLambdaPi' t) + Second t -> Raw.Second loc (fromLambdaPi' t) + Product l r -> Raw.Product loc (fromLambdaPi' l) (fromLambdaPi' r) + Universe -> Raw.Universe loc + where + loc = error "no location info available when converting from an AST" + ppName name = Raw.VarIdent ("x" ++ show (Foil.nameId name)) + -- | Pretty-print a /closed/ \(\lambda\Pi\)-term. ppLambdaPi :: LambdaPi Foil.VoidS -> String -ppLambdaPi = Raw.printTree . fromLambdaPi [ Raw.VarIdent ("x" <> show i) | i <- [1 :: Integer ..] ] Foil.emptyNameMap +ppLambdaPi = Raw.printTree . fromLambdaPi' -- | Interpret a λΠ command. interpretCommand :: Raw.Command -> IO () diff --git a/haskell/lambda-pi/test/Language/LambdaPi/Impl/FoilSpec.hs b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FoilSpec.hs new file mode 100644 index 00000000..27f29fb6 --- /dev/null +++ b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FoilSpec.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE LambdaCase #-} +module Language.LambdaPi.Impl.FoilSpec where + +import Test.Hspec +import Test.QuickCheck +import Data.Bifunctor + +import qualified Control.Monad.Foil.Internal as Foil.Internal +import Control.Monad.Foil +import Language.LambdaPi.Impl.Foil + +shrinkExprs :: (Expr n, Expr l) -> [(Expr n, Expr l)] +shrinkExprs = \case + (AppE t1 t2, AppE t1' t2') -> [(t1, t1'), (t2, t2')] + (PairE t1 t2, PairE t1' t2') -> [(t1, t1'), (t2, t2')] + (FirstE t, FirstE t') -> [(t, t')] + (SecondE t, SecondE t') -> [(t, t')] + (ProductE t1 t2, ProductE t1' t2') -> [(t1, t1'), (t2, t2')] + (LamE x body, LamE x' body') -> + [ (LamE x t, LamE x' t') + | (t, t') <- shrinkExprs (body, body')] + (PiE x a b, PiE x' a' b') -> + [ (PiE x c d, PiE x' c' d') + | (c, c') <- shrinkExprs (a, a') + , (d, d') <- shrinkExprs (b, b')] + _ -> [] + +genExpr :: Distinct n => Scope n -> [Name n] -> Gen (Expr n) +genExpr scope names = fst <$> genAlphaEquivExprs withRefreshed scope scope (zip names names) + +-- | Generate a term that contains /approximately/ @n@ redexes for WHNF to deal with. +genNonWHNF :: Distinct n => Int -> Scope n -> [Name n] -> Gen (Expr n) +genNonWHNF n scope names = oneof + [ withFresh scope $ \binder -> do + body <- genNonWHNF n2 (extendScope binder scope) (nameOf binder : map sink names) + AppE (LamE (PatternVar binder) body) <$> go n2 + , FirstE <$> (PairE <$> go (n - 1) <*> go n) + , SecondE <$> (PairE <$> go n <*> go (n - 1)) + , go (n - 1) + ] + where + n2 = n `div` 2 + go k + | k < 1 = genExpr scope names + | otherwise = genNonWHNF k scope names + +genAlphaEquivExprs + :: (Distinct n, Distinct l) + => (forall x y r. Distinct x => Scope x -> Name y -> (forall o'. DExt x o' => NameBinder x o' -> r) -> r) + -> Scope n -> Scope l -> [(Name n, Name l)] -> Gen (Expr n, Expr l) +genAlphaEquivExprs withRefreshed' scope1 scope2 names = sized go + where + go n = oneof $ + map (pure . bimap VarE VarE) names ++ concat + [ if n < 1 then [] else [ do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (AppE f1 x1, AppE f2 x2) + , do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (PairE f1 x1, PairE f2 x2) + , bimap FirstE FirstE <$> go (n - 1) + , bimap SecondE SecondE <$> go (n - 1) + , do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (ProductE f1 x1, ProductE f2 x2) + , pure (UniverseE, UniverseE) + , do + name1 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + name2 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + withRefreshed' scope1 name1 $ \binder1 -> + withRefreshed' scope2 name2 $ \binder2 -> do + let names' = (nameOf binder1, nameOf binder2) : map (bimap sink sink) names + scope1' = extendScope binder1 scope1 + scope2' = extendScope binder2 scope2 + (a1, a2) <- go (n `div` 2) + (body1, body2) <- resize (n `div` 2) $ genAlphaEquivExprs withRefreshed' scope1' scope2' names' + return (PiE (PatternVar binder1) a1 body1, PiE (PatternVar binder2) a2 body2) + ] + -- allow LamE when we do not have any names + , if n < 1 && not (null names) then [] else [ do + name1 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + name2 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + withRefreshed' scope1 name1 $ \binder1 -> + withRefreshed' scope2 name2 $ \binder2 -> do + let names' = (nameOf binder1, nameOf binder2) : map (bimap sink sink) names + scope1' = extendScope binder1 scope1 + scope2' = extendScope binder2 scope2 + (body1, body2) <- resize (max 0 (n - 1)) $ genAlphaEquivExprs withRefreshed' scope1' scope2' names' + return (LamE (PatternVar binder1) body1, LamE (PatternVar binder2) body2) + ] + ] + +-- | Alter at most @n@ names in a given expression. +-- The result contains the number of unused changes and a new expression. +-- If the result contains the original number, then no changes took place. +alterNames :: Distinct n => Scope n -> [Name n] -> Int -> Expr n -> Gen (Int, Expr n) +alterNames scope names = go + where + go n = \case + t@(VarE x) -> elements $ + (n, t) : if n > 0 then [ (n - 1, VarE name) | name <- names, name /= x ] else [] + AppE l r -> do + (m, l') <- go n l + (k, r') <- go m r + return (k, AppE l' r') + LamE x body -> + case (assertExtPattern x, assertDistinctPattern x) of + (Ext, Distinct) -> fmap (LamE x) <$> + alterNames (extendScopePattern x scope) (namesOfPattern x ++ map sink names) n body + PiE x a b -> + case (assertExtPattern x, assertDistinctPattern x) of + (Ext, Distinct) -> do + (m, a') <- go n a + (k, b') <- alterNames (extendScopePattern x scope) (namesOfPattern x ++ map sink names) m b + return (k, PiE x a' b') + PairE l r -> do + (m, l') <- go n l + (k, r') <- go m r + return (k, PairE l' r') + FirstE t -> fmap FirstE <$> go n t + SecondE t -> fmap SecondE <$> go n t + ProductE l r -> do + (m, l') <- go n l + (k, r') <- go m r + return (k, ProductE l' r') + UniverseE -> pure (n, UniverseE) + +instance Arbitrary (Expr VoidS) where + arbitrary = genExpr emptyScope [] + +data AlphaEquiv = AlphaEquiv Bool (Expr VoidS) (Expr VoidS) + +instance Show AlphaEquiv where + show (AlphaEquiv equiv t1 t2) = unlines + [ "t1 = " <> show t1 + , "t2 = " <> show t2 + , if equiv + then "t1 and t2 are α-equivalent" + else "t1 and t2 are not α-equivalent" + ] + +instance Arbitrary AlphaEquiv where + arbitrary = do + (t, t') <- genAlphaEquivExprs withRefreshed emptyScope emptyScope [] + (n, alt) <- alterNames emptyScope [] 1 t + return (AlphaEquiv (n == 1) alt t') + + -- cannot shrink non-equivalent pair + -- since we do not know which subterm contains non-equivalent part + shrink (AlphaEquiv False _ _) = [] + -- if terms are equivalent, then we can shrink + shrink (AlphaEquiv True t t') = + [ AlphaEquiv True s s' + | (s, s') <- shrinkExprs (t, t') + ] + +newtype AlphaEquivRefreshed = AlphaEquivRefreshed AlphaEquiv + deriving (Arbitrary) + +instance Show AlphaEquivRefreshed where + show (AlphaEquivRefreshed ae@(AlphaEquiv _equiv t1 t2)) = unlines + [ show ae + , "refreshExpr _ t1 = " <> show (refreshExpr emptyScope t1) + , "refreshExpr _ t2 = " <> show (refreshExpr emptyScope t2) + , "alphaEquivRefreshed _ t1 t2 = " <> show (alphaEquivRefreshed emptyScope t1 t2) + ] + +genExprWithFresh :: (Distinct n, Distinct l) => Scope n -> Scope l -> [(Name n, Name l)] -> Gen (Expr n, Expr l) +genExprWithFresh = genAlphaEquivExprs (\s _ -> withFresh s) + +data ExprWithFresh = ExprWithFresh (Expr VoidS) (Expr VoidS) + +instance Arbitrary ExprWithFresh where + arbitrary = do + (t, t') <- genExprWithFresh emptyScope emptyScope [] + return (ExprWithFresh t t') + shrink (ExprWithFresh t t') = + [ ExprWithFresh s s' + | (s, s') <- shrinkExprs (t, t') + ] + +instance Show ExprWithFresh where + show (ExprWithFresh t t') = unlines + [ " t = " <> show t + , " fresh t = " <> show t' + , "refreshExpr _ t = " <> show (refreshExpr emptyScope t) + ] + +spec :: Spec +spec = do + describe "α-equivalence" $ do + it "refreshExpr is correct" $ property $ \(ExprWithFresh t t') -> + refreshExpr emptyScope t `unsafeEqExpr` t' + it "alphaEquiv is correct" $ property $ \(AlphaEquiv equiv t t') -> + alphaEquiv emptyScope t t' `shouldBe` equiv + it "alphaEquivRefreshed is correct" $ property $ \(AlphaEquivRefreshed (AlphaEquiv equiv t t')) -> + alphaEquivRefreshed emptyScope t t' `shouldBe` equiv + describe "weak head normal form (WHNF)" $ do + it "whnf is idempotent (strictly, not just up to α-equivalence)" $ property $ forAll (genNonWHNF 10 emptyScope []) $ \t -> + discardAfter 100000 $ -- discard tests where whnf hangs + let t' = whnf emptyScope t + in whnf emptyScope t' `unsafeEqExpr` t' diff --git a/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs new file mode 100644 index 00000000..a72396f4 --- /dev/null +++ b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs @@ -0,0 +1,175 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.LambdaPi.Impl.FreeFoilSpec where + +import Control.Monad.State +import Test.Hspec +import Test.QuickCheck +import Data.Bifunctor +import Data.Bitraversable + +import qualified Control.Monad.Foil.Internal as Foil.Internal +import Control.Monad.Foil +import Control.Monad.Free.Foil +import Language.LambdaPi.Impl.FreeFoil + +shrinkLambdaPis :: (LambdaPi n, LambdaPi l) -> [(LambdaPi n, LambdaPi l)] +shrinkLambdaPis = \case + (App t1 t2, App t1' t2') -> [(t1, t1'), (t2, t2')] + (Pair t1 t2, Pair t1' t2') -> [(t1, t1'), (t2, t2')] + (First t, First t') -> [(t, t')] + (Second t, Second t') -> [(t, t')] + (Product t1 t2, Product t1' t2') -> [(t1, t1'), (t2, t2')] + (Lam x body, Lam x' body') -> + [ (Lam x t, Lam x' t') + | (t, t') <- shrinkLambdaPis (body, body')] + (Pi x a b, Pi x' a' b') -> + [ (Pi x c d, Pi x' c' d') + | (c, c') <- shrinkLambdaPis (a, a') + , (d, d') <- shrinkLambdaPis (b, b')] + _ -> [] + +genLambdaPi :: Distinct n => Scope n -> [Name n] -> Gen (LambdaPi n) +genLambdaPi scope names = fst <$> genAlphaEquivLambdaPis withRefreshed scope scope (zip names names) + +genAlphaEquivLambdaPis + :: (Distinct n, Distinct l) + => (forall x y r. Distinct x => Scope x -> Name y -> (forall o'. DExt x o' => NameBinder x o' -> r) -> r) + -> Scope n -> Scope l -> [(Name n, Name l)] -> Gen (LambdaPi n, LambdaPi l) +genAlphaEquivLambdaPis withRefreshed' scope1 scope2 names = sized go + where + go n = oneof $ + map (pure . bimap Var Var) names ++ concat + [ if n < 1 then [] else [ do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (App f1 x1, App f2 x2) + , do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (Pair f1 x1, Pair f2 x2) + , bimap First First <$> go (n - 1) + , bimap Second Second <$> go (n - 1) + , do + (f1, f2) <- go (n `div` 2) + (x1, x2) <- go (n `div` 2) + return (Product f1 x1, Product f2 x2) + , pure (Universe, Universe) + , do + name1 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + name2 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + withRefreshed' scope1 name1 $ \binder1 -> + withRefreshed' scope2 name2 $ \binder2 -> do + let names' = (nameOf binder1, nameOf binder2) : map (bimap sink sink) names + scope1' = extendScope binder1 scope1 + scope2' = extendScope binder2 scope2 + (a1, a2) <- go (n `div` 2) + (body1, body2) <- resize (n `div` 2) $ genAlphaEquivLambdaPis withRefreshed' scope1' scope2' names' + return (Pi binder1 a1 body1, Pi binder2 a2 body2) + ] + , if n < 1 && not (null names) then [] else [ do + name1 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + name2 <- Foil.Internal.UnsafeName <$> choose (1, 1000) + withRefreshed' scope1 name1 $ \binder1 -> + withRefreshed' scope2 name2 $ \binder2 -> do + let names' = (nameOf binder1, nameOf binder2) : map (bimap sink sink) names + scope1' = extendScope binder1 scope1 + scope2' = extendScope binder2 scope2 + (body1, body2) <- resize (max 0 (n - 1)) $ genAlphaEquivLambdaPis withRefreshed' scope1' scope2' names' + return (Lam binder1 body1, Lam binder2 body2) + ] + ] + +-- | Alter at most @n@ names in a given expression. +-- The result contains the number of unused changes and a new expression. +-- If the result contains the original number, then no changes took place. +alterNames :: Distinct n => Scope n -> [Name n] -> LambdaPi n -> StateT Int Gen (LambdaPi n) +alterNames scope names = go + where + go = \case + t@(Var x) -> do + n <- get + (m, t') <- lift $ elements $ + (n, t) : if n > 0 then [ (n - 1, Var name) | name <- names, name /= x ] else [] + put m + return t' + Node node -> Node <$> bitraverse goScoped go node + + goScoped (ScopedAST binder body) = + case (assertExt binder, assertDistinct binder) of + (Ext, Distinct) -> ScopedAST binder <$> + alterNames (extendScope binder scope) (nameOf binder : map sink names) body + +instance Arbitrary (LambdaPi VoidS) where + arbitrary = genLambdaPi emptyScope [] + +data AlphaEquiv = AlphaEquiv Bool (LambdaPi VoidS) (LambdaPi VoidS) + +instance Show AlphaEquiv where + show (AlphaEquiv equiv t1 t2) = unlines + [ "t1 = " <> show t1 + , "t2 = " <> show t2 + , if equiv + then "t1 and t2 are α-equivalent" + else "t1 and t2 are not α-equivalent" + ] + +instance Arbitrary AlphaEquiv where + arbitrary = do + (t, t') <- genAlphaEquivLambdaPis withRefreshed emptyScope emptyScope [] + (alt, n) <- runStateT (alterNames emptyScope [] t) 1 + return (AlphaEquiv (n == 1) alt t') + + -- cannot shrink non-equivalent pair + -- since we do not know which subterm contains non-equivalent part + shrink (AlphaEquiv False _ _) = [] + -- if terms are equivalent, then we can shrink + shrink (AlphaEquiv True t t') = + [ AlphaEquiv True s s' + | (s, s') <- shrinkLambdaPis (t, t') + ] + +newtype AlphaEquivRefreshed = AlphaEquivRefreshed AlphaEquiv + deriving (Arbitrary) + +instance Show AlphaEquivRefreshed where + show (AlphaEquivRefreshed ae@(AlphaEquiv _equiv t1 t2)) = unlines + [ show ae + , "refreshAST _ t1 = " <> show (refreshAST emptyScope t1) + , "refreshAST _ t2 = " <> show (refreshAST emptyScope t2) + , "alphaEquivRefreshed _ t1 t2 = " <> show (alphaEquivRefreshed emptyScope t1 t2) + ] + +data LambdaPiWithFresh = LambdaPiWithFresh (LambdaPi VoidS) (LambdaPi VoidS) + +instance Arbitrary LambdaPiWithFresh where + arbitrary = do + (t, t') <- genAlphaEquivLambdaPis (\s _ -> withFresh s) emptyScope emptyScope [] + return (LambdaPiWithFresh t t') + + shrink (LambdaPiWithFresh t t') = + [ LambdaPiWithFresh s s' + | (s, s') <- shrinkLambdaPis (t, t') + ] + +instance Show LambdaPiWithFresh where + show (LambdaPiWithFresh t t') = unlines + [ " t = " <> show t + , " fresh t = " <> show t' + , "refreshAST _ t = " <> show (refreshAST emptyScope t) + ] + +spec :: Spec +spec = do + describe "α-equivalence" $ do + it "refreshAST is correct" $ property $ \(LambdaPiWithFresh t t') -> + refreshAST emptyScope t `unsafeEqAST` t' + it "alphaEquiv is correct" $ property $ \(AlphaEquiv equiv t t') -> + alphaEquiv emptyScope t t' `shouldBe` equiv + it "alphaEquivRefreshed is correct" $ property $ \(AlphaEquivRefreshed (AlphaEquiv equiv t t')) -> + alphaEquivRefreshed emptyScope t t' `shouldBe` equiv diff --git a/haskell/lambda-pi/test/Spec.hs b/haskell/lambda-pi/test/Spec.hs index cd4753fc..a824f8c3 100644 --- a/haskell/lambda-pi/test/Spec.hs +++ b/haskell/lambda-pi/test/Spec.hs @@ -1,2 +1 @@ -main :: IO () -main = putStrLn "Test suite not yet implemented" +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}