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

Constructor for abstractions. The term 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 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.

A pattern matching syntax for abstractions. The pattern (x :. t) is called an abstraction pattern. It matches any term of type (Bind a b). The result of matching the pattern (x :. t) against a value y.s is to bind x to a fresh name and t to a value such that x.t = y.s. 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 (.). This can be useful when using qualified module names, because "̈Nominal.." is not valid syntax.

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.

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.