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

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

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

A runtime check for potential name capture.

Since: 0.0.1

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

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

Since: 0.0.1

We will use Int for efficient representation of identifiers.

Since: 0.0.1

Raw name is simply an identifier.

Since: 0.0.1

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

An inclusive reservation of a contiguous range of raw names.

A range is a bound on an allocator (see withFreshIn), not a set of names: its runtime content is two Ints. A range with lo > hi is empty.

Since: 0.4.0

The range of all non-negative names.

On a scope without negative members, allocation within fullNameRange agrees with rawFreshName. The two diverge on a scope with negative members: rawFreshName allocates right above the maximum, wherever that lands, while fullNameRange clamps allocation to non-negative names.

Since: 0.4.0

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

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

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

The names a pattern binds.

Since: 0.4.0

All the names in a scope.

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

Sinkable for a type with any number of scope indices, and the class a pattern derives to obtain the foil's traversals. An instance is normally empty, leaving the generic implementation to walk the RepK of the type.

Since: 0.3.0

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

Since: 0.0.1

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.

Since: 0.0.1

The renaming that carries a pattern's payloads into the ambient scope of withPattern.

A pattern may carry fields indexed by its own scope, the standard example being a telescope, where each step has a type in the scope the steps before it extend to. Rebuilding such a pattern at the ambient scope means rebuilding those fields there too, and withPattern hands the instance no renaming for it. This is that renaming, accumulated as the traversal goes.

It is abstract on purpose: the only ways to build one are verbatimTransport and transportUnderBinder, which together are exactly what a correct withPattern does.

Soundness rests on what withPattern is allowed to do. It replaces binders and nothing else, so a raw name the pattern does not bind means in o what it meant in n, and the identity on raw names is a renaming from the one to the other. That is the same coercion extendRenaming and unsafeAssertFresh already perform.

Since: 0.4.0

The transport to start a withPattern traversal with, before any binder has been seen.

Since: 0.4.0

Extend a transport by one binder of the pattern.

The names of the inner scope are the binder's own, which goes to whatever the refreshed binder introduces, and the names of the outer scope, which the transport so far already answers for.

Since: 0.4.0

Carry a payload along a transport.

The Sinkable instance does the walking, and only when it has to. While no binder has been refreshed the payload is taken over as it stands, so the traversals that never rename (extendScopePattern, namesOfPattern, nameBinderListOf) do not walk payloads at all.

The whole recipe for a payload-carrying pattern, at a telescope of labelled steps:

