Safe Haskell	None
Language	Haskell2010

Control.Monad.Foil

Contents

Safe scopes, names, and binders
Safe (co)sinking and renaming
Safe substitutions
Unification of binders
- Eliminating impossible unification
Name maps
Constraints

Description

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». 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
data Scope (n :: S)
data Name (n :: S)
data NameBinder (n :: S) (l :: S)
emptyScope :: Scope 'VoidS
extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScopePattern :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern 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
namesOfPattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern 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
withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFreshPattern :: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r) -> r
withRefreshed :: forall (o :: S) (i :: S) r. Distinct o => Scope o -> Name i -> (forall (o' :: S). DExt o o' => NameBinder o o' -> r) -> r
withRefreshedPattern :: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r) -> r
withRefreshedPattern' :: forall pattern (o :: S) e (n :: S) (l :: S) r. (CoSinkable pattern, Distinct o, InjectName e, Sinkable e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r
unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n)
unsinkNamePattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Name l -> Maybe (Name n)
class Sinkable (e :: S -> Type) where
- sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> e n -> e l
class CoSinkable (pattern :: S -> S -> Type) where
- coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r
- withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r) -> r
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
data Substitution (e :: S -> Type) (i :: S) (o :: S)
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
data UnifyNameBinders (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S) where
- SameNameBinders :: forall (n :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n l -> UnifyNameBinders pattern n l l
- RenameLeftNameBinder :: forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n r -> (NameBinder n l -> NameBinder n r) -> UnifyNameBinders pattern n l r
- RenameRightNameBinder :: forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n l -> (NameBinder n r -> NameBinder n l) -> UnifyNameBinders pattern n l r
- RenameBothBinders :: forall (n :: S) (lr :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n lr -> (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> UnifyNameBinders pattern n l r
- NotUnifiable :: forall (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S). UnifyNameBinders pattern n l r
unifyNameBinders :: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). Distinct i => NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
andThenUnifyPatterns :: forall pattern (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') => UnifyNameBinders pattern n l l' -> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
andThenUnifyNameBinders :: forall (pattern :: S -> S -> Type) (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') => UnifyNameBinders pattern n l l' -> (NameBinder l r, NameBinder l' r') -> UnifyNameBinders pattern n r r'
class CoSinkable pattern => UnifiablePattern (pattern :: S -> S -> Type) where
- unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
class UnifiableInPattern a where
- unifyInPattern :: a -> a -> Bool
data NameBinders (n :: S) (l :: S)
emptyNameBinders :: forall (n :: S). NameBinders n n
mergeNameBinders :: forall (n :: S) (i :: S) (l :: S). NameBinders n i -> NameBinders i l -> NameBinders n l
data V2 (n :: S) (l :: S)
absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a
data NameMap (n :: S) 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
class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S)
data ExtEvidence (n :: S) (l :: S) where
- Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l
class Distinct (n :: S)
data DistinctEvidence (n :: S) where
- Distinct :: forall (n :: S). Distinct n => DistinctEvidence n
assertDistinct :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l
assertExt :: forall pattern (n :: S) (l :: S). CoSinkable pattern => pattern n l -> ExtEvidence n l
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 scopes, names, and binders

data S Source #

S is a data kind of scope indices.

Constructors

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.

data Scope (n :: S) Source #

A safe scope, indexed by a type-level scope index n.

Instances

Instances details

NFData (Scope n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: Scope n -> () #

data Name (n :: S) Source #

A name in a safe scope, indexed by a type-level scope index n.

Instances

Instances details

Sinkable Name Source #	Sinking a `Name` is as simple as applying the renaming.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #
RelMonad Name Expr Source #	`Expr` is a monad relative to `Name`.
Instance details Defined in Control.Monad.Foil.Example Methods rreturn :: forall (a :: S). Name a -> Expr a Source # rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b Source #
(Bifunctor sig, CoSinkable binder) => RelMonad Name (AST binder sig) Source #	`AST sig` is a monad relative to `Name`.
Instance details Defined in Control.Monad.Free.Foil Methods rreturn :: forall (a :: S). Name a -> AST binder sig a Source # rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> AST binder sig a -> (Name a -> AST binder sig b) -> AST binder sig b Source #
Show (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods showsPrec :: Int -> Name n -> ShowS # show :: Name n -> String # showList :: [Name n] -> ShowS #
NFData (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: Name n -> () #
Eq (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods (==) :: Name n -> Name n -> Bool # (/=) :: Name n -> Name n -> Bool #
Ord (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods compare :: Name n -> Name n -> Ordering # (<) :: Name n -> Name n -> Bool # (<=) :: Name n -> Name n -> Bool # (>) :: Name n -> Name n -> Bool # (>=) :: Name n -> Name n -> Bool # max :: Name n -> Name n -> Name n # min :: Name n -> Name n -> Name n #

data NameBinder (n :: S) (l :: S) Source #

A name binder is a name that extends scope n to a (larger) scope l.

Instances

Instances details

CoSinkable NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods 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 # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #
UnifiablePattern NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r Source #
Show (Expr n) Source #	Use `ppExpr` to show \(\lambda\)-terms.
Instance details Defined in Control.Monad.Free.Foil.Example Methods showsPrec :: Int -> Expr n -> ShowS # show :: Expr n -> String # showList :: [Expr n] -> ShowS #
Show (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods showsPrec :: Int -> NameBinder n l -> ShowS # show :: NameBinder n l -> String # showList :: [NameBinder n l] -> ShowS #
NFData (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: NameBinder n l -> () #
Eq (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods (==) :: NameBinder n l -> NameBinder n l -> Bool # (/=) :: NameBinder n l -> NameBinder n l -> Bool #
Ord (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods compare :: NameBinder n l -> NameBinder n l -> Ordering # (<) :: NameBinder n l -> NameBinder n l -> Bool # (<=) :: NameBinder n l -> NameBinder n l -> Bool # (>) :: NameBinder n l -> NameBinder n l -> Bool # (>=) :: NameBinder n l -> NameBinder n l -> Bool # max :: NameBinder n l -> NameBinder n l -> NameBinder n l # min :: NameBinder n l -> NameBinder n l -> NameBinder n l #

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.

extendScopePattern :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Scope n -> Scope l Source #

Extend scope with variables inside a pattern. This is a more flexible version of extendScope.

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.

namesOfPattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> [Name l] Source #

Extract names from a pattern. This is a more flexible version of namesOf.

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.

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.

withFreshPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o	Ambient scope.
-> pattern n l	Pattern to refresh (if it clashes with the ambient scope).
-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)	Continuation, accepting the refreshed pattern.
-> r

Rename a given pattern into a fresh version of it to extend a given scope.

This is similar to withRefreshPattern, except here renaming always takes place.

withRefreshed Source #

Arguments

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

withRefreshedPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o	Ambient scope.
-> pattern n l	Pattern to refresh (if it clashes with the ambient scope).
-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)	Continuation, accepting the refreshed pattern.
-> r

Safely rename (if necessary) a given pattern to extend a given scope. This is similar to withFreshPattern, except if a name in the pattern does not clash with the scope, it can be used immediately, without renaming.

This is a more general version of withRefreshed.

withRefreshedPattern' :: forall pattern (o :: S) e (n :: S) (l :: S) r. (CoSinkable pattern, Distinct o, InjectName e, Sinkable e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r Source #

Refresh (if needed) bound variables introduced in a pattern.

This is a version of withRefreshedPattern that uses functional renamings instead of Substitution.

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.

unsinkNamePattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Name l -> Maybe (Name n) Source #

Check if a name in the extended context is introduced in a pattern or comes from the outer scope n.

This is a generalization of unsinkName.

Safe (co)sinking and renaming

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

Methods

sinkabilityProof Source #

Arguments

:: forall (n :: S) (l :: S). (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

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.

Instances

Instances details

Sinkable Expr Source #	This instance serves as a proof that sinking of `Expr` is safe.
Instance details Defined in Control.Monad.Foil.Example Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l Source #
Sinkable Name Source #	Sinking a `Name` is as simple as applying the renaming.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #
Sinkable e => Sinkable (Substitution e i) Source #	Substitutions are sinkable as long as corresponding expressions are.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source #
(Bifunctor sig, CoSinkable binder) => Sinkable (AST binder sig) Source #
Instance details Defined in Control.Monad.Free.Foil Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> AST binder sig n -> AST binder sig l Source #

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.

Methods

coSinkabilityProof Source #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (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' :: S). (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

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.

withPattern Source #

Arguments

:: forall (o :: S) f (n :: S) (l :: S) r. Distinct o
=> (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')	Processing of a single `NameBinder`, this will be applied to each binder in a pattern.
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')	Result in case no binders are present. This can be seen as scope-indexed `mempty`.
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')	Composition of results for nested binders/patterns. This can be seen as scope-indexed `mappend`.
-> Scope o	Ambient scope.
-> pattern n l	Pattern to process.
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)	Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
-> r

Generalized processing of a pattern.

You can see withPattern as a CPS-style traversal over the binders in a pattern.

Instances

Instances details

CoSinkable NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods 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 # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #
CoSinkable NameBinderList Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinderList n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinderList n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinderList o o' -> r) -> r Source #
CoSinkable NameBinders Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #
CoSinkable U2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> U2 n l -> (forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> U2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r) -> r Source #
CoSinkable V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r 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.

extendRenaming Source #

Arguments

:: forall pattern (n :: S) (n' :: S) (l :: S) r. 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' :: S). (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

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 #

Arguments

:: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern
=> (NameBinder i n -> NameBinder i n')	Map names from scope `n` to a (possibly larger) scope `n'`.
-> pattern n l	A pattern that extends scope `n` to another scope `l`.
-> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r)	A continuation, accepting an extended renaming from `l` to `l'` (which itself extends `n'`) and a (possibly refreshed) pattern that extends `n'` to `l'`.
-> r

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 #

Arguments

:: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i')	Rename binders extending scope `n` from `i` to `i'`.
-> (NameBinder i' l -> NameBinder i' l')	Rename binders extending scope `i'` from `l` to `l'`.
-> NameBinder n l
-> NameBinder n l'

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 #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (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' :: S). (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

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

Safe substitutions

data 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.

Instances

Instances details

Sinkable e => Sinkable (Substitution e i) Source #	Substitutions are sinkable as long as corresponding expressions are.
Instance details Defined in Control.Monad.Foil.Internal Methods 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.

Unification of binders

data UnifyNameBinders (pattern :: S -> S -> Type) (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, we can often rename binders efficiently, by renaming binders only in one of the two unified terms.

Constructors

SameNameBinders	Binders are the same, proving that type parameters `l` and `r` are in fact equivalent.
Fields :: forall (n :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n l Unordered set of binders in the unified pattern (from any of the original patterns). -> UnifyNameBinders pattern n l l
RenameLeftNameBinder	It is possible to safely rename the left binder to match the right one.
Fields :: forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n r Unordered set of binders in the unified pattern (the binders from the right pattern). -> (NameBinder n l -> NameBinder n r) Binder renaming for the left pattern. -> UnifyNameBinders pattern n l r
RenameRightNameBinder	It is possible to safely rename the right binder to match the left one.
Fields :: forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n l Unordered set of binders in the unified pattern (the binders from the left pattern). -> (NameBinder n r -> NameBinder n l) Binder renaming for the right pattern. -> UnifyNameBinders pattern n l r
RenameBothBinders	It is necessary to rename both binders.
Fields :: forall (n :: S) (lr :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n lr Unordered set of binders in the unified pattern -> (NameBinder n l -> NameBinder n lr) Binder renaming for the left pattern. -> (NameBinder n r -> NameBinder n lr) Binder renaming for the right pattern. -> UnifyNameBinders pattern n l r
NotUnifiable :: forall (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S). UnifyNameBinders pattern n l r	Cannot unify to (sub)patterns.

unifyNameBinders Source #

Arguments

:: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). Distinct i
=> NameBinder i l	Left pattern.
-> NameBinder i r	Right pattern.
-> UnifyNameBinders pattern i l r

Unify binders either by asserting that they are the same, or by providing a safe renaming function to convert one binder to another.

andThenUnifyPatterns Source #

Arguments

:: forall pattern (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'	Unifying action for some outer patterns.
-> (pattern l r, pattern l' r')	Two nested patterns (cannot be unified directly since they extend different scopes).
-> UnifyNameBinders pattern n r r'

Chain unification of nested patterns.

andThenUnifyNameBinders Source #

Arguments

:: forall (pattern :: S -> S -> Type) (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'	Unifying action for some outer patterns.
-> (NameBinder l r, NameBinder l' r')	Two nested binders (cannot be unified directly since they extend different scopes).
-> UnifyNameBinders pattern n r r'

Chain unification of nested patterns with NameBinders.

class CoSinkable pattern => UnifiablePattern (pattern :: S -> S -> Type) where Source #

A pattern type is unifiable if it is possible to match two patterns and decide how to rename binders.

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r Source #

Unify two patterns and decide which binders need to be renamed.

Instances

Instances details

UnifiablePattern NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r Source #
UnifiablePattern U2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => U2 n l -> U2 n r -> UnifyNameBinders U2 n l r Source #
UnifiablePattern V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

class UnifiableInPattern a where Source #

Unification of values in patterns. By default, Eq instance is used, but it may be useful to ignore some data in pattens (such as location annotations).

Minimal complete definition

Nothing

Methods

unifyInPattern :: a -> a -> Bool Source #

Unify non-binding components of a pattern.

default unifyInPattern :: Eq a => a -> a -> Bool Source #

data NameBinders (n :: S) (l :: S) Source #

An unordered collection of NameBinders, that together extend scope n to scope l.

For an ordered version see NameBinderList.

Instances

Instances details

CoSinkable NameBinders Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #

emptyNameBinders :: forall (n :: S). NameBinders n n Source #

An empty set of binders keeps the scope as is.

mergeNameBinders :: forall (n :: S) (i :: S) (l :: S). NameBinders n i -> NameBinders i l -> NameBinders n l Source #

Composition of sets of binders.

Eliminating impossible unification

data V2 (n :: S) (l :: S) Source #

An empty pattern type specifies zero possibilities for patterns.

This type can be used to specify that patterns are not possible.

Instances

Instances details

CoSinkable V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r Source #
UnifiablePattern V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a Source #

Since V2 values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".

Name maps

data NameMap (n :: S) a Source #

A total map from names in scope n to elements of type a.

emptyNameMap :: NameMap 'VoidS a Source #

An empty map belongs in the empty scope.

lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a Source #

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.

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.

Constraints

class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S) Source #

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.

Instances

Instances details

(ExtEndo n => ExtEndo l) => Ext n l Source #
Instance details Defined in Control.Monad.Foil.Internal

data ExtEvidence (n :: S) (l :: S) where Source #

Evidence that scope l extends scope n.

Constructors

Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l

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

Instances details

Distinct 'VoidS Source #
Instance details Defined in Control.Monad.Foil.Internal

data DistinctEvidence (n :: S) where Source #

Evidence that scope n contains distinct names.

Constructors

Distinct :: forall (n :: S). Distinct n => DistinctEvidence n

assertDistinct :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l Source #

A distinct scope extended with a NameBinder is also distinct.

assertExt :: forall pattern (n :: S) (l :: S). CoSinkable pattern => pattern n l -> ExtEvidence n l Source #

A distinct scope extended with a NameBinder is also distinct.

type DExt (n :: S) (l :: S) = (Distinct l, Ext n l) Source #

Scope extensions with distinct names.

class InjectName (e :: S -> Type) where Source #

Instances of this typeclass possess the ability to inject names. Usually, this is a variable data constructor.

Methods

injectName :: forall (n :: S). Name n -> e n Source #

Inject names into expressions.

Instances

Instances details

InjectName Expr Source #
Instance details Defined in Control.Monad.Foil.Example Methods injectName :: forall (n :: S). Name n -> Expr n Source #
InjectName (AST binder sig) Source #
Instance details Defined in Control.Monad.Free.Foil Methods injectName :: forall (n :: S). Name n -> AST binder sig n Source #