Safe Haskell | None |
---|---|
Language | Haskell2010 |
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».
This module also introduces CoSinkable
class,
generalizing handling of patterns, as described in
«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax».
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).
Synopsis
- data S = VoidS
- newtype Scope (n :: S) = UnsafeScope RawScope
- newtype Name (n :: S) = UnsafeName RawName
- newtype NameBinder (n :: S) (l :: S) = UnsafeNameBinder (Name l)
- emptyScope :: Scope 'VoidS
- extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
- member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool
- nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l
- nameId :: forall (l :: S). Name l -> Id
- withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r
- data DistinctEvidence (n :: S) where
- Distinct :: forall (n :: S). Distinct n => DistinctEvidence n
- unsafeDistinct :: forall (n :: S). DistinctEvidence n
- data ExtEvidence (n :: S) (l :: S) where
- Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l
- unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l
- withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
- unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r. NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
- assertDistinct :: forall (n :: S) (l :: S). Distinct n => NameBinder n l -> DistinctEvidence l
- assertExt :: forall (n :: S) (l :: S). NameBinder n l -> ExtEvidence n l
- withRefreshed :: forall (o :: S) (i :: S) r. Distinct o => Scope o -> Name i -> (forall (o' :: S). DExt o o' => NameBinder o o' -> r) -> r
- unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n)
- data UnifyNameBinders (n :: S) (l :: S) (r :: S) where
- SameNameBinders :: forall (n :: S) (l :: S). UnifyNameBinders n l l
- RenameLeftNameBinder :: forall (n :: S) (l :: S) (r :: S). (NameBinder n l -> NameBinder n r) -> UnifyNameBinders n l r
- RenameRightNameBinder :: forall (n :: S) (r :: S) (l :: S). (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r
- unifyNameBinders :: forall (i :: S) (l :: S) (r :: S). NameBinder i l -> NameBinder i r -> UnifyNameBinders i l r
- class Sinkable (e :: S -> Type) where
- sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> e n -> e l
- sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l
- extendRenaming :: forall pattern (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern => (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r
- extendNameBinderRenaming :: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern => (NameBinder i n -> NameBinder i n') -> pattern n l -> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r) -> r
- composeNameBinderRenamings :: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i') -> (NameBinder i' l -> NameBinder i' l') -> NameBinder n l -> NameBinder n l'
- fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S). (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
- extendRenamingNameBinder :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r
- class CoSinkable (pattern :: S -> S -> Type) where
- newtype Substitution (e :: S -> Type) (i :: S) (o :: S) = UnsafeSubstitution (IntMap (e o))
- lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o
- identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i
- addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
- addRename :: forall (e :: S -> Type) (i :: S) (o :: S) (i' :: S). InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o
- newtype NameMap (n :: S) a = NameMap {
- getNameMap :: IntMap a
- emptyNameMap :: NameMap 'VoidS a
- lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a
- addNameBinder :: forall (n :: S) (l :: S) a. NameBinder n l -> a -> NameMap n a -> NameMap l a
- type Id = Int
- type RawName = Id
- type RawScope = IntSet
- rawFreshName :: RawScope -> RawName
- rawMember :: RawName -> RawScope -> Bool
- class ExtEndo (n :: S)
- class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S)
- class Distinct (n :: S)
- type DExt (n :: S) (l :: S) = (Distinct l, Ext n l)
- class InjectName (e :: S -> Type) where
- injectName :: forall (n :: S). Name n -> e n
Safe types and operations
S
is a data kind of scope indices.
VoidS |
|
newtype Name (n :: S) Source #
A name in a safe scope, indexed by a type-level scope index n
.
Instances
Sinkable Name Source # | Sinking a |
Defined in Control.Monad.Foil.Internal | |
RelMonad Name Expr Source # | |
Bifunctor sig => RelMonad Name (AST sig) Source # | |
Show (Name n) Source # | |
NFData (Name n) Source # | |
Defined in Control.Monad.Foil.Internal | |
Eq (Name n) Source # | |
Ord (Name n) Source # | |
newtype NameBinder (n :: S) (l :: S) Source #
A name binder is a name that extends scope n
to a (larger) scope l
.
UnsafeNameBinder (Name l) |
Instances
emptyScope :: Scope 'VoidS Source #
An empty scope (without any names).
extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l Source #
\(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.
member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool Source #
A runtime check for potential name capture.
nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l Source #
Extract name from a name binder.
nameId :: forall (l :: S). Name l -> Id Source #
Convert Name
into an identifier.
This may be useful for printing and debugging.
withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r Source #
Allocate a fresh binder for a given scope.
data DistinctEvidence (n :: S) where Source #
Evidence that scope n
contains distinct names.
Distinct :: forall (n :: S). Distinct n => DistinctEvidence n |
unsafeDistinct :: forall (n :: S). DistinctEvidence n Source #
Unsafely declare that scope n
is distinct.
Used in unsafeAssertFresh
.
data ExtEvidence (n :: S) (l :: S) where Source #
Evidence that scope l
extends scope n
.
Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l |
unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l Source #
Unsafely declare that scope l
extends scope n
.
Used in unsafeAssertFresh
.
withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r Source #
Safely produce a fresh name binder with respect to a given scope.
unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r. NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r Source #
Unsafely declare that a given name (binder)
is already fresh in any scope n'
.
assertDistinct :: forall (n :: S) (l :: S). Distinct n => NameBinder n l -> DistinctEvidence l Source #
A distinct scope extended with a NameBinder
is also distinct.
assertExt :: forall (n :: S) (l :: S). NameBinder n l -> ExtEvidence n l Source #
A distinct scope extended with a NameBinder
is also distinct.
:: forall (o :: S) (i :: S) r. Distinct o | |
=> Scope o | Ambient scope. |
-> Name i | Name to refresh (if it clashes with the ambient scope). |
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r) | Continuation, accepting the refreshed name. |
-> r |
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.
unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n) Source #
Try coercing the name back to the (smaller) scope, given a binder that extends that scope.
Unification of binders
data UnifyNameBinders (n :: S) (l :: S) (r :: S) where Source #
Unification result for two binders,
extending some common scope to scopes l
and r
respectively.
Due to the implementation of the foil,
SameNameBinders :: forall (n :: S) (l :: S). UnifyNameBinders n l l | Binders are the same, proving that type parameters |
RenameLeftNameBinder :: forall (n :: S) (l :: S) (r :: S). (NameBinder n l -> NameBinder n r) -> UnifyNameBinders n l r | It is possible to safely rename the left binder to match the right one. |
RenameRightNameBinder :: forall (n :: S) (r :: S) (l :: S). (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r | It is possible to safely rename the right binder to match the left one. |
unifyNameBinders :: forall (i :: S) (l :: S) (r :: S). NameBinder i l -> NameBinder i r -> UnifyNameBinders i l r Source #
Unify binders either by asserting that they are the same, or by providing a safe renaming function to convert one binder to another.
Safe sinking
class Sinkable (e :: S -> Type) where Source #
Sinking an expression from scope n
into a (usualy extended) scope l
,
given the renaming (injection from scope n
to scope l
).
Instances
Sinkable Expr Source # | This instance serves as a proof
that sinking of |
Defined in Control.Monad.Foil.Example | |
Sinkable Name Source # | Sinking a |
Defined in Control.Monad.Foil.Internal | |
Bifunctor sig => Sinkable (AST sig) Source # | |
Defined in Control.Monad.Free.Foil | |
Sinkable e => Sinkable (Substitution e i) Source # | Substitutions are sinkable as long as corresponding expressions are. |
Defined in Control.Monad.Foil.Internal sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source # |
sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l Source #
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» for the details.
:: forall pattern (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern | |
=> (Name n -> Name n') | Map names from scope |
-> pattern n l | A pattern that extends scope |
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) | A continuation, accepting an extended renaming from |
-> r |
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
.
extendNameBinderRenaming Source #
:: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern | |
=> (NameBinder i n -> NameBinder i n') | Map names from scope |
-> pattern n l | A pattern that extends scope |
-> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r) | A continuation, accepting an extended renaming from |
-> r |
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.
composeNameBinderRenamings Source #
:: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i') | Rename binders extending scope |
-> (NameBinder i' l -> NameBinder i' l') | Rename binders extending scope |
-> NameBinder n l | |
-> NameBinder n l' |
Safely compose renamings of name binders. The underlying implementation is
fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S). (NameBinder n l -> NameBinder n l') -> Name l -> Name l' Source #
Convert renaming of name binders into renaming of names in the inner scopes.
extendRenamingNameBinder Source #
:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') | Map names from scope |
-> NameBinder n l | A name binder that extends scope |
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) | A continuation, accepting an extended renaming from |
-> r |
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» 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
).
class CoSinkable (pattern :: S -> S -> Type) where Source #
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» for more details.
:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') | Map names from scope |
-> pattern n l | A pattern that extends scope |
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) | A continuation, accepting an extended renaming from |
-> r |
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.
Instances
CoSinkable NameBinder Source # | |
Defined in Control.Monad.Foil.Internal coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r Source # |
Safe substitions
newtype Substitution (e :: S -> Type) (i :: S) (o :: S) Source #
A substitution is a mapping from names in scope i
to expressions e o
in scope o
.
UnsafeSubstitution (IntMap (e o)) |
Instances
Sinkable e => Sinkable (Substitution e i) Source # | Substitutions are sinkable as long as corresponding expressions are. |
Defined in Control.Monad.Foil.Internal sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source # |
lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o Source #
Apply substitution to a given name.
identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i Source #
Identity substitution maps all names to expresion-variables.
addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o Source #
Extend substitution with a particular mapping.
addRename :: forall (e :: S -> Type) (i :: S) (o :: S) (i' :: S). InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o Source #
Add variable renaming to a substitution. This includes the performance optimization of eliding names mapped to themselves.
Name
maps
newtype NameMap (n :: S) a Source #
A total map from names in scope n
to elements of type a
.
NameMap | |
|
emptyNameMap :: NameMap 'VoidS a Source #
An empty map belongs in the empty scope.
addNameBinder :: forall (n :: S) (l :: S) a. NameBinder n l -> a -> NameMap n a -> NameMap l a Source #
Extending a map with a single mapping.
Note that the scope parameter of the result differs from the initial map.
Raw types and operations
rawFreshName :: RawScope -> RawName Source #
\(O(\min(n, W))\). Generate a fresh raw name that does not appear in a given raw scope.
Constraints
class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S) Source #
class Distinct (n :: S) Source #
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
.
Instances
Distinct 'VoidS Source # | |
Defined in Control.Monad.Foil.Internal |
class InjectName (e :: S -> Type) where Source #
Instances of this typeclass possess the ability to inject names. Usually, this is a variable data constructor.
injectName :: forall (n :: S). Name n -> e n Source #
Inject names into expressions.
Instances
InjectName Expr Source # | |
Defined in Control.Monad.Foil.Example | |
InjectName (AST sig) Source # | |
Defined in Control.Monad.Free.Foil |