Control.Monad.Foil.Internal

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

Safe types and operations

data S

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.

newtype Scope (n :: S)

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

Constructors

UnsafeScope RawScope

Instances

NFData (Scope n)

Defined in Control.Monad.Foil.Internal

Methods

rnf :: Scope n -> ()

newtype Name (n :: S)

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

Constructors

UnsafeName RawName

Instances

Sinkable Name

Sinking a Name is as simple as applying the renaming.

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l

RelMonad Name Expr

Expr is a monad relative to Name.

Defined in Control.Monad.Foil.Example

Methods

rreturn :: forall (a :: S). Name a -> Expr a

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b

(Bifunctor sig, CoSinkable binder) => RelMonad Name (AST binder sig)

AST sig is a monad relative to Name.

Defined in Control.Monad.Free.Foil

Methods

rreturn :: forall (a :: S). Name a -> AST binder sig a

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> AST binder sig a -> (Name a -> AST binder sig b) -> AST binder sig b

Show (Name n)

Defined in Control.Monad.Foil.Internal

Methods

showsPrec :: Int -> Name n -> ShowS

show :: Name n -> String

showList :: [Name n] -> ShowS

NFData (Name n)

Defined in Control.Monad.Foil.Internal

Methods

rnf :: Name n -> ()

Eq (Name n)

Defined in Control.Monad.Foil.Internal

Methods

(==) :: Name n -> Name n -> Bool

(/=) :: Name n -> Name n -> Bool

Ord (Name n)

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

nameId :: forall (l :: S). Name l -> Id

Convert Name into an identifier. This may be useful for printing and debugging.

newtype NameBinder (n :: S) (l :: S)

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

Constructors

UnsafeNameBinder (Name l)

Instances

CoSinkable NameBinder

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

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

UnifiablePattern NameBinder

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

Show (Expr n)

Use ppExpr to show \(\lambda\)-terms.

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)

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)

Defined in Control.Monad.Foil.Internal

Methods

rnf :: NameBinder n l -> ()

Eq (NameBinder n l)

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)

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

An empty scope (without any names).

member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool

A runtime check for potential name capture.

Extending scopes

extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l

