Names are things that get bound. This type is intentionally abstract; to create a Name you can use string2Name or integer2Name. The type parameter is a tag, or sort, which tells us what sorts of things this name may stand for. The sort must be a representable type, i.e. an instance of the Rep type class from the RepLib generic programming framework.

To hide the sort of a name, use AnyName.

A name with a hidden (existentially quantified) sort. To hide the sort of a name, use the AnyName constructor directly; to extract a name with a hidden sort, use toSortedName.

Create a free Name from an Integer.

Create a free Name from a String.

Convenient synonym for string2Name.

Create a free Name from a String and an Integer index.

Get the integer index of a Name.

Get the string part of a Name.

Get the integer index of an AnyName.

Get the string part of an AnyName.

Change the sort of a name.

Cast a name with an existentially hidden sort to an explicitly sorted name.

A smart constructor for binders, also sometimes referred to as "close". Free variables in the term are taken to be references to matching binders in the pattern. (Free variables with no matching binders will remain free.)

Bind the pattern in the term "up to permutation" of bound variables. For example, the following 4 terms are all alpha-equivalent:

 permbind [a,b] (a,b)
 permbind [a,b] (b,a)
 permbind [b,a] (a,b)
 permbind [b,a] (b,a)

Note that none of these terms is equivalent to a term with a redundant pattern such as

 permbind [a,b,c] (a,b)

For binding constructors which do render these equivalent, see setbind and setbindAny.

Bind the list of names in the term up to permutation and dropping of unused variables.

For example, the following 5 terms are all alpha-equivalent:

 setbind [a,b] (a,b)
 setbind [a,b] (b,a)
 setbind [b,a] (a,b)
 setbind [b,a] (b,a)
 setbind [a,b,c] (a,b)

There is also a variant, setbindAny, which ignores name sorts.

Bind the list of (any-sorted) names in the term up to permutation and dropping of unused variables. See setbind.

Unbind (also known as "open") is the simplest destructor for bindings. It ensures that the names in the binding are globally fresh, using a monad which is an instance of the Fresh type class.

lunbind opens a binding in an LFresh monad, ensuring that the names chosen for the binders are locally fresh. The components of the binding are passed to a continuation, and the resulting monadic action is run in a context extended to avoid choosing new names which are the same as the ones chosen for this binding.

For more information, see the documentation for the LFresh type class.

Unbind two terms with the same fresh names, provided the binders have the same binding variables (both number and sort). If the patterns have different binding variables, return Nothing. Otherwise, return the renamed patterns and the associated terms.

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 for more details.

Unbind two terms with the same locally fresh names, provided the patterns have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

Unbind three terms with the same locally fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

Embed allows for terms to be embedded within patterns. Such embedded terms do not bind names along with the rest of the pattern. For examples, see the tutorial or examples directories.

If t is a term type, then Embed t is a pattern type.

Embed is not abstract since it involves no binding, and hence it is safe to manipulate directly. To create and destruct Embed terms, you may use the Embed constructor directly. (You may also use the functions embed and unembed, which additionally can construct or destruct any number of enclosing Shifts at the same time.)

Construct an embedded term, which is an instance of Embed with any number of enclosing Shifts. That is, embed can have any of the types

• t -> Embed t

• t -> Shift (Embed t)

• t -> Shift (Shift (Embed t))

and so on.

Destruct an embedded term. unembed can have any of the types

• Embed t -> t

• Shift (Embed t) -> t

and so on.

Rebind allows for nested bindings. If p1 and p2 are pattern types, then Rebind p1 p2 is also a pattern type, similar to the pattern type (p1,p2) except that p1 scopes over p2. That is, names within terms embedded in p2 may refer to binders in p1.

Constructor for rebinding patterns.

Destructor for rebinding patterns. It does not need a monadic context for generating fresh names, since Rebind can only occur in the pattern of a Bind; hence a previous call to unbind (or something similar) must have already freshened the names at this point.

If p is a pattern type, then Rec p is also a pattern type, which is recursive in the sense that p may bind names in terms embedded within itself. Useful for encoding e.g. lectrec and Agda's dot notation.

Constructor for recursive patterns.

Destructor for recursive patterns.

