S is a data kind of scope indices.

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

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

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

An empty scope (without any names).

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

A runtime check for potential name capture.

Extract name from a name binder.

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

Allocate a fresh binder for a given scope.

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

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.

Try coercing the name back to the (smaller) scope, given a binder that extends that scope.

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

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.

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.

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.

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.

Safely compose renamings of name binders. The underlying implementation is

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

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

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

Apply substitution to a given name.

Identity substitution maps all names to expresion-variables.

Extend substitution with a particular mapping.

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

Unification result for two binders, extending some common scope to scopes l and r respectively.

Due to the implementation of the foil,

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

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

An empty map belongs in the empty scope.

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.

Extending a map with a single mapping.

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

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.

Evidence that scope l extends scope n.

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.

Evidence that scope n contains distinct names.

A distinct scope extended with a NameBinder is also distinct.

A distinct scope extended with a NameBinder is also distinct.

Scope extensions with distinct names.

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