\(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

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

newtype ExtendScope (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary data structure for scope extension. Used in extendScopePattern.

Constructors

ExtendScope (Scope n -> Scope l)

idExtendScope :: forall (n :: S) (o :: S) (o' :: S). ExtendScope n n o o'

Identity scope extension (no extension).

compExtendScope :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). ExtendScope n i o o' -> ExtendScope i l o' o'' -> ExtendScope n l o o''

Compose scope extensions.

Collecting new names

nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l

Extract name from a name binder.

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

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

newtype NamesOf (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary structure collecting names in scope l that extend scope n. Used in namesOfPattern.

Constructors

NamesOf [Name l]

idNamesOf :: forall (n :: S) (o :: S) (o' :: S). NamesOf n n o o'

Empty list of names in scope n.

compNamesOf :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''

Concatenation of names, resulting in a list of names in l that extend scope n.

Refreshing binders

withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r

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

Safely produce a fresh name binder with respect to a given scope.

withFreshPattern

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

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

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

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

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

unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r. NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r

Unsafely declare that a given name (binder) is already fresh in any scope n'.

newtype WithRefreshedPattern (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary structure to accumulate substitution extensions produced when refreshing a pattern. Used in withRefreshedPattern and withFreshPattern.

Constructors

WithRefreshedPattern (Substitution e n o -> Substitution e l o')

idWithRefreshedPattern :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern e n n o o'

Trivial substitution (coercion via sink).

compWithRefreshedPattern :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern e n i o o' -> WithRefreshedPattern e i l o' o'' -> WithRefreshedPattern e n l o o''

Composition of substitution extensions.

newtype WithRefreshedPattern' (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary structure to accumulate substitution extensions produced when refreshing a pattern. Similar to WithRefreshedPattern, except here substitutions are represented as functions. Used in withRefreshedPattern'.

Constructors

WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')

idWithRefreshedPattern' :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern' e n n o o'

Trivial substitution extension (coercion via sink).

compWithRefreshedPattern' :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern' e n i o o' -> WithRefreshedPattern' e i l o' o'' -> WithRefreshedPattern' e n l o o''

Composition of substitution extensions.

Extracting proofs from binders and patterns

data DistinctEvidence (n :: S) where

Evidence that scope n contains distinct names.

Constructors

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

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

Evidence that scope l extends scope n.

Constructors

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

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

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

A distinct scope extended with a NameBinder is also distinct.

unsafeDistinct :: forall (n :: S). DistinctEvidence n

Unsafely declare that scope n is distinct. Used in unsafeAssertFresh.

unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l

Unsafely declare that scope l extends scope n. Used in unsafeAssertFresh.

Unsinking names

unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n)

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)

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.

newtype UnsinkName (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary structure for unsinking names. Used in unsinkNamePattern.

Constructors

UnsinkName (Name l -> Maybe (Name n))

idUnsinkName :: forall (n :: S) (o :: S) (o' :: S). UnsinkName n n o o'

Trivial unsinking. If no scope extension took place, any name is free (since it cannot be bound by anything).

compUnsinkName :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). UnsinkName n i o o' -> UnsinkName i l o' o'' -> UnsinkName n l o o''

Composition of unsinking for nested binders/patterns.

Unification of binders

data UnifyNameBinders (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S) where

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

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.

unsafeMergeUnifyBinders :: forall (pattern :: S -> S -> Type) (a :: S) (a' :: S) (a'' :: S) (a''' :: S) (b' :: S) (b'' :: S). UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''

Unsafely merge results of unification for nested binders/patterns. Used in andThenUnifyPatterns.

andThenUnifyPatterns

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

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.

newtype NameBinders (n :: S) (l :: S)

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

For an ordered version see NameBinderList.

Constructors

UnsafeNameBinders IntSet

Instances

CoSinkable NameBinders

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

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

unsafeMergeNameBinders :: forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S). NameBinders a b -> NameBinders c d -> NameBinders n l

Unsafely merge sets of binders (via set union).

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

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

Composition of sets of binders.

nameBindersSingleton :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l

A singleton name binder set.

data NameBinderList (n :: S) (l :: S) where

An ordered collection (list) of NameBinders, that together extend scope n to scope l.

For an unordered version see NameBinders.

Constructors

NameBinderListEmpty :: forall (n :: S). NameBinderList n n

An empty list of binders keeps the scope as is.

NameBinderListCons

A non-empty list of binders.

Fields

• :: forall (n :: S) (i :: S) (l :: S). NameBinder n i

  Outermost binder.

• -> NameBinderList i l

  Remaining list of binders.

• -> NameBinderList n l

Instances

CoSinkable NameBinderList

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

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

nameBindersList :: forall (n :: S) (l :: S). NameBinders n l -> NameBinderList n l

Convert an unordered set of name binders into an ordered list (with some order).

fromNameBindersList :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l

Convert an ordered list of name binders into an unordered set.

Pattern combinators

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

An empty pattern type specifies zero possibilities for patterns.

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

Instances

CoSinkable V2

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

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

UnifiablePattern V2

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

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

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

data U2 (n :: S) (l :: S) where

A unit pattern type corresponds to a wildcard pattern.

Constructors

U2

Fields

• :: forall (n :: S). U2 n n

  Wildcard patten does not modify the scope.

Instances

CoSinkable U2

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

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

UnifiablePattern U2

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

Unifiable patterns

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

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

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

Instances

UnifiablePattern NameBinder

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

UnifiablePattern U2

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

UnifiablePattern V2

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

class UnifiableInPattern a where

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

Unify non-binding components of a pattern.

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

unsafeEqPattern :: forall pattern (n :: S) (l :: S) (n' :: S) (l' :: S). (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool

The easiest way to compare two patterns is to check if they are the same. This function is labelled unsafe, since we generally are interested in proper α-equivalence instead of direct equality.

Safe sinking

class Sinkable (e :: S -> Type) where

Sinking an expression from scope n into a (usualy extended) scope l, given the renaming (injection from scope n to scope l).

Methods

sinkabilityProof

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

Sinkable Expr

This instance serves as a proof that sinking of Expr is safe.

Defined in Control.Monad.Foil.Example

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l

Sinkable Name

Sinking a Name is as simple as applying the renaming.

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l

Sinkable e => Sinkable (Substitution e i)

Substitutions are sinkable as long as corresponding expressions are.

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

(Bifunctor sig, CoSinkable binder) => Sinkable (AST binder sig)

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

sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l

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

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

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

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'

Convert renaming of name binders into renaming of names in the inner scopes.

extendRenamingNameBinder

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

class CoSinkable (pattern :: S -> S -> Type) where

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

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

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

CoSinkable NameBinder

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

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

CoSinkable NameBinderList

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

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

CoSinkable NameBinders

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

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

CoSinkable U2

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

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

CoSinkable V2

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

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

newtype WithNameBinderList (r :: S) (n :: S) (l :: S) (o :: S) (o' :: S)

Auxiliary data structure for collecting name binders. Used in nameBinderListOf.

Constructors

WithNameBinderList (NameBinderList l r -> NameBinderList n r)

idWithNameBinderList :: forall (o :: S) (o' :: S) (r :: S) (n :: S). DExt o o' => WithNameBinderList r n n o o'

Empty list of name binders (identity).

compWithNameBinderList :: forall (o :: S) (o' :: S) (o'' :: S) (r :: S) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithNameBinderList r n i o o' -> WithNameBinderList r i l o' o'' -> WithNameBinderList r n l o o''

Concatenating lists of name binders (compose).

nameBinderListOf :: forall binder (n :: S) (l :: S). CoSinkable binder => binder n l -> NameBinderList n l

Collect name binders of a generalized pattern into a name binder list, which can be more easily traversed.

Safe substitions

newtype Substitution (e :: S -> Type) (i :: S) (o :: S)

A substitution is a mapping from names in scope i to expressions e o in scope o.

Constructors

UnsafeSubstitution (IntMap (e o))

Instances

Sinkable e => Sinkable (Substitution e i)

Substitutions are sinkable as long as corresponding expressions are.

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

lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o

Apply substitution to a given name.

identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i

Identity substitution maps all names to expresion-variables.

voidSubst :: forall (e :: S -> Type) (n :: S). Substitution e 'VoidS n

An empty substitution from an empty scope.

addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o

Extend substitution with a particular mapping.

addSubstPattern :: forall binder e (i :: S) (o :: S) (i' :: S). CoSinkable binder => Substitution e i o -> binder i i' -> [e o] -> Substitution e i' o

addSubstList :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinderList 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

Add variable renaming to a substitution. This includes the performance optimization of eliding names mapped to themselves.

Name maps

newtype NameMap (n :: S) a

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

Constructors

NameMap

Fields

• getNameMap :: IntMap a

emptyNameMap :: NameMap 'VoidS a

An empty map belongs in the empty scope.

nameMapToSubstitution :: forall (i :: S) e (o :: S). NameMap i (e o) -> Substitution e i o

Convert a NameMap of expressions into a Substitution.

addNameBinders :: forall binder (n :: S) (l :: S) a. CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input pattern (generalized binder).

addNameBinderList :: forall (n :: S) (l :: S) a. NameBinderList n l -> [a] -> NameMap n a -> NameMap l a

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input name binder list.

See also addNameBinders for a generalized version.

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

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

Extending a map with a single mapping.

Note that the scope parameter of the result differs from the initial map.

Raw types and operations

type Id = Int

We will use Int for efficient representation of identifiers.

type RawName = Id

Raw name is simply an identifier.

type RawScope = IntSet

A raw scope is a set of raw names.

rawFreshName :: RawScope -> RawName

\(O(\min(n, W))\). Generate a fresh raw name that does not appear in a given raw scope.

rawMember :: RawName -> RawScope -> Bool

Check if a raw name is contained in a raw scope.

Constraints

class ExtEndo (n :: S)

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 => ExtEndo l) => Ext (n :: S) (l :: 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.

Instances

(ExtEndo n => ExtEndo l) => Ext n l

Defined in Control.Monad.Foil.Internal

class Distinct (n :: S)

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

Defined in Control.Monad.Foil.Internal

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

Scope extensions with distinct names.

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

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

Inject names into expressions.

Instances

InjectName Expr

Defined in Control.Monad.Foil.Example

Methods

injectName :: forall (n :: S). Name n -> Expr n

InjectName (AST binder sig)

Defined in Control.Monad.Free.Foil

Methods

injectName :: forall (n :: S). Name n -> AST binder sig n