S is a data kind of scope indices.

Since: 0.0.1

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

Since: 0.0.1

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

Since: 0.0.1

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

Since: 0.0.1

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

Since: 0.0.1

An empty scope (without any names).

Since: 0.0.1

A runtime check for potential name capture.

Since: 0.0.1

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

Since: 0.0.1

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

Since: 0.0.1

Auxiliary data structure for scope extension. Used in extendScopePattern.

Since: 0.1.0

Identity scope extension (no extension).

Since: 0.1.0

Compose scope extensions.

Since: 0.1.0

Extract name from a name binder.

Since: 0.0.1

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

Since: 0.1.0

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

Since: 0.1.0

Empty list of names in scope n.

Since: 0.1.0

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

Since: 0.1.0

Allocate a fresh binder for a given scope.

Since: 0.0.1

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

Since: 0.0.1

Safely produce a fresh name binder, allocated within a given range.

The binder is fresh with respect to the whole ambient scope, not merely to its part inside the range. Indeed, the allocated name lies in the range and is greater than every scope member there, while a scope member outside the range cannot be equal to a name inside it (see rawFreshNameIn). Thus the usual freshness evidence applies, and no invariant beyond the scope itself is required.

This is the primitive behind allocation policies such as per-module name blocks: reserve disjoint ranges for independently checked units, and the names allocated for them can never collide.

Fails with error when the range is exhausted. Use tryWithFreshIn to handle exhaustion instead.

>>> withFreshIn (NameRange 100 199) emptyScope (nameId . nameOf)
100

Since: 0.4.0

A version of withFreshIn that reports an exhausted range with Nothing instead of failing. A driver that hands out ranges can then report which unit ran out of its reservation.

Since: 0.4.0

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

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

Since: 0.1.0

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.

Since: 0.0.1

A version of withRefreshed that allocates the replacement name within a given range when the candidate is taken. A client that reserves regions of the raw-name line (per-module stripes, a region for locals) uses this so that a rename cannot stray into someone else's reservation.

Since: 0.4.0

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.

The continuation also receives the scope extended with the refreshed pattern: the traversal computes it along the way, so the caller does not recompute it with extendScopePattern (a second traversal of the same pattern). The same holds for withFreshPattern and withRefreshedPattern'.

Note that there is deliberately no fast path for the case when every binder of the pattern is already fresh in the ambient scope. It is tempting to test all binders at once and, when none clashes, hand the continuation sink instead of a renaming composed per binder. That would be unsound.

Even when a binder is not renamed, the per-binder step is not the identity: addRename deletes the name from the substitution, which is how the binder shadows an outer binding of the same raw name. For skipping that delete to be harmless we would need the substitution's domain to avoid the pattern's binder names, but the substitution's domain lives in the pattern's own scope n, while freshness is tested against the unrelated ambient scope o.

The two can indeed disagree, because sink is a coercion and does not rename: a term built in a small scope keeps its binder names when it is placed in a larger one, so a binder can share a raw name with its own enclosing scope. Ordinary evaluation produces such terms, with a λ x1 nested inside another λ x1. Handing such a caller sink would apply its substitution to a name the pattern binds, which is to say capture the bound variable.

Since: 0.0.1

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

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

Like withRefreshedPattern, this has no all-binders-already-fresh fast path, and for the same reason. Here shadowing is handled by unsinkName rather than by a delete: a name the pattern binds is routed to injectName and never reaches the caller's renaming, whether or not the binder was refreshed.

Since: 0.1.0

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

Since: 0.0.1

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

Since: 0.1.0

Trivial substitution (coercion via sink).

Since: 0.1.0

Composition of substitution extensions.

Since: 0.1.0

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

Since: 0.1.0

Trivial substitution extension (coercion via sink).

Since: 0.1.0

Composition of substitution extensions.

Since: 0.1.0

Evidence that scope n contains distinct names.

Since: 0.0.1

Evidence that scope l extends scope n.

Since: 0.0.1

A distinct scope extended with a NameBinder is also distinct.

Since: 0.0.1

A distinct scope extended with a NameBinder is also distinct.

Since: 0.0.3

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

Since: 0.0.1

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

Since: 0.0.1

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

Since: 0.0.1

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.

Since: 0.1.0

Auxiliary structure for unsinking names. Used in unsinkNamePattern.

Since: 0.1.0

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

Since: 0.1.0

Composition of unsinking for nested binders/patterns.

Since: 0.1.0

A set of names of scope n.

This is not a Scope: a Scope is all the names in scope, and the foil relies on that (it is what freshness is tested against, and what Distinct speaks about). A NameSet is any subset of them, such as the names a term uses or the assumptions a declaration depends on, and carries no such invariant.

<> is union and mempty is empty, so a NameSet can be accumulated with foldMap.

Since: 0.4.0