instance Sinkable e => CoSinkable (Telescope label e) where
  withPattern withBinder unit comp = go verbatimTransport
    where
      go _transport _scope TelescopeEmpty cont = cont unit TelescopeEmpty
      go transport scope (TelescopeCons label payload binder rest) cont =
        withBinder scope binder $ \fbinder binder' ->
          go (transportUnderBinder transport binder binder')
             (extendScope binder' scope) rest $ \frest rest' ->
            cont (comp fbinder frest)
              (TelescopeCons label (transportPayload transport payload)
                             binder' rest')

Note which transport each payload takes: the one accumulated before its own binder, since that is the scope the payload lives in.

Since: 0.4.0

Carry a single name along a transport.

Since: 0.4.0

If HasNameBinders f, then f n l is expected to act as a binder, introducing into scope n some local variables, extending it to scope l. This class allows to extract and modify the set of binders.

Since: 0.3.0

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.

sink is the base of a family of \(O(1)\) coercions, named after Data.Functor.Classes: sink1 sinks through one Functor layer and sink2 through a Bifunctor, each justified by a lifted sinkability proof of its own.

Tuples and records need no private unsafeCoerce helpers either. A pair of sinkables is a sink2 (Tannen for a whole container of them), and a pair whose first component is scope-free is a sink1 through Compose f ((,) a). A record of sinkable fields derives Sinkable through deriveGenericK and empty SinkableK and Sinkable instances, after which the whole record sinks in one coercion. A record holding the Scope itself is rightly refused, since there is no SinkableK Scope: the scope must grow when a binder is entered, so keep it beside the sinkable part and not inside it.

Do not map sink over a container. fmap sink walks the whole spine to apply a per-element coercion, where sink1 is one coercion. Rewrite rules turn the elementwise forms into the corresponding family member where they fire, but they are best-effort (they need optimisation on, and fmap at a known functor is often resolved to the instance method first), so write the family member directly.

Since: 0.0.1

Sink an entire container of sinkable expressions, in \(O(1)\): sink lifted through one Functor layer, justified by the Sinkable instance of Compose.

The soundness argument for sink extends to a container of sinkables, such as an IntMap of terms, a Map keyed by something else, or a list of them. So there is no need to walk the spine with fmap sink, and entering a binder need not be \(O(size)\).

>>> :{
sinkEnv :: DExt n l => Map.Map String (Name n) -> Map.Map String (Name l)
sinkEnv = sink1
:}

A nested container is one Compose away: f (g (e n)) is Compose f g (e n), and the composition is again a Functor, so sink1 covers it too.

Two things this does not cover:

• A Scope is not sinkable, and must not be sunk: it is the set of names in scope n, and it has to grow when a binder is entered (see extendScope).
• A NameMap must stay total on the names in scope (lookupName errors otherwise), so sinking one has to be paired with adding the new binder's entry (see addNameBinder).

Since: 0.4.0

Sink both slots of a Bifunctor of sinkables, in \(O(1)\), the two scopes moving independently: the shape of liftEq2, with a coercion in place of each of the two functions.

>>> :{
sinkBoth :: (DExt n n', DExt m m') => (Name n, Name m) -> (Name n', Name m')
sinkBoth = sink2
:}

A container of such pairs is a Bifunctor again, via Tannen, so a list of pairs of names, the shape an α-equivalence test threads, also sinks in one coercion:

>>> :{
sinkPairs :: (DExt n n', DExt m m') => [(Name n, Name m)] -> [(Name n', Name m')]
sinkPairs = runTannen . sink2 . Tannen
:}

Since: 0.4.0

The sinkability proof lifted through a Bifunctor, with one renaming per slot. Once this typechecks, sinking both slots at once is a coercion; sink2 is to this proof exactly what sink is to sinkabilityProof.

Since: 0.4.0

The name sink1 had before the family existed.

Since: 0.3.2

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.

Since: 0.0.1

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.

Since: 0.0.3

Safely compose renamings of name binders. The underlying implementation is

Since: 0.0.3

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

Since: 0.0.3

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

Since: 0.0.1

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

Since: 0.0.1

Apply substitution to a given name.

Since: 0.0.1

Identity substitution maps all names to expresion-variables.

Since: 0.0.1

Whether a substitution maps every name to itself (see addRename, which deletes identity renames, so this is one null test).

Since: 0.4.0

An empty substitution from an empty scope.

Since: 0.2.0

Extend substitution with a particular mapping.

Since: 0.0.1

Extend a substitution with a value for each binder of a pattern, in the order the pattern binds them.

Since: 0.2.0

Extend a substitution with a value for each binder of a chain, in order. Fails with error when the list of values is too short.

Since: 0.2.0

Add variable renaming to a substitution.

When the binder is mapped to its own name, the name is deleted from the substitution rather than mapped to itself. This is an optimization, but it is not only an optimization: it is also how the binder shadows an outer binding of the same raw name, so the delete cannot be skipped even when nothing is being renamed. See withRefreshedPattern for why that rules out an all-binders-fresh fast path.

Since: 0.0.1

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

Chain unification of nested patterns.

Since: 0.1.0

Chain unification of nested patterns with NameBinders.

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

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

Since: 0.1.0

Comparison of scope-indexed values up to α, in a known scope.

unifyPatterns is given only Distinct, which is enough to line up binders and not enough to compare anything living in a scope. A pattern that carries a payload needs this to compare its payloads against another's, which is what unifyPatternsIn is for.

Since: 0.4.0