The type of abstractions of a list of atoms. It is equivalent to Bind [Atom] t, but has a more low-level implementation.

Abstract a list of atoms in a term.

Open a list abstraction.

Open a list abstraction for printing.

Merge a pair of list abstractions. If the lists are of different lengths, return Nothing.

A representation of patterns of type a. This is an abstract type with no exposed structure. The only way to construct a value of type NominalPattern a is through the Applicative interface and by using the functions binding and nobinding.

Constructor for non-binding patterns. This can be used to mark non-binding subterms when defining a Bindable instance. See "Defining custom instances" for examples.

Constructor for a pattern binding a single atom.

Map a function over a NominalPattern.

Combinator giving NominalPattern an applicative structure. This is used for constructing tuple binders.

Bind a t is the type of atom abstractions, denoted [A]T in the nominal logic literature. Its elements are pairs (a,t) modulo alpha-equivalence. We also write a.t for such an equivalence class of pairs. For full technical details on what this means, see Definition 4 of [Pitts 2002].

A type is Bindable if its elements can be abstracted by binders. Such elements are also called patterns. Examples include atoms, tuples of atoms, list of atoms, etc.

In most cases, instances of Nominal can be automatically derived. See "Deriving generic instances" for information on how to do so, and "Defining custom instances" for how to write custom instances.

Atom abstraction: a.t represents the equivalence class of pairs (a,t) modulo alpha-equivalence.

We use the infix operator (.), which is normally bound to function composition in the standard Haskell library. Thus, nominal programs should import the standard library like this:

import Prelude hiding ((.))

Note that (.) is a binder of the object language (i.e., whatever datatype you are defining), not of the metalanguage (i.e., Haskell). A term such as a.t only makes sense if a is already defined to be some atom. Thus, binders are often used in a context of with_fresh or open, such as the following:

with_fresh (\a -> a.a)

An alternative non-infix notation for (.). This can be useful when using qualified module names, because "̈Nominal.." is not valid syntax.

Destructor for atom abstraction. In an ideal programming idiom, we would be able to define a function on atom abstractions by pattern matching like this:

f (a.s) = body.

Haskell doesn't let us provide this syntax, but using the open function, we can equivalently write:

f t = open t (\a s -> body).

Each time an abstraction is opened, a is guaranteed to be a fresh atom. To guarantee soundness (referential transparency and equivariance), the body is subject to the same restriction as with_fresh, namely, a must be fresh for the body (in symbols a # body).

A variant of open which moreover chooses a name for the bound atom that does not clash with any free name in its scope. This function is mostly useful for building custom pretty-printers for nominal terms. Except in pretty-printers, it is equivalent to open.

Usage:

open_for_printing sup t (\x s sup' -> body)

Here, sup = support t (this requires a NominalSupport instance). For printing to be efficient (roughly O(n)), the support must be pre-computed in a bottom-up fashion, and then passed into each subterm in a top-down fashion (rather than re-computing it at each level, which would be O(n²)). For this reason, open_for_printing takes the support of t as an additional argument, and provides sup', the support of s, as an additional parameter to the body.

Open two abstractions at once. So

f t = open t (\x y s -> body)

is equivalent to the nominal pattern matching

f (x.y.s) = body

Like open2, but open two abstractions for printing.

The type constructor NoBind permits data of arbitrary types (including nominal types) to be embedded in binders without becoming bound. For example, in the term

m = (a, NoBind b).(a,b),

the atom a is bound, but the atom b remains free. Thus, m is alpha-equivalent to (x, NoBind b).(x,b), but not to (x, NoBind c).(x,c).

A typical use case is using contexts as binders. A context is a map from atoms to some data (for example, a typing context is a map from atoms to types, and an evaluation context is a map from atoms to values). If we define contexts like this:

type Context t = [(Atom, NoBind t)]

then we can use contexts as binders. Specifically, if Γ = {x₁ ↦ A₁, …, xₙ ↦ Aₙ} is a context, then (Γ . t) binds the context to a term t. This means, x₁,…,xₙ are bound in t, but not any atoms that occur in A₁,…,Aₙ. Without the use of NoBind, any atoms occurring on A₁,…,Aₙ would have been bound as well.

Even though atoms under NoBind are not binding, they can still be bound by other binders. For example, the term x.(x, NoBind x) is alpha-equivalent to y.(y, NoBind y). Another way to say this is that NoBind has a special behavior on the left, but not on the right of a dot.

A helper function for defining Bindable instances for non-nominal types.

A specialized combinator. Although this functionality is expressible in terms of the applicative structure, we give a custom CPS-based implementation for performance reasons. It improves the overall performance by 14% (time) and 16% (space) in a typical benchmark.

A version of the Bindable class suitable for generic programming.

Function composition.

Since we hide (.) from the standard library, and the fully qualified name of the Prelude's dot operator, "̈Prelude..", is not legal syntax, we provide '∘' as an alternate notation for composition.