TRec is a standalone variant of Rec: the only difference is that whereas Rec p is a pattern type, TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Note that TRec corresponds to Pottier's abstraction construct from alpha-Caml. In this context, Embed t corresponds to alpha-Caml's inner t, and Shift (Embed t) corresponds to alpha-Caml's outer t.

Constructor for recursive abstractions.

Destructor for recursive abstractions which picks globally fresh names for the binders.

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

Shift the scope of an embedded term one level outwards.

Determine the alpha-equivalence of two terms.

Determine (alpha-)equivalence of patterns. Do they bind the same variables in the same patterns and have alpha-equivalent annotations in matching positions?

An alpha-respecting total order on terms involving binders.

Calculate the free variables of a particular sort contained in a term.

Calculate the free variables (of any sort) contained in a term.

Calculate the variables of a particular sort that occur freely in terms embedded within a pattern (but are not bound by the pattern).

Calculate the variables (of any sort) that occur freely in terms embedded within a pattern (but are not bound by the pattern).

Calculate the binding variables (of a particular sort) in a pattern.

Calculate the binding variables (of any sort) in a pattern.

Collections are foldable types that support empty, singleton, union, and map operations. The result of a free variable calculation may be any collection. Instances are provided for lists, sets, and multisets.

A simple representation of multisets.

The Subst class governs capture-avoiding substitution. To derive this class, you only need to indicate where the variables are in the data type, by overriding the method isvar.

See isvar.

A permutation is a bijective function from names to names which is the identity on all but a finite set of names. They form the basis for nominal approaches to binding, but can also be useful in general.

Create a permutation which swaps two elements.

Compose two permutations. The right-hand permutation will be applied first.

Apply a permutation to an element of the domain.

The support of a permutation is the set of elements which are not fixed.

Is this the identity permutation?

Join two permutations by taking the union of their relation graphs. Fail if they are inconsistent, i.e. map the same element to two different elements.

The empty (identity) permutation.

Restrict a permutation to a certain domain.

mkPerm l1 l2 creates a permutation that sends l1 to l2. Fail if there is no such permutation, either because the lists have different lengths or because they are inconsistent (which can only happen if l1 or l2 have repeated elements).

Apply a permutation to a term.

Apply a permutation to the embedded terms in a pattern. Binding names are left alone by the permutation.

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

Freshen a pattern by replacing all old binding Names with new fresh Names, returning a new pattern and a Perm Name specifying how Names were replaced.

The Fresh type class governs monads which can generate new globally unique Names based on a given Name.

A convenient monad which is an instance of Fresh. It keeps track of a global index used for generating fresh names, which is incremented every time fresh is called.

Run a FreshM computation (with the global index starting at zero).

The FreshM monad transformer. Keeps track of the lowest index still globally unused, and increments the index every time it is asked for a fresh name.

Run a FreshMT computation (with the global index starting at zero).

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, not necessarily globally fresh.

A convenient monad which is an instance of LFresh. It keeps track of a set of names to avoid, and when asked for a fresh one will choose the first unused numerical name.

Run a LFreshM computation in an empty context.

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first numeric prefix of the given name which is currently unused.

Run an LFreshMT computation in an empty context.

The Alpha type class is for types which may contain names. The Rep1 constraint means that we can only make instances of this class for types that have generic representations (which can be automatically derived by RepLib.)

Note that the methods of Alpha should almost never be called directly. Instead, use other methods provided by this module which are defined in terms of Alpha methods.

Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring

 instance Alpha MyType

Occasionally, however, it may be useful to override the default implementations of one or more Alpha methods for a particular type. For example, consider a type like

 data Term = ...
           | Annotation Stuff Term

where the Annotation constructor of Term associates some sort of annotation with a term --- say, information obtained from a parser about where in an input file the term came from. This information is needed to produce good error messages, but should not be taken into consideration when, say, comparing two Terms for alpha-equivalence. In order to make aeq ignore annotations, you can override the implementation of aeq' like so:

 instance Alpha Term where
   aeq' c (Annotation _ t1) t2 = aeq' c t1 t2
   aeq' c t1 (Annotation _ t2) = aeq' c t1 t2
   aeq' c t1 t2 = aeqR1 rep1 t1 t2

Note how the call to aeqR1 handles all the other cases generically.