diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,28 @@ +BSD 3-Clause License + +Copyright (c) 2023, Nikolai Kudasov + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,2 @@ +# free-foil +Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,6 @@ +module Main (main) where + +import Distribution.Simple (defaultMain) + +main :: IO () +main = defaultMain diff --git a/free-foil.cabal b/free-foil.cabal new file mode 100644 --- /dev/null +++ b/free-foil.cabal @@ -0,0 +1,93 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.36.0. +-- +-- see: https://github.com/sol/hpack + +name: free-foil +version: 0.0.2 +synopsis: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) +description: Please see the README on GitHub at +category: Parsing +homepage: https://github.com/fizruk/free-foil#readme +bug-reports: https://github.com/fizruk/free-foil/issues +author: Nikolai Kudasov +maintainer: nickolay.kudasov@gmail.com +copyright: 2023–2024 Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + LICENSE + +source-repository head + type: git + location: https://github.com/fizruk/free-foil + +library + exposed-modules: + Control.Monad.Foil + Control.Monad.Foil.Example + Control.Monad.Foil.Internal + Control.Monad.Foil.Relative + Control.Monad.Foil.TH + Control.Monad.Foil.TH.MkFoilData + Control.Monad.Foil.TH.MkFromFoil + Control.Monad.Foil.TH.MkInstancesFoil + Control.Monad.Foil.TH.MkToFoil + Control.Monad.Foil.TH.Util + Control.Monad.Free.Foil + Control.Monad.Free.Foil.Example + other-modules: + Paths_free_foil + hs-source-dirs: + src + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , template-haskell >=2.21.0.0 + , text >=1.2.3.1 + default-language: Haskell2010 + +test-suite doctests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: + src/ + test/doctests + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , doctest-parallel + , free-foil + , template-haskell >=2.21.0.0 + , text >=1.2.3.1 + default-language: Haskell2010 + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Paths_free_foil + hs-source-dirs: + test + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , free-foil + , template-haskell >=2.21.0.0 + , text >=1.2.3.1 + default-language: Haskell2010 diff --git a/src/Control/Monad/Foil.hs b/src/Control/Monad/Foil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil.hs @@ -0,0 +1,58 @@ +-- | Main definitions of the foil that can be +-- reused for specific implementations. +-- +-- The original description of this approach +-- is described in 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). +-- This module also introduces 'CoSinkable' class, +-- generalizing handling of patterns, as described in +-- [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384). +-- +-- Since the representation of scopes and substitutions +-- is either 'IntMap' or 'IntSet', many of the operations +-- have a worst-case complexity of \(O(\min(n,W))\). +-- This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\) +-- — the number of bits in an 'Int' (32 or 64). +module Control.Monad.Foil ( + -- * Safe scopes, names, and binders + S(..), + Scope, + Name, + NameBinder, + emptyScope, + extendScope, + member, + nameOf, + nameId, + withFreshBinder, + withFresh, + withRefreshed, + unsinkName, + -- * Safe (co)sinking + Sinkable(..), + CoSinkable(..), + sink, + extendRenaming, + extendRenamingNameBinder, + -- * Safe substitutions + Substitution, + lookupSubst, + identitySubst, + addSubst, + addRename, + -- * Name maps + NameMap, + emptyNameMap, + lookupName, + addNameBinder, + -- * Constraints + Ext, + ExtEvidence(..), + Distinct, + DistinctEvidence(..), + assertDistinct, + DExt, + InjectName(..), +) where + +import Control.Monad.Foil.Internal diff --git a/src/Control/Monad/Foil/Example.hs b/src/Control/Monad/Foil/Example.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/Example.hs @@ -0,0 +1,155 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +-- | Example implementation of untyped \(\lambda\)-calculus with the foil. +module Control.Monad.Foil.Example where + +import Control.DeepSeq +import Control.Monad.Foil +import Control.Monad.Foil.Relative + +-- $setup +-- >>> import Control.Monad.Foil + +-- | Untyped \(\lambda\)-terms in scope @n@. +data Expr n where + -- | Variables are names in scope @n@: \(x\) + VarE :: Name n -> Expr n + -- | Application of one term to another: \((t_1, t_2)\) + AppE :: Expr n -> Expr n -> Expr n + -- | \(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\) + LamE :: NameBinder n l -> Expr l -> Expr n + +-- | Use 'ppExpr' to show \(\lambda\)-terms. +instance Show (Expr n) where + show = ppExpr + +instance NFData (Expr l) where + rnf (LamE binder body) = rnf binder `seq` rnf body + rnf (AppE fun arg) = rnf fun `seq` rnf arg + rnf (VarE name) = rnf name + +-- | This instance serves as a proof +-- that sinking of 'Expr' is safe. +instance Sinkable Expr where + sinkabilityProof rename (VarE v) = VarE (rename v) + sinkabilityProof rename (AppE f e) = AppE (sinkabilityProof rename f) (sinkabilityProof rename e) + sinkabilityProof rename (LamE binder body) = extendRenaming rename binder $ \rename' binder' -> + LamE binder' (sinkabilityProof rename' body) + +instance InjectName Expr where + injectName = VarE + +-- | 'Expr' is a monad relative to 'Name'. +instance RelMonad Name Expr where + rreturn = VarE + rbind scope term subst = + case term of + VarE name -> subst name + AppE x y -> AppE (rbind scope x subst) (rbind scope y subst) + LamE binder body -> + withRefreshed scope (nameOf binder) $ \binder' -> + let scope' = extendScope binder' scope + subst' name = case unsinkName binder name of + Nothing -> rreturn (nameOf binder') + Just n -> sink (subst n) + in LamE binder' (rbind scope' body subst') + +-- | Substitution for untyped \(\lambda\)-terms. +-- The foil helps implement this function without forgetting scope extensions and renaming. +substitute :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o +substitute scope subst = \case + VarE name -> lookupSubst subst name + AppE f x -> AppE (substitute scope subst f) (substitute scope subst x) + LamE binder body -> withRefreshed scope (nameOf binder) $ \binder' -> + let subst' = addRename (sink subst) binder (nameOf binder') + scope' = extendScope binder' scope + body' = substitute scope' subst' body + in LamE binder' body' + +-- | Compute weak head normal form (WHNF) of a \(\lambda\)-term. +-- +-- >>> whnf emptyScope (AppE (churchN 2) (churchN 2)) +-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1)) +whnf :: Distinct n => Scope n -> Expr n -> Expr n +whnf scope = \case + AppE fun arg -> + case whnf scope fun of + LamE binder body -> + let subst = addSubst identitySubst binder arg + in whnf scope (substitute scope subst body) + fun' -> AppE fun' arg + t -> t + +-- | Compute weak head normal form (WHNF) of a __closed__ \(\lambda\)-term. +-- +-- >>> whnf' (AppE (churchN 2) (churchN 2)) +-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1)) +whnf' :: Expr VoidS -> Expr VoidS +whnf' = whnf emptyScope + +-- | Compute normal form (NF) of a \(\lambda\)-term. +-- +-- >>> nf emptyScope (AppE (churchN 2) (churchN 2)) +-- λx1. λx2. (x1 (x1 (x1 (x1 x2)))) +nf :: Distinct n => Scope n -> Expr n -> Expr n +nf scope expr = case expr of + LamE binder body -> + -- Instead of using 'assertDistinct', + -- another option is to add 'Distinct l' constraint + -- to the definition of 'LamE'. + case assertDistinct binder of + Distinct -> + let scope' = extendScope binder scope + in LamE binder (nf scope' body) + AppE fun arg -> + case whnf scope fun of + LamE binder body -> + let subst = addSubst identitySubst binder arg + in nf scope (substitute scope subst body) + fun' -> AppE (nf scope fun') (nf scope arg) + t -> t + +-- | Compute normal form (NF) of a __closed__ \(\lambda\)-term. +-- +-- >>> nf' (AppE (churchN 2) (churchN 2)) +-- λx1. λx2. (x1 (x1 (x1 (x1 x2)))) +nf' :: Expr VoidS -> Expr VoidS +nf' = nf emptyScope + +-- | Pretty print a name. +ppName :: Name n -> String +ppName name = "x" <> show (nameId name) + +-- | Pretty-print a \(\lambda\)-term. +-- +-- >>> ppExpr (churchN 3) +-- "\955x0. \955x1. (x0 (x0 (x0 x1)))" +ppExpr :: Expr n -> String +ppExpr = \case + VarE name -> ppName name + AppE x y -> "(" <> ppExpr x <> " " <> ppExpr y <> ")" + LamE binder body -> "λ" <> ppName (nameOf binder) <> ". " <> ppExpr body + +-- | A helper for constructing \(\lambda\)-abstractions. +lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n +lam scope mkBody = withFresh scope $ \x -> + let scope' = extendScope x scope + in LamE x (mkBody scope' x) + +-- | Church-encoding of a natural number \(n\). +-- +-- >>> churchN 0 +-- λx0. λx1. x1 +-- +-- >>> churchN 3 +-- λx0. λx1. (x0 (x0 (x0 x1))) +churchN :: Int -> Expr VoidS +churchN n = + lam emptyScope $ \sx nx -> + lam sx $ \_sxy ny -> + let x = sink (VarE (nameOf nx)) + y = VarE (nameOf ny) + in iterate (AppE x) y !! n diff --git a/src/Control/Monad/Foil/Internal.hs b/src/Control/Monad/Foil/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/Internal.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# OPTIONS_GHC -Wno-redundant-constraints #-} +-- | Main definitions of the foil that can be +-- reused for specific implementations. +-- This is an internal module, so it also contains implementation details of the foil. +-- +-- The original description of this approach +-- is described in 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). +-- This module also introduces 'CoSinkable' class, +-- generalizing handling of patterns, as described in +-- [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384). +-- +-- Since the representation of scopes and substitutions +-- is either 'IntMap' or 'IntSet', many of the operations +-- have a worst-case complexity of \(O(\min(n,W))\). +-- This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\) +-- — the number of bits in an 'Int' (32 or 64). +module Control.Monad.Foil.Internal where + +import Control.DeepSeq (NFData (..)) +import Data.IntMap +import qualified Data.IntMap as IntMap +import Data.IntSet +import qualified Data.IntSet as IntSet +import Data.Kind (Type) +import Unsafe.Coerce + +-- * Safe types and operations + +-- | 'S' is a data kind of scope indices. +data S + = VoidS -- ^ 'VoidS' is the only explicit scope available to the users, representing an empty scope. + -- All other scopes are represented with type variables, + -- bound in rank-2 polymophic functions like 'withFreshBinder'. + +-- | A safe scope, indexed by a type-level scope index 'n'. +newtype Scope (n :: S) = UnsafeScope RawScope + deriving newtype NFData + +-- | A name in a safe scope, indexed by a type-level scope index 'n'. +newtype Name (n :: S) = UnsafeName RawName + deriving newtype (NFData, Eq, Ord, Show) + +-- | A name binder is a name that extends scope @n@ to a (larger) scope @l@. +newtype NameBinder (n :: S) (l :: S) = + UnsafeNameBinder (Name l) + deriving newtype (NFData, Eq, Ord, Show) + +-- | An empty scope (without any names). +emptyScope :: Scope VoidS +emptyScope = UnsafeScope IntSet.empty + +-- | \(O(\min(n,W))\). +-- Extend a scope with one name (safely). +-- Note that as long as the foil is used as intended, +-- the name binder is guaranteed to introduce a name +-- that does not appear in the initial scope. +extendScope :: NameBinder n l -> Scope n -> Scope l +extendScope (UnsafeNameBinder (UnsafeName name)) (UnsafeScope scope) = + UnsafeScope (IntSet.insert name scope) + +-- | A runtime check for potential name capture. +member :: Name l -> Scope n -> Bool +member (UnsafeName name) (UnsafeScope s) = rawMember name s + +-- | Extract name from a name binder. +nameOf :: NameBinder n l -> Name l +nameOf (UnsafeNameBinder name) = name + +-- | Convert 'Name' into an identifier. +-- This may be useful for printing and debugging. +nameId :: Name l -> Id +nameId (UnsafeName i) = i + +-- | Allocate a fresh binder for a given scope. +withFreshBinder + :: Scope n + -> (forall l. NameBinder n l -> r) -> r +withFreshBinder (UnsafeScope scope) cont = + cont binder + where + binder = UnsafeNameBinder (UnsafeName (rawFreshName scope)) + +-- | Evidence that scope @n@ contains distinct names. +data DistinctEvidence (n :: S) where + Distinct :: Distinct n => DistinctEvidence n + +-- | Unsafely declare that scope @n@ is distinct. +-- Used in 'unsafeAssertFresh'. +unsafeDistinct :: DistinctEvidence n +unsafeDistinct = unsafeCoerce (Distinct :: DistinctEvidence VoidS) + +-- | Evidence that scope @l@ extends scope @n@. +data ExtEvidence (n :: S) (l :: S) where + Ext :: Ext n l => ExtEvidence n l + +-- | Unsafely declare that scope @l@ extends scope @n@. +-- Used in 'unsafeAssertFresh'. +unsafeExt :: ExtEvidence n l +unsafeExt = unsafeCoerce (Ext :: ExtEvidence VoidS VoidS) + +-- | Safely produce a fresh name binder with respect to a given scope. +withFresh + :: Distinct n => Scope n + -> (forall l. DExt n l => NameBinder n l -> r) -> r +withFresh scope cont = withFreshBinder scope (`unsafeAssertFresh` cont) + +-- | Unsafely declare that a given name (binder) +-- is already fresh in any scope @n'@. +unsafeAssertFresh :: forall n l n' l' r. NameBinder n l + -> (DExt n' l' => NameBinder n' l' -> r) -> r +unsafeAssertFresh binder cont = + case unsafeDistinct @l' of + Distinct -> case unsafeExt @n' @l' of + Ext -> cont (unsafeCoerce binder) + +-- | A distinct scope extended with a 'NameBinder' is also distinct. +assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l +assertDistinct _ = unsafeDistinct + +-- | 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. +withRefreshed + :: Distinct o + => Scope o -- ^ Ambient scope. + -> Name i -- ^ Name to refresh (if it clashes with the ambient scope). + -> (forall o'. DExt o o' => NameBinder o o' -> r) + -- ^ Continuation, accepting the refreshed name. + -> r +withRefreshed scope@(UnsafeScope rawScope) name@(UnsafeName rawName) cont + | IntSet.member rawName rawScope = withFresh scope cont + | otherwise = unsafeAssertFresh (UnsafeNameBinder name) cont + +-- | Try coercing the name back to the (smaller) scope, +-- given a binder that extends that scope. +unsinkName :: NameBinder n l -> Name l -> Maybe (Name n) +unsinkName binder name@(UnsafeName raw) + | nameOf binder == name = Nothing + | otherwise = Just (UnsafeName raw) + +-- * Safe sinking + +-- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@, +-- given the renaming (injection from scope @n@ to scope @l@). +class Sinkable (e :: S -> Type) where + -- | An implementation of this method that typechecks + -- proves to the compiler that the expression is indeed + -- 'Sinkable'. However, instead of this implementation, 'sink' + -- should be used at all call sites for efficiency. + sinkabilityProof + :: (Name n -> Name l) -- ^ Map names from scope @n@ to a (possibly larger) scope @l@. + -> e n -- ^ Expression with free variables in scope @n@. + -> e l + +-- | Sinking a 'Name' is as simple as applying the renaming. +instance Sinkable Name where + sinkabilityProof rename = rename + +-- | Efficient version of 'sinkabilityProof'. +-- In fact, once 'sinkabilityProof' typechecks, +-- it is safe to 'sink' by coercion. +-- See Section 3.5 in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details. +sink :: (Sinkable e, DExt n l) => e n -> e l +sink = unsafeCoerce + +-- | Extend renaming when going under a 'CoSinkable' pattern (generalized binder). +-- Note that the scope under pattern is independent of the codomain of the renaming. +-- +-- This function is used to go under binders when implementing 'sinkabilityProof' +-- and is both a generalization of 'extendRenamingNameBinder' and an efficient implementation of 'coSinkabilityProof'. +extendRenaming + :: CoSinkable pattern + => (Name n -> Name 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'. (Name l -> Name 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 +extendRenaming _ pattern cont = + cont unsafeCoerce (unsafeCoerce pattern) + +-- | Extend renaming when going under a 'NameBinder'. +-- Note that the scope under binder is independent of the codomain of the renaming. +-- +-- Semantically, this function may need to rename the binder (resulting in the new scope @l'@), +-- to make sure it does not clash with scope @n'@. +-- However, as it turns out, the foil makes it safe +-- to implement this function as a coercion. +-- See Appendix A in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details. +-- +-- This function is used to go under binders when implementing 'sinkabilityProof'. +-- A generalization of this function is 'extendRenaming' (which is an efficient version of 'coSinkabilityProof'). +extendRenamingNameBinder + :: (Name n -> Name n') -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@. + -> NameBinder n l -- ^ A name binder that extends scope @n@ to another scope @l@. + -> (forall l'. (Name l -> Name l') -> NameBinder n' l' -> r ) + -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@) + -- and a (possibly refreshed) binder that extends @n'@ to @l'@. + -> r +extendRenamingNameBinder _ (UnsafeNameBinder name) cont = + cont unsafeCoerce (UnsafeNameBinder name) + +-- | 'CoSinkable' is to patterns (generalized binders) +-- what 'Sinkable' is to expressions. +-- +-- See Section 2.3 of [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384) for more details. +class CoSinkable (pattern :: S -> S -> Type) where + -- | An implementation of this method that typechecks + -- proves to the compiler that the pattern is indeed + -- 'CoSinkable'. However, instead of this implementation, + -- 'extendRenaming' should be used at all call sites for efficiency. + coSinkabilityProof + :: (Name n -> Name 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'. (Name l -> Name 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 + +instance CoSinkable NameBinder where + coSinkabilityProof _rename (UnsafeNameBinder name) cont = + cont unsafeCoerce (UnsafeNameBinder name) + +-- * Safe substitions + +-- | A substitution is a mapping from names in scope @i@ +-- to expressions @e o@ in scope @o@. +newtype Substitution (e :: S -> Type) (i :: S) (o :: S) = + UnsafeSubstitution (IntMap (e o)) + +-- | Apply substitution to a given name. +lookupSubst :: InjectName e => Substitution e i o -> Name i -> e o +lookupSubst (UnsafeSubstitution env) (UnsafeName name) = + case IntMap.lookup name env of + Just ex -> ex + Nothing -> injectName (UnsafeName name) + +-- | Identity substitution maps all names to expresion-variables. +identitySubst + :: InjectName e => Substitution e i i +identitySubst = UnsafeSubstitution IntMap.empty + +-- | Extend substitution with a particular mapping. +addSubst + :: Substitution e i o + -> NameBinder i i' + -> e o + -> Substitution e i' o +addSubst (UnsafeSubstitution env) (UnsafeNameBinder (UnsafeName name)) ex + = UnsafeSubstitution (IntMap.insert name ex env) + +-- | Add variable renaming to a substitution. +-- This includes the performance optimization of eliding names mapped to themselves. +addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o +addRename s@(UnsafeSubstitution env) b@(UnsafeNameBinder (UnsafeName name1)) n@(UnsafeName name2) + | name1 == name2 = UnsafeSubstitution (IntMap.delete name1 env) + | otherwise = addSubst s b (injectName n) + +-- | Substitutions are sinkable as long as corresponding expressions are. +instance (Sinkable e) => Sinkable (Substitution e i) where + sinkabilityProof rename (UnsafeSubstitution env) = + UnsafeSubstitution (fmap (sinkabilityProof rename) env) + +-- * 'Name' maps + +-- | A /total/ map from names in scope @n@ to elements of type @a@. +newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } + +-- | An empty map belongs in the empty scope. +emptyNameMap :: NameMap VoidS a +emptyNameMap = NameMap IntMap.empty + +-- | Looking up a name should always succeed. +-- +-- Note that since 'Name' is 'Sinkable', you can lookup a name from scope @n@ in a 'NameMap' for scope @l@ whenever @l@ extends @n@. +lookupName :: Name n -> NameMap n a -> a +lookupName name (NameMap m) = + case IntMap.lookup (nameId name) m of + Nothing -> error "impossible: unknown name in a NameMap" + Just x -> x + +-- | Extending a map with a single mapping. +-- +-- Note that the scope parameter of the result differs from the initial map. +addNameBinder :: NameBinder n l -> a -> NameMap n a -> NameMap l a +addNameBinder name x (NameMap m) = NameMap (IntMap.insert (nameId (nameOf name)) x m) + +-- * Raw types and operations + +-- | We will use 'Int' for efficient representation of identifiers. +type Id = Int + +-- | Raw name is simply an identifier. +type RawName = Id + +-- | A raw scope is a set of raw names. +type RawScope = IntSet + +-- | \(O(\min(n, W))\). +-- Generate a fresh raw name that +-- does not appear in a given raw scope. +rawFreshName :: RawScope -> RawName +rawFreshName scope | IntSet.null scope = 0 + | otherwise = IntSet.findMax scope + 1 + +-- | Check if a raw name is contained in a raw scope. +rawMember :: RawName -> RawScope -> Bool +rawMember = IntSet.member + +-- * Constraints + +-- | Every scope is a (trivial) extension of itself. +-- +-- __Important__: this class exists to assist tracking scope extensions +-- for type variables of kind 'S'. +-- Users of the foil are not supposed to implement any instances of 'ExtEndo'. +class ExtEndo (n :: S) + +-- | Some scopes are extensions of other scopes. +-- +-- __Important__: this class exists to assist tracking scope extensions +-- for type variables of kind 'S'. +-- Users of the foil are not supposed to implement any instances of 'Ext'. +class (ExtEndo n => ExtEndo l ) => Ext (n :: S) (l :: S) +instance ( ExtEndo n => ExtEndo l ) => Ext n l + +-- | Scopes with distinct names. +-- +-- __Important__: this class exists to explicitly +-- mark scopes with distinct names. +-- Users of the foil are not supposed to implement any instances of 'Distinct'. +class Distinct (n :: S) +instance Distinct VoidS + +-- | Scope extensions with distinct names. +type DExt n l = (Distinct l, Ext n l) + +-- | Instances of this typeclass possess the ability to inject names. +-- Usually, this is a variable data constructor. +class InjectName (e :: S -> Type) where + -- | Inject names into expressions. + injectName :: Name n -> e n diff --git a/src/Control/Monad/Foil/Relative.hs b/src/Control/Monad/Foil/Relative.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/Relative.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +module Control.Monad.Foil.Relative where + +import Control.Monad.Foil +import Data.Kind (Type) + +-- | Relative monads, restricted to types indexed by scopes in kind 'S'. +class RelMonad (f :: S -> Type) (m :: S -> Type) where + -- | Relative version of 'return'. + rreturn :: f a -> m a + + -- | Relative version of '>>='. + -- + -- Note the two special additions to the usual definition of a relative binding operation: + -- + -- 1. @'Scope' b@ is added since is corresponds to the runtime counterpart of the type parameter @b@. + -- 2. @t'Distinct' b@ constraint helps to ensure we only work with scopes that are distinct. + -- + -- Technically, it is also possible add similar components for @a@ parameter. + -- 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 diff --git a/src/Control/Monad/Foil/TH.hs b/src/Control/Monad/Foil/TH.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH.hs @@ -0,0 +1,11 @@ +module Control.Monad.Foil.TH ( + module Control.Monad.Foil.TH.MkFoilData, + module Control.Monad.Foil.TH.MkToFoil, + module Control.Monad.Foil.TH.MkFromFoil, + module Control.Monad.Foil.TH.MkInstancesFoil +) where + +import Control.Monad.Foil.TH.MkFoilData +import Control.Monad.Foil.TH.MkFromFoil +import Control.Monad.Foil.TH.MkInstancesFoil +import Control.Monad.Foil.TH.MkToFoil diff --git a/src/Control/Monad/Foil/TH/MkFoilData.hs b/src/Control/Monad/Foil/TH/MkFoilData.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH/MkFoilData.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskellQuotes #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} +module Control.Monad.Foil.TH.MkFoilData (mkFoilData) where + +import Language.Haskell.TH + +import qualified Control.Monad.Foil.Internal as Foil +import Control.Monad.Foil.TH.Util + +-- | Generate scope-safe variants given names of types for the raw representation. +mkFoilData + :: Name -- ^ Type name for raw terms. + -> Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw scoped terms. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkFoilData termT nameT scopeT patternT = do + n <- newName "n" + l <- newName "l" + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT + TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT + + foilPatternCons <- mapM (toPatternCon patternTVars n) patternCons + let foilScopeCons = map (toScopeCon scopeTVars n) scopeCons + let foilTermCons = map (toTermCon termTVars n l) termCons + + return + [ DataD [] foilTermT (termTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilTermCons [] + , DataD [] foilScopeT (scopeTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilScopeCons [] + , DataD [] foilPatternT (patternTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S), KindedTV l BndrReq (PromotedT ''Foil.S)]) Nothing foilPatternCons [] + ] + where + foilTermT = mkName ("Foil" ++ nameBase termT) + foilScopeT = mkName ("Foil" ++ nameBase scopeT) + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + -- | Convert a constructor declaration for a raw pattern type + -- into a constructor for the scope-safe pattern type. + toPatternCon + :: [TyVarBndr BndrVis] + -> Name -- ^ Name for the starting scope type variable. + -> Con -- ^ Raw pattern constructor. + -> Q Con + toPatternCon tvars n (NormalC conName params) = do + (lastScopeName, foilParams) <- toPatternConParams 1 n params + let foilConName = mkName ("Foil" ++ nameBase conName) + return (GadtC [foilConName] foilParams (PeelConT foilPatternT (map (VarT . tvarName) tvars ++ [VarT n, VarT lastScopeName]))) + where + -- | Process type parameters of a pattern, + -- introducing (existential) type variables for the intermediate scopes, + -- if necessary. + toPatternConParams + :: Int -- ^ Index of the component in the constructor. + -> Name -- ^ Current scope (after processing any previous bindings). + -> [BangType] -- ^ Leftover pattern components. + -> Q (Name, [BangType]) -- ^ Resulting extended scope and a list of corresponding scope-safe components. + toPatternConParams _ p [] = return (p, []) + toPatternConParams i p (param@(bang_, type_) : conParams) = + case type_ of + -- if the current component is a variable identifier + -- then treat it as a single name binder (see 'Foil.NameBinder') + PeelConT tyName _tyParams | tyName == nameT -> do + l <- newName ("n" <> show i) + let type' = AppT (AppT (ConT ''Foil.NameBinder) (VarT p)) (VarT l) + (l', conParams') <- toPatternConParams (i+1) l conParams + return (l', (bang_, type') : conParams') + -- if the current component is a raw pattern + -- then convert it into a scope-safe pattern + PeelConT tyName tyParams | tyName == patternT -> do + l <- newName ("n" <> show i) + let type' = PeelConT foilPatternT (tyParams ++ [VarT p, VarT l]) + (l', conParams') <- toPatternConParams (i+1) l conParams + return (l', (bang_, type') : conParams') + -- otherwise, ignore the component as non-binding + _ -> do + (l, conParams') <- toPatternConParams (i+1) p conParams + return (l, param : conParams') + + -- | Convert a constructor declaration for a raw scoped term + -- into a constructor for the scope-safe scoped term. + toScopeCon :: [TyVarBndr BndrVis] -> Name -> Con -> Con + toScopeCon _tvars n (NormalC conName params) = + NormalC foilConName (map toScopeParam params) + where + foilConName = mkName ("Foil" ++ nameBase conName) + toScopeParam (_bang, PeelConT tyName tyParams) + | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n])) + toScopeParam _bangType = _bangType + + -- | Convert a constructor declaration for a raw term + -- into a constructor for the scope-safe term. + toTermCon :: [TyVarBndr BndrVis] -> Name -> Name -> Con -> Con + toTermCon tvars n l (NormalC conName params) = + GadtC [foilConName] (map toTermParam params) (PeelConT foilTermT (map (VarT . tvarName) tvars ++ [VarT n])) + where + foilNames = [n, l] + foilConName = mkName ("Foil" ++ nameBase conName) + toTermParam (_bang, PeelConT tyName tyParams) + | tyName == patternT = (_bang, PeelConT foilPatternT (tyParams ++ map VarT foilNames)) + | tyName == nameT = (_bang, AppT (ConT ''Foil.Name) (VarT n)) + | tyName == scopeT = (_bang, PeelConT foilScopeT (tyParams ++ [VarT l])) + | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n])) + toTermParam _bangType = _bangType diff --git a/src/Control/Monad/Foil/TH/MkFromFoil.hs b/src/Control/Monad/Foil/TH/MkFromFoil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH/MkFromFoil.hs @@ -0,0 +1,232 @@ +{-# OPTIONS_GHC -fno-warn-type-defaults #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskellQuotes #-} +module Control.Monad.Foil.TH.MkFromFoil (mkFromFoil) where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax (addModFinalizer) + +import qualified Control.Monad.Foil as Foil +import Control.Monad.Foil.TH.Util + +-- | Generate conversion functions from raw to scope-safe representation. +mkFromFoil + :: Name -- ^ Type name for raw terms. + -> Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw scoped terms. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkFromFoil termT nameT scopeT patternT = do + n <- newName "n" + let ntype = return (VarT n) + l <- newName "l" + let ltype = return (VarT l) + r <- newName "r" + let rtype = return (VarT r) + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT + TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT + + let termParams = map (VarT . tvarName) termTVars + let scopeParams = map (VarT . tvarName) scopeTVars + let patternParams = map (VarT . tvarName) patternTVars + + fromFoilTermSignature <- + SigD fromFoilTermT <$> + [t| [$(return (ConT nameT))] + -> Foil.NameMap $ntype $(return (ConT nameT)) + -> $(return (PeelConT foilTermT termParams)) $ntype + -> $(return (PeelConT termT termParams)) + |] + fromFoilScopedSignature <- + SigD fromFoilScopedT <$> + [t| [$(return (ConT nameT))] + -> Foil.NameMap $ntype $(return (ConT nameT)) + -> $(return (PeelConT foilScopeT scopeParams)) $ntype + -> $(return (PeelConT scopeT scopeParams)) + |] + fromFoilPatternSignature <- + SigD fromFoilPatternT <$> + [t| [$(return (ConT nameT))] + -> Foil.NameMap $ntype $(return (ConT nameT)) + -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype + -> ([$(return (ConT nameT))] -> Foil.NameMap $ltype $(return (ConT nameT)) -> $(return (PeelConT patternT patternParams)) -> $rtype) + -> $rtype + |] + + addModFinalizer $ putDoc (DeclDoc fromFoilTermT) + "Convert a scope-safe term into a raw term." + addModFinalizer $ putDoc (DeclDoc fromFoilPatternT) + "Convert a scope-safe pattern into a raw pattern." + addModFinalizer $ putDoc (DeclDoc fromFoilScopedT) + "Convert a scope-safe scoped term into a raw scoped term." + + return + [ fromFoilTermSignature + , fromFoilTermBody termCons + , fromFoilPatternSignature + , fromFoilPatternBody patternCons + , fromFoilScopedSignature + , fromFoilScopedBody scopeCons + ] + where + foilTermT = mkName ("Foil" ++ nameBase termT) + foilScopeT = mkName ("Foil" ++ nameBase scopeT) + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + fromFoilTermT = mkName ("fromFoil" ++ nameBase termT) + fromFoilPatternT = mkName ("fromFoil" ++ nameBase patternT) + fromFoilScopedT = mkName ("fromFoil" ++ nameBase scopeT) + + fromFoilTermBody termCons = FunD fromFoilTermT + [Clause [VarP freshVars, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch termCons))) []] + where + freshVars = mkName "freshVars" + env = mkName "env" + term = mkName "term" + + toMatch (NormalC conName params) = + Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) [] + where + conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params + + go _i _freshVars' _env' p [] = p + go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams + | tyName == termT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilTermT) (VarE freshVars)) (VarE env)) (VarE xi))) conParams + | tyName == scopeT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilScopedT) freshVars') env') (VarE xi))) conParams + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi)) + (LamE [VarP freshVarsi, VarP envi, VarP xi'] + (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams)) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + freshVarsi = mkName ("freshVars" <> show i) + envi = mkName ("env" <> show i) + go i freshVars' env' p (_ : conParams) = + go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ty i = mkName ("x" <> show i) + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + + fromFoilPatternBody patternCons = FunD fromFoilPatternT + [Clause [VarP freshVars, VarP env, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []] + where + freshVars = mkName "freshVars" + env = mkName "env" + pattern = mkName "pattern" + cont = mkName "cont" + + toMatch (NormalC conName params) = + Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) [] + where + conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params + + go _i freshVars' env' p [] = AppE (AppE (AppE (VarE cont) freshVars') env') p + go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + CaseE freshVars' + [ Match (ListP []) (NormalB (AppE (VarE 'error) (LitE (StringL "not enough fresh variables")))) [] + , Match (InfixP (VarP var) '(:) (VarP vars)) + (NormalB (LetE + [ValD (VarP envi) (NormalB (AppE (AppE (AppE (VarE 'Foil.addNameBinder) (VarE xi)) (VarE var)) env')) []] + (go (i + 1) (VarE vars) (VarE envi) (AppE p (VarE var)) conParams))) + [] + ] + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi)) + (LamE [VarP freshVarsi, VarP envi, VarP xi'] + (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams)) + where + var = mkName "var" + vars = mkName "vars" + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + freshVarsi = mkName ("freshVars" <> show i) + envi = mkName ("env" <> show i) + go i freshVars' env' p (_ : conParams) = + go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ i = mkName ("x" <> show i) + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + + fromFoilScopedBody freshVarsCons = FunD fromFoilScopedT + [Clause [VarP freshVars, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch freshVarsCons))) []] + where + freshVars = mkName "freshVars" + env = mkName "env" + term = mkName "term" + + toMatch (NormalC conName params) = + Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) [] + where + conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params + + go _i _freshVars' _env' p [] = p + go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams + | tyName == termT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilTermT) (VarE freshVars)) (VarE env)) (VarE xi))) conParams + | tyName == scopeT = + go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilScopedT) freshVars') env') (VarE xi))) conParams + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi)) + (LamE [VarP freshVarsi, VarP envi, VarP xi'] + (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams)) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + freshVarsi = mkName ("freshVars" <> show i) + envi = mkName ("env" <> show i) + go i freshVars' env' p (_ : conParams) = + go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ty i = mkName ("x" <> show i) + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" diff --git a/src/Control/Monad/Foil/TH/MkInstancesFoil.hs b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskellQuotes #-} +{-# OPTIONS_GHC -fno-warn-type-defaults #-} +module Control.Monad.Foil.TH.MkInstancesFoil (mkInstancesFoil) where + +import Language.Haskell.TH + +import qualified Control.Monad.Foil as Foil +import Control.Monad.Foil.TH.Util + +-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances. +mkInstancesFoil + :: Name -- ^ Type name for raw terms. + -> Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw scoped terms. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkInstancesFoil termT nameT scopeT patternT = do + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT + TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT + + return + [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars))) + [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ] + + , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) + [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons) ] + + , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars))) + [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)] + ] + + where + foilTermT = mkName ("Foil" ++ nameBase termT) + foilScopeT = mkName ("Foil" ++ nameBase scopeT) + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + clauseScopedTerm :: Con -> Clause + clauseScopedTerm = clauseTerm + + clauseTerm :: Con -> Clause + clauseTerm RecC{} = error "Record constructors (RecC) are not supported yet!" + clauseTerm InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + clauseTerm ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + clauseTerm GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + clauseTerm RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + clauseTerm (NormalC conName params) = + Clause + [VarP rename, ConP foilConName [] conParamPatterns] + (NormalB (go 1 (VarE rename) (ConE foilConName) params)) + [] + where + foilConName = mkName ("Foil" ++ nameBase conName) + rename = mkName "rename" + conParamPatterns = zipWith mkConParamPattern params [1..] + mkConParamPattern _ i = VarP (mkName ("x" ++ show i)) + + go _i _rename' p [] = p + go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + go (i + 1) rename' (AppE p (AppE (VarE rename) (VarE xi))) conParams + | tyName == termT = + go (i + 1) rename' (AppE p (AppE (AppE (VarE 'Foil.sinkabilityProof) (VarE rename)) (VarE xi))) conParams + | tyName == scopeT = + go (i + 1) rename' (AppE p (AppE (AppE (VarE 'Foil.sinkabilityProof) rename') (VarE xi))) conParams + | tyName == patternT = + AppE + (AppE (AppE (VarE 'Foil.coSinkabilityProof) rename') (VarE xi)) + (LamE [VarP renamei, VarP xi'] + (go (i + 1) (VarE renamei) (AppE p (VarE xi')) conParams)) + where + xi = mkName ("x" ++ show i) + xi' = mkName ("x" ++ show i ++ "'") + renamei = mkName ("rename" ++ show i) + go i rename' p (_ : conPatterns) = + go (i + 1) rename' (AppE p (VarE xi)) conPatterns + where + xi = mkName ("x" ++ show i) + + clausePattern :: Con -> Clause + clausePattern RecC{} = error "Record constructors (RecC) are not supported yet!" + clausePattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + clausePattern ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + clausePattern GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + clausePattern RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + clausePattern (NormalC conName params) = + Clause + [VarP rename, ConP foilConName [] conParamPatterns, VarP cont] + (NormalB (go 1 (VarE rename) (ConE foilConName) params)) + [] + where + foilConName = mkName ("Foil" ++ nameBase conName) + rename = mkName "rename" + cont = mkName "cont" + conParamPatterns = zipWith mkConParamPattern params [1..] + mkConParamPattern _ i = VarP (mkName ("x" ++ show i)) + + go _i rename' p [] = AppE (AppE (VarE cont) rename') p + go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT || tyName == patternT = + AppE + (AppE (AppE (VarE 'Foil.coSinkabilityProof) rename') (VarE xi)) + (LamE [VarP renamei, VarP xi'] + (go (i + 1) (VarE renamei) (AppE p (VarE xi')) conParams)) + where + xi = mkName ("x" ++ show i) + xi' = mkName ("x" ++ show i ++ "'") + renamei = mkName ("rename" ++ show i) + go i rename' p (_ : conPatterns) = + go (i + 1) rename' (AppE p (VarE xi)) conPatterns + where + xi = mkName ("x" ++ show i) diff --git a/src/Control/Monad/Foil/TH/MkToFoil.hs b/src/Control/Monad/Foil/TH/MkToFoil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH/MkToFoil.hs @@ -0,0 +1,458 @@ +{-# OPTIONS_GHC -fno-warn-type-defaults #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskellQuotes #-} +module Control.Monad.Foil.TH.MkToFoil (mkToFoil) where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax (addModFinalizer) + +import qualified Control.Monad.Foil as Foil +import Data.Maybe (catMaybes) +import Data.Map (Map) +import qualified Data.Map as Map +import Control.Monad.Foil.TH.Util + +-- | Generate conversion functions from raw to scope-safe representation. +mkToFoil + :: Name -- ^ Type name for raw terms. + -> Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw scoped terms. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkToFoil termT nameT scopeT patternT = do + extendScopeFoilPattenD <- mkExtendScopeFoilPattern nameT patternT + withRefreshedFoilPatternD <- mkWithRefreshedFoilPattern nameT patternT + toFoilTermD <- mkToFoilTerm termT nameT scopeT patternT + return ( + extendScopeFoilPattenD ++ + withRefreshedFoilPatternD ++ + toFoilTermD + ) + +-- | Generate a function to extend scope with variables from a given pattern. +mkExtendScopeFoilPattern + :: Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkExtendScopeFoilPattern nameT patternT = do + n <- newName "n" + l <- newName "l" + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + + let extendScopePatternSignature = + SigD extendScopePatternFunName $ + ForallT ([ PlainTV name SpecifiedSpec | name <- (map tvarName patternTVars ++ [n, l]) ]) [] + (AppT (AppT ArrowT + (PeelConT foilPatternT [ VarT name | name <- (map tvarName patternTVars ++ [n, l]) ])) + (AppT (AppT ArrowT + (AppT (ConT ''Foil.Scope) (VarT n))) + (AppT (ConT ''Foil.Scope) (VarT l)))) + + composefun <- [e| (.) |] + idfun <- [e| id |] + extendScopeFun <- [e| Foil.extendScope |] + + addModFinalizer $ putDoc (DeclDoc extendScopePatternFunName) + "Extend a scope with the names bound by the given pattern.\nThis is a more flexible version of 'Control.Monad.Foil.extendScope'." + + return + [ extendScopePatternSignature + , extendScopePatternBody extendScopeFun composefun idfun patternCons + ] + where + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT) + extendScopePatternBody extendScopeFun composefun idfun patternCons = FunD extendScopePatternFunName + [Clause [VarP p] (NormalB (CaseE (VarE p) (map toMatch patternCons))) []] + where + p = mkName "pattern" + toMatch (NormalC conName conParams) = + Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) [] + where + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map toConParamPattern conParamVars + conMatchExts = map snd (catMaybes conParamVars) + conMatchBody = foldr (\f g -> InfixE (Just g) composefun (Just f)) idfun conMatchExts + + toConParamPattern Nothing = WildP + toConParamPattern (Just (x, _f)) = VarP x + + conParamVars = zipWith mkConParamVar conParams [1..] + + mkConParamVar :: BangType -> Int -> Maybe (Name, Exp) + mkConParamVar (_bang, PeelConT tyName _tyParams) i + | tyName == nameT = Just (x, AppE extendScopeFun (VarE x)) + | tyName == patternT = Just (x, AppE (VarE extendScopePatternFunName) (VarE x)) + where + x = mkName ("x" <> show i) + mkConParamVar (_bang, _type) _i = Nothing + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + +-- | Generate a function to extend scope with variables from a given pattern. +mkWithRefreshedFoilPattern + :: Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkWithRefreshedFoilPattern nameT patternT = do + o <- newName "o" + o' <- newName "o'" + e <- newName "e" + n <- newName "n" + l <- newName "l" + r <- newName "r" + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + + let withRefreshedFoilPatternSignature = + SigD withRefreshedFoilPatternFunName $ + ForallT + [ PlainTV name SpecifiedSpec | name <- map tvarName patternTVars ++ [o, e, n, l, r] ] + [ AppT (ConT ''Foil.Distinct) (VarT o) + , AppT (ConT ''Foil.InjectName) (VarT e) + , AppT (ConT ''Foil.Sinkable) (VarT e) + ] + (AppT (AppT ArrowT (PeelConT ''Foil.Scope [VarT o])) + (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT n, VarT l]))) + (AppT (AppT ArrowT + (ForallT [PlainTV o' SpecifiedSpec] [PeelConT ''Foil.DExt [VarT o, VarT o']] + (AppT (AppT ArrowT (AppT (AppT ArrowT (PeelConT ''Foil.Substitution [VarT e, VarT n, VarT o])) (PeelConT ''Foil.Substitution [VarT e, VarT l, VarT o']))) + (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT o, VarT o']))) + (VarT r))))) + (VarT r)))) + + -- [t| ( Foil.Distinct o, Foil.InjectName e, Foil.Sinkable e ) + -- => Foil.Scope o + -- -> $(return (PeelConT foilPatternT (map (VarT . tyName patternTVars)))) n l + -- -> (forall o'. Foil.DExt o o' + -- => (Foil.Substitution e n o -> Foil.Substitution e l o') + -- -> $(return (ConT foilPatternT)) o o' + -- -> r) + -- -> r + -- |] + + composefun <- [e| (.) |] + addRenameFun <- [e| Foil.addRename |] + nameOfFun <- [e| Foil.nameOf |] + sinkFun <- [e| Foil.sink |] + withRefreshedFun <- [e| Foil.withRefreshed |] + extendScopeFun <- [e| Foil.extendScope |] + + addModFinalizer $ putDoc (DeclDoc withRefreshedFoilPatternFunName) + "Refresh (if needed) bound variables introduced in a pattern.\nThis is a more flexible version of 'Control.Monad.Foil.withRefreshed'." + + return + [ withRefreshedFoilPatternSignature + , withRefreshedFoilPatternBody composefun addRenameFun nameOfFun sinkFun withRefreshedFun extendScopeFun patternCons + ] + where + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT) + extendScopePatternFun = VarE extendScopePatternFunName + + withRefreshedFoilPatternFunName = mkName ("withRefreshedFoil" ++ nameBase patternT) + withRefreshedFoilPatternFun = VarE withRefreshedFoilPatternFunName + + withRefreshedFoilPatternBody composefun addRenameFun nameOfFun sinkFun withRefreshedFun extendScopeFun patternCons = FunD withRefreshedFoilPatternFunName + [Clause [VarP scope, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []] + where + scope = mkName "scope" + pattern = mkName "pattern" + cont = mkName "cont" + + toMatch (NormalC conName params) = + Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) [] + where + conMatchBody = go 1 (VarE scope) sinkFun (ConE foilConName) params + + go _i _scope' f p [] = AppE (AppE (VarE cont) f) p + go i scope' f p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + AppE + (AppE (AppE withRefreshedFun scope') (AppE nameOfFun (VarE xi))) + (LamE [VarP xi'] + (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopeFun (VarE xi')) scope')) []] + (go (i+1) (VarE scopei) (InfixE (Just fi) composefun (Just f)) (AppE p (VarE xi')) conParams))) + | tyName == patternT = + AppE + (AppE (AppE withRefreshedFoilPatternFun scope') (VarE xi)) + (LamE [VarP xsubst, VarP xi'] + (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []] + (go (i+1) (VarE scopei) (InfixE (Just (VarE xsubst)) composefun (Just f)) (AppE p (VarE xi')) conParams))) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + scopei = mkName ("scope" <> show i) + xsubst = mkName ("subst" <> show i) + subst = mkName "subst" + fi = LamE [VarP subst] + (AppE (AppE (AppE addRenameFun + (VarE subst)) + (VarE xi)) + (AppE nameOfFun (VarE xi'))) + go i scope' f p (_ : conParams) = + go (i + 1) scope' f (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ i = mkName ("x" <> show i) + + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + +-- | Generate a conversion function from raw terms to scope-safe terms. +mkToFoilTerm + :: Name -- ^ Type name for raw terms. + -> Name -- ^ Type name for raw variable identifiers. + -> Name -- ^ Type name for raw scoped terms. + -> Name -- ^ Type name for raw patterns. + -> Q [Dec] +mkToFoilTerm termT nameT scopeT patternT = do + n <- newName "n" + let ntype = return (VarT n) + r <- newName "r" + let rtype = return (VarT r) + TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT + TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT + TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT + + toFoilTermSignature <- + SigD toFoilTermT <$> + [t| Foil.Distinct $ntype + => Foil.Scope $ntype + -> Map $(return (ConT nameT)) (Foil.Name $ntype) + -> $(return (PeelConT termT (map (VarT . tvarName) termTVars ))) + -> $(return (PeelConT foilTermT (map (VarT . tvarName) termTVars))) $ntype + |] + toFoilScopedSignature <- + SigD toFoilScopedT <$> + [t| Foil.Distinct $ntype + => Foil.Scope $ntype + -> Map $(return (ConT nameT)) (Foil.Name $ntype) + -> $(return (PeelConT scopeT (map (VarT . tvarName) scopeTVars))) + -> $(return (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars))) $ntype + |] + toFoilPatternSignature <- + SigD toFoilPatternT <$> + [t| Foil.Distinct $ntype + => Foil.Scope $ntype + -> Map $(return (ConT nameT)) (Foil.Name $ntype) + -> $(return (PeelConT patternT (map (VarT . tvarName) patternTVars))) + -> (forall l. Foil.DExt $ntype l => $(return (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) $ntype l -> Map $(return (ConT nameT)) (Foil.Name l) -> $rtype) + -> $rtype + |] + + addModFinalizer $ putDoc (DeclDoc toFoilTermT) + "Convert a raw term into a scope-safe term." + addModFinalizer $ putDoc (DeclDoc toFoilPatternT) + "Convert a raw pattern into a scope-safe pattern." + addModFinalizer $ putDoc (DeclDoc toFoilScopedT) + "Convert a raw scoped term into a scope-safe scoped term." + + return + [ toFoilTermSignature + , toFoilTermBody termCons + , toFoilPatternSignature + , toFoilPatternBody patternCons + , toFoilScopedSignature + , toFoilScopedBody scopeCons + ] + where + foilTermT = mkName ("Foil" ++ nameBase termT) + foilScopeT = mkName ("Foil" ++ nameBase scopeT) + foilPatternT = mkName ("Foil" ++ nameBase patternT) + + toFoilTermT = mkName ("toFoil" ++ nameBase termT) + toFoilPatternT = mkName ("toFoil" ++ nameBase patternT) + toFoilScopedT = mkName ("toFoil" ++ nameBase scopeT) + + extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT) + extendScopePatternFun = VarE extendScopePatternFunName + + toFoilTermBody termCons = FunD toFoilTermT + [Clause [VarP scope, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch termCons))) []] + where + scope = mkName "scope" + env = mkName "env" + term = mkName "term" + + toMatch (NormalC conName params) = + Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD] + where + toFoilVarFunName = mkName "lookupRawVar" + toFoilVarFun = VarE toFoilVarFunName + x = mkName "x" + name = mkName "name" + toFoilVarD = FunD toFoilVarFunName [Clause [VarP x] + (NormalB (CaseE (AppE (AppE (VarE 'Map.lookup) (VarE x)) (VarE env)) + [ Match (ConP 'Just [] [VarP name]) (NormalB (VarE name)) [] + , Match (ConP 'Nothing [] []) (NormalB (AppE (VarE 'error) (LitE (StringL "undefined variable")))) []])) + []] + + conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params + + go _i _scope' _env' p [] = p + go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams + | tyName == termT = + go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilTermT) (VarE scope)) (VarE env)) (VarE xi))) conParams + | tyName == scopeT = + go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilScopedT) scope') env') (VarE xi))) conParams + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi)) + (LamE [VarP xi', VarP envi] + (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []] + (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams))) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + scopei = mkName ("scope" <> show i) + envi = mkName ("env" <> show i) + go i scope' env' p (_ : conParams) = + go (i + 1) scope' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ty i = mkName ("x" <> show i) + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + + toFoilPatternBody patternCons = FunD toFoilPatternT + [Clause [VarP scope, VarP env, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []] + where + scope = mkName "scope" + env = mkName "env" + pattern = mkName "pattern" + cont = mkName "cont" + + toMatch (NormalC conName params) = + Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [] + where + conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params + + go _i _scope' env' p [] = AppE (AppE (VarE cont) p) env' + go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + AppE (AppE (VarE 'Foil.withFresh) scope') + (LamE [VarP xi'] + (LetE [ ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScope) (VarE xi')) scope')) [] + , ValD (VarP envi) (NormalB + (AppE (AppE (AppE (VarE 'Map.insert) (VarE xi)) + (AppE (VarE 'Foil.nameOf) (VarE xi'))) + (InfixE (Just (VarE 'Foil.sink)) (VarE '(<$>)) (Just (VarE envi))))) []] + (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams))) + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi)) + (LamE [VarP xi', VarP envi] + (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []] + (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams))) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + scopei = mkName ("scope" <> show i) + envi = mkName ("env" <> show i) + go i scope' env' p (_ : conParams) = + go (i + 1) scope' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ i = mkName ("x" <> show i) + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" + + toFoilScopedBody scopeCons = FunD toFoilScopedT + [Clause [VarP scope, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch scopeCons))) []] + where + scope = mkName "scope" + env = mkName "env" + term = mkName "term" + + toMatch (NormalC conName params) = + Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD] + where + toFoilVarFunName = mkName "lookupRawVar" + toFoilVarFun = VarE toFoilVarFunName + x = mkName "x" + name = mkName "name" + toFoilVarD = FunD toFoilVarFunName [Clause [VarP x] + (NormalB (CaseE (AppE (AppE (VarE 'Map.lookup) (VarE x)) (VarE env)) + [ Match (ConP 'Just [] [VarP name]) (NormalB (VarE name)) [] + , Match (ConP 'Nothing [] []) (NormalB (AppE (VarE 'error) (LitE (StringL "undefined variable")))) []])) + []] + + conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params + + go _i _scope' _env' p [] = p + go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams) + | tyName == nameT = + go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams + | tyName == termT = + go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilTermT) (VarE scope)) (VarE env)) (VarE xi))) conParams + | tyName == scopeT = + go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilScopedT) scope') env') (VarE xi))) conParams + | tyName == patternT = + AppE + (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi)) + (LamE [VarP xi', VarP envi] + (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []] + (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams))) + where + xi = mkName ("x" <> show i) + xi' = mkName ("x" <> show i <> "'") + scopei = mkName ("scope" <> show i) + envi = mkName ("env" <> show i) + go i scope' env' p (_ : conParams) = + go (i + 1) scope' env' (AppE p (VarE xi)) conParams + where + xi = mkName ("x" <> show i) + + foilConName = mkName ("Foil" ++ nameBase conName) + conParamPatterns = map VarP conParamVars + + conParamVars = zipWith mkConParamVar params [1..] + + mkConParamVar :: BangType -> Int -> Name + mkConParamVar _ty i = mkName ("x" <> show i) + + toMatch RecC{} = error "Record constructors (RecC) are not supported yet!" + toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!" + toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!" + toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!" + toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!" diff --git a/src/Control/Monad/Foil/TH/Util.hs b/src/Control/Monad/Foil/TH/Util.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Foil/TH/Util.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} +module Control.Monad.Foil.TH.Util where + +import Language.Haskell.TH + +peelConT :: Type -> Maybe (Name, [Type]) +peelConT (ConT name) = Just (name, []) +peelConT (AppT f x) = + case peelConT f of + Just (g, xs) -> Just (g, xs ++ [x]) + Nothing -> Nothing +peelConT _ = Nothing + +unpeelConT :: Name -> [Type] -> Type +unpeelConT = foldl AppT . ConT + +pattern PeelConT :: Name -> [Type] -> Type +pattern PeelConT name types <- (peelConT -> Just (name, types)) where + PeelConT name types = unpeelConT name types + +tvarName :: TyVarBndr a -> Name +tvarName = \case + PlainTV name _ -> name + KindedTV name _ _ -> name diff --git a/src/Control/Monad/Free/Foil.hs b/src/Control/Monad/Free/Foil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Free/Foil.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +-- | This module defines a variation of +-- free scoped (relative) monads relying on the foil for +-- the scope-safe efficient handling of the binders. +-- +-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384). +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.Bifunctor +import GHC.Generics (Generic) + +-- | Scoped term under a (single) name binder. +data ScopedAST sig n where + ScopedAST :: Foil.NameBinder n l -> AST sig l -> ScopedAST sig n + +instance (forall l. NFData (AST sig l)) => NFData (ScopedAST sig n) where + rnf (ScopedAST binder body) = rnf binder `seq` rnf body + +-- | A term, generated by a signature 'Bifunctor' @sig@, +-- with (free) variables in scope @n@. +data AST sig n where + -- | A (free) variable in scope @n@. + Var :: Foil.Name n -> AST sig n + -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@. + Node :: sig (ScopedAST sig n) (AST sig n) -> AST sig n + +deriving instance Generic (AST sig n) +deriving instance (forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST sig n) + +instance Bifunctor sig => Foil.Sinkable (AST sig) where + sinkabilityProof rename = \case + Var name -> Var (rename name) + Node node -> Node (bimap f (Foil.sinkabilityProof rename) node) + where + f (ScopedAST binder body) = + Foil.extendRenaming rename binder $ \rename' binder' -> + ScopedAST binder' (Foil.sinkabilityProof rename' body) + +instance Foil.InjectName (AST sig) where + injectName = Var + +-- | Substitution for free (scoped monads). +substitute + :: (Bifunctor sig, Foil.Distinct o) + => Foil.Scope o + -> Foil.Substitution (AST sig) i o + -> AST sig i + -> AST sig o +substitute scope subst = \case + Var name -> Foil.lookupSubst subst name + Node node -> Node (bimap f (substitute scope subst) node) + where + f (ScopedAST binder body) = + Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' -> + let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder') + scope' = Foil.extendScope binder' scope + body' = substitute 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 + rbind scope term subst = + case term of + Var name -> subst name + Node node -> Node (bimap g' g node) + where + g x = Foil.rbind scope x subst + g' (ScopedAST binder body) = + Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' -> + let scope' = Foil.extendScope binder' scope + subst' name = case Foil.unsinkName binder name of + Nothing -> Foil.rreturn (Foil.nameOf binder') + Just n -> Foil.sink (subst n) + in ScopedAST binder' (Foil.rbind scope' body subst') diff --git a/src/Control/Monad/Free/Foil/Example.hs b/src/Control/Monad/Free/Foil/Example.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Free/Foil/Example.hs @@ -0,0 +1,125 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +-- | Example implementation of untyped \(\lambda\)-calculus with the foil. +module Control.Monad.Free.Foil.Example where + +import Control.Monad.Foil +import Control.Monad.Free.Foil +import Data.Bifunctor.TH + +-- $setup +-- >>> import Control.Monad.Foil + +-- | Untyped \(\lambda\)-terms in scope @n@. +data ExprF scope term + -- | Application of one term to another: \((t_1, t_2)\) + = AppF term term + -- | \(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\) + | LamF scope + deriving (Functor) +deriveBifunctor ''ExprF + +pattern AppE :: AST ExprF n -> AST ExprF n -> AST ExprF n +pattern AppE x y = Node (AppF x y) + +pattern LamE :: NameBinder n l -> AST ExprF l -> AST ExprF n +pattern LamE binder body = Node (LamF (ScopedAST binder body)) + +{-# COMPLETE Var, AppE, LamE #-} + +type Expr = AST ExprF + +-- | Use 'ppExpr' to show \(\lambda\)-terms. +instance Show (Expr n) where + show = ppExpr + +-- | Compute weak head normal form (WHNF) of a \(\lambda\)-term. +-- +-- >>> whnf emptyScope (AppE (churchN 2) (churchN 2)) +-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1)) +whnf :: Distinct n => Scope n -> Expr n -> Expr n +whnf scope = \case + AppE fun arg -> + case whnf scope fun of + LamE binder body -> + let subst = addSubst identitySubst binder arg + in whnf scope (substitute scope subst body) + fun' -> AppE fun' arg + t -> t + +-- | Compute weak head normal form (WHNF) of a __closed__ \(\lambda\)-term. +-- +-- >>> whnf' (AppE (churchN 2) (churchN 2)) +-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1)) +whnf' :: Expr VoidS -> Expr VoidS +whnf' = whnf emptyScope + +-- | Compute normal form (NF) of a \(\lambda\)-term. +-- +-- >>> nf emptyScope (AppE (churchN 2) (churchN 2)) +-- λx1. λx2. (x1 (x1 (x1 (x1 x2)))) +nf :: Distinct n => Scope n -> Expr n -> Expr n +nf scope expr = case expr of + LamE binder body -> + -- Instead of using 'assertDistinct', + -- another option is to add 'Distinct l' constraint + -- to the definition of 'LamE'. + case assertDistinct binder of + Distinct -> + let scope' = extendScope binder scope + in LamE binder (nf scope' body) + AppE fun arg -> + case whnf scope fun of + LamE binder body -> + let subst = addSubst identitySubst binder arg + in nf scope (substitute scope subst body) + fun' -> AppE (nf scope fun') (nf scope arg) + t -> t + +-- | Compute normal form (NF) of a __closed__ \(\lambda\)-term. +-- +-- >>> nf' (AppE (churchN 2) (churchN 2)) +-- λx1. λx2. (x1 (x1 (x1 (x1 x2)))) +nf' :: Expr VoidS -> Expr VoidS +nf' = nf emptyScope + +-- | Pretty print a name. +ppName :: Name n -> String +ppName name = "x" <> show (nameId name) + +-- | Pretty-print a \(\lambda\)-term. +-- +-- >>> ppExpr (churchN 3) +-- "\955x0. \955x1. (x0 (x0 (x0 x1)))" +ppExpr :: Expr n -> String +ppExpr = \case + Var name -> ppName name + AppE x y -> "(" <> ppExpr x <> " " <> ppExpr y <> ")" + LamE binder body -> "λ" <> ppName (nameOf binder) <> ". " <> ppExpr body + +-- | A helper for constructing \(\lambda\)-abstractions. +lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n +lam scope mkBody = withFresh scope $ \x -> + let scope' = extendScope x scope + in LamE x (mkBody scope' x) + +-- | Church-encoding of a natural number \(n\). +-- +-- >>> churchN 0 +-- λx0. λx1. x1 +-- +-- >>> churchN 3 +-- λx0. λx1. (x0 (x0 (x0 x1))) +churchN :: Int -> Expr VoidS +churchN n = + lam emptyScope $ \sx nx -> + lam sx $ \_sxy ny -> + let x = sink (Var (nameOf nx)) + y = Var (nameOf ny) + in iterate (AppE x) y !! n diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,2 @@ +main :: IO () +main = putStrLn "Test suite not yet implemented" diff --git a/test/doctests/Main.hs b/test/doctests/Main.hs new file mode 100644 --- /dev/null +++ b/test/doctests/Main.hs @@ -0,0 +1,7 @@ +module Main where + +import System.Environment (getArgs) +import Test.DocTest (mainFromCabal) + +main :: IO () +main = mainFromCabal "free-foil" =<< getArgs