An empty set of names.

Since: 0.4.0

\(O(1)\). A set of one name.

Since: 0.4.0

\(O(\min(n,W))\). Add a name to a set.

Since: 0.4.0

\(O(\min(n,W))\). Is this name in the set?

Since: 0.4.0

Is the set empty?

Since: 0.4.0

How many names are in the set?

Since: 0.4.0

The names in the set, in ascending order of their identifiers.

Since: 0.4.0

A set of the given names.

Since: 0.4.0

All the names in a scope.

Since: 0.4.0

The names a pattern binds.

Since: 0.4.0

\(O(\min(n,W))\). Does the scope contain every name in the set?

This is the test that restriction of a term comes down to, so it is the one place a restriction is paid for: compare a term's support against the scope it is to be restricted to.

Since: 0.4.0

Drop the names a pattern binds, taking a set of names of the inner scope to a set of names of the outer one.

This is unsinkNamePattern for a whole set at once, and \(O(\min(n,W))\) rather than one membership test per name. Removing the pattern's names is right even when one of them shares a raw name with the enclosing scope: inside the pattern that raw name denotes the binder, so no occurrence of it there is an occurrence of the outer name.

Since: 0.4.0

Cut a scope down to a subset of its names.

The names must be names of n; nothing checks it, which is why this is the only entry point and takes a NameSet rather than a bare IntSet. The continuation gets Ext m n, so anything living in the smaller scope can be sinked back into the larger one for free, and Distinct m, since a subset of distinct names is distinct.

Note on allocation. A name allocated from the restricted scope is fresh with respect to m and not to n, so it may collide with a name of n that the restriction dropped. This is sound, since Ext m n gives no way to move a term of n into a scope extending m. It does mean that a restricted scope is for inspecting and restricting terms, and not a base to build new binders on and then mix with the original scope.

Since: 0.4.0

Unsafely declare that a scope is a restriction of scope n. Used in withRestrictedScope.

Since: 0.4.0

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.

Since: 0.0.3

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

When the binders differ, the one with the larger name is renamed towards the one with the smaller name. The direction is deliberate, but it is not what makes the renaming safe.

The renaming returned here is not applied by substituting names blindly. Callers push it through a term with liftRM, which refreshes a binder whenever it would capture. So the target name may well be used by a binder inside the term being renamed, and the result is still correct. Binder names do not always grow with depth: a term built in a small scope keeps its small binder names when sink places it in a larger one.

Since: 0.0.3

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

Since: 0.1.0

Chain unification of nested patterns.

Since: 0.1.0

Chain unification of nested patterns with NameBinders.

Since: 0.1.0

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

For an ordered version see NameBinderList.

Since: 0.1.0

Unsafely merge sets of binders (via set union).

Since: 0.1.0

An empty set of binders keeps the scope as is.

Since: 0.1.0

Composition of sets of binders.

Since: 0.1.0

A singleton name binder set.

Since: 0.1.0

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

For an unordered version see NameBinders.

Since: 0.1.0

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

Since: 0.1.0

The raw names a list of binders binds, outermost first.

Since: 0.4.0

Keep only those binders of a list whose names are in a given set.

This is the thinning of a chain of binders, and it is what turns a support into a smaller chain in one step. The alternative, asking unsinkAST at every binder whether the term can do without it, walks the term once per binder, whereas a caller can compute the support once and thin against it.

The thinned scope m is produced rather than given, because there is nothing to give: a term's relevant scope (see withRelevantScope) is a subset of l and generally not an extension of n, since a term need not use everything already in scope. What comes back is n extended by the binders that survived, with Ext n m and Ext m l to place it between the two.

The set is taken as given. For a chain whose binders carry types, or anything else living in the intermediate scopes, the caller has to close the set under whatever those mention before thinning by it, since dropping a binder that a surviving binder's type refers to would leave that type unplaceable. The library cannot do that closure, having no view of what a binder carries.

Since: 0.4.0

Unsafely place a chain of binders between two scopes.

Sound for a chain thinned out of n to l: its names are those of n plus some of the binders between n and l, so it extends n, is extended by l, and is distinct because l was.

Since: 0.4.0

Add a binder to the end of an (ordered) list of binders.

Note that NameBinderListCons adds a binder to the front of the list, which is the outermost position. This adds one to the innermost position instead.

Since: 0.3.1

Concatenate two (ordered) lists of binders, the second extending the scope that the first extends to.

Since: 0.3.1

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

Since: 0.1.0

An empty pattern type specifies zero possibilities for patterns.

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

Since: 0.1.0

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

Since: 0.1.0

A unit pattern type corresponds to a wildcard pattern.

Since: 0.1.0

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

Note that the default implementation compares patterns only up to their binders. See unifyPatterns for what that does and does not distinguish.

Since: 0.0.1