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.

The correct use of this function is subject to Pitts's freshness condition.

Open a list abstraction for printing.

The correct use of this function is subject to Pitts's freshness condition.

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

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

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

Constructor for a binder binding a single atom.

Map a function over a NominalBinder.

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

Bind a t is the type of 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, which is denoted a.t in the nominal logic literature. For full technical details on what this means, see Definition 4 of [Pitts 2003].

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

In most cases, instances of Bindable 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.

Usage as a constructor

The term a :. t is a constructor for abstractions. It represents the equivalence class of pairs (a,t) modulo alpha-equivalence. This is the same concept that is written as a.t in the nominal logic literature. We use the notation (:.) because the standard Haskell library reserves (.) for function composition.

Note that (:.) is an abstraction operator 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 the variable a is already defined to be a particular atom. Thus, abstractions are often used in the context of a scoped operation such as with_fresh or on the right-hand side of an abstraction pattern match, as in the following examples:

with_fresh (\a -> a :. a)

subst m z (Abs (x :. t)) = Abs (x :. subst m z t)

For building an abstraction by using a binder of the metalanguage, see also the function bind.

Usage as a pattern

We can also use (x :. t) as a pattern for pattern matching. It is called an abstraction pattern. Its behavior is very different from ordinary patterns. An abstraction pattern (x :. t) matches any term of type (Bind a b). When matching the pattern (x :. t) with a value y:.s, the effect is that a fresh name x and a value t will be generated such that x :. t = y :. s. Is it important to note that a different fresh x is chosen each time an abstraction patterns is used. Here are some examples:

foo (x :. t) = body

let (x :. t) = s in body

case t of
  Var v -> body1
  App m n -> body2
  Abs (x :. t) -> body3

Like all patterns, abstraction patterns can be nested. For example:

foo1 (a :. b :. t) = ...

foo2 (x :. (s,t)) = (x :. s, x :. t)

foo3 (Abs (x :. Var y))
  | x == y    = ...
  | otherwise = ...

The correct use of abstraction patterns is subject to Pitts's freshness condition. Thus, for example, the following are permitted

let (x :. t) = s in x :. t,
let (x :. t) = s in f x t == g x t,

whereas the following is not permitted:

let (x :. t) = s in (x,t).

See "Pitts's freshness condition" for more details.

An alternative non-infix notation for (:.).

An alternative notation for abstraction patterns.

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

is precisely equivalent to

f (x :. s) = body.

The correct use of this function is subject to Pitts's freshness condition.

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.

The correct use of this function is subject to Pitts's freshness condition.

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.