An efficient and easy-to-use library for defining datatypes with binders, and automatically handling bound variables and alpha-equivalence. It is based on Gabbay and Pitts's theory of nominal sets.

Most users should only import the top-level module Nominal, which exports all the relevant functionality in a clean and abstract way. Its submodules, such as Nominal.Unsafe, are implementation specific and subject to change, and should not normally be imported by user code.

We start with a minimal example. The following code defines a datatype of untyped lambda terms, as well as a substitution function. The important point is that the definition of lambda terms is automatically up to alpha-equivalence (i.e., up to renaming of bound variables), and substitution is automatically capture-avoiding. These details are handled by the Nominal library and do not require any special programming by the user.

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

import Nominal
import Prelude hiding ((.))

-- Untyped lambda terms, up to alpha-equivalence.
data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
  deriving (Generic, Nominal)

-- Capture-avoiding substitution.
subst :: Term -> Atom -> Term -> Term
subst m x (Var y)
  | x == y = m
  | otherwise = Var y
subst m x (App t s) = App (subst m x t) (subst m x s)
subst m x (Abs body) = open body (\y s -> Abs (y . subst m x s))

Let us examine this code in more detail:

• The first four lines are boilerplate. Any code that uses the Nominal library should enable the language options DeriveGeneric and DeriveAnyClass, and should import Nominal. We also hide the (.) operator from the Prelude, because the Nominal library re-purposes the period as a binding operator.
• The next line defines the datatype Term of untyped lambda terms. Here, Atom is a predefined type of atomic names, which we use as the names of variables. A term is either a variable, an application, or an abstraction. The type (Bind Atom Term) is defined by the Nominal library and represents pairs (a,t) of an atom and a term, modulo alpha-equivalence. We write a.t to denote such an alpha-equivalence class of pairs.
• The next line declares that Term is a nominal type, by deriving an instance of the type class Nominal (and also Generic, which enables the magic that allows Nominal instances to be derived automatically). In a nutshell, a nominal datatype is a type that is aware of the existence of atoms. The Bind operation can only be applied to nominal datatypes, because otherwise alpha-equivalence would not make sense.
• The substitution function inputs a term m, a variable x, and a term t, and outputs the term obtained from t by replacing all occurrences of the variable x by m. The clauses for variables and application are straightforward. Note that atoms can be compared for equality. In the clause for abstraction, the body of the abstraction, which is of type (Bind Atom Term), is opened: this means that a fresh name y and a term s are generated such that body = y.s. Since the name y is guaranteed to be fresh, the substitution can be recursively applied to s without the possibility that y may be captured in m or x.

Atoms are things that can be bound. The important properties of atoms are: there are infinitely many of them (so we can always find a fresh one), and atoms can be compared for equality. Atoms do not have any other special properties, and in particular, they are interchangeable (any atom is as good as any other atom).

As shown in the introductory example above, the type Atom can be used for this purpose. In addition, it is often useful to have more than one kind of atoms (for example, term variables and type variables), and/or to customize the default names that are used when atoms of each kind are displayed (for example, to use x, y, z for term variables and α, β, γ for type variables).

The standard way to define an additional type of atoms is to define a new empty type t that is an instance of AtomKind. Optionally, a list of suggested names for the atoms can be provided. Then AtomOfKind t is a new type of atoms. For example:

data VarName
instance AtomKind VarName where
  suggested_names _ = ["x", "y", "z"]

newtype Variable = AtomOfKind VarName

All atom types are members of the type class Atomic.

Sometimes we need to generate a fresh atom. In the Nominal library, the philosophy is that a fresh atom is usually generated for a particular purpose, and the use of the atom is local to that purpose. Therefore, a fresh atom should always be generated within a local scope. So instead of

let a = fresh in something,

we write

with_fresh (\a -> something).

To ensure soundness, the programmer must ensure that the fresh atom does not escape the body of the with_fresh block. See the documentation of with_fresh for examples of what is and is not permitted, and a more precise statement of the correctness condition.

Occasionally, it can be useful to generate a globally fresh atom. This is done within the IO monad, and therefore, the function fresh (and its friends) have no corresponding correctness condition as for with_fresh.

These functions are primarily intended for testing. They give the user a convenient way to generate fresh names in the read-eval-print loop, for example:

>>> a <- fresh :: IO Atom
>>> b <- fresh :: IO Atom
>>> a.b.(a,b)
x . y . (x,y)

These functions should rarely be used in programs. Normally you should use with_fresh instead of fresh, to generate a fresh atom in a specific scope for a specific purpose. If you find yourself generating a lot of global names and not binding them, consider whether the Nominal library is the wrong tool for your purpose. Perhaps you should use Data.Unique instead?

Informally, a type of nominal if if is aware of the existence of atoms, and knows what to do in case an atom needs to be renamed. More formally, a type is nominal if it is acted upon by the group of finitely supported permutations of atoms. Ideally, all types are nominal.

When using the Nominal library, all types whose elements can occur in the scope of a binder must be instances of the Nominal type class. Fortunately, in most cases, new instances of Nominal can be derived automatically.

The Bindable class contains things that can be abstracted by binders (sometimes called patterns). In addition to atoms, this also includes pairs of atoms, lists of atoms, and so on. In most cases, new instances of Bindable can be derived automatically.

The printing of nominal values requires concrete names for the bound variables to be chosen in such a way that they do not clash with the names of any free variables, constants, or other bound variables. This requires the ability to compute the set of free atoms (and constants) of a term. We call this set the support of a term.

Our mechanism for pretty-printing nominal values consists of two things: the type class NominalSupport, which represents terms whose support can be calculated, and the function open_for_printing, which handles choosing concrete names for bound variables.

In addition to this general-purpose mechanism, there is also the NominalShow type class, which is analogous to Show and provides a default representation of nominal terms.

The NominalShow class is analogous to Haskell's standard Show class, and provides a default method for converting elements of nominal datatypes to strings. The function nominal_show is analogous to show. In most cases, new instances of NominalShow can be derived automatically.

In many cases, instances of Nominal, NominalSupport, NominalShow, and/or Bindable can be derived automatically, using the generic "deriving" mechanism. To do so, enable the language options DeriveGeneric and DeriveAnyClass, and derive a Generic instance in addition to whatever other instances you want to derive.

Example 1: Trees

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

data MyTree a = Leaf | Branch a (MyTree a) (MyTree a)
  deriving (Generic, Nominal, NominalSupport, NominalShow, Show, Bindable)

Example 2: Untyped lambda calculus

Note that in the case of lambda terms, it does not make sense to derive a Bindable instance, as lambda terms cannot be used as binders.

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
  deriving (Generic, Nominal, NominalSupport, NominalShow, Show)

There are some cases where instances of Nominal and the other type classes cannot be automatically derived. These include: (a) base types such as Double, (b) types that are not generic, such as certain GADTs, and (c) types that require a custom Nominal instance for some other reason (advanced users only!). In such cases, instances must be defined explicitly. The follow examples explain how this is done.

A type is basic or non-nominal if its elements cannot contain atoms. Typical examples are base types such as Integer and Bool, and other types constructed exclusively from them, such as [Integer] or Bool -> Bool.

For basic types, it is very easy to define instances of Nominal, NominalSupport, NominalShow, and Bindable: for each class method, we provide a corresponding helper function whose name starts with basic_ that does the correct thing. These functions can only be used to define instances for non-nominal types.

Example

We show how the nominal type class instances for the base type Double were defined.

instance Nominal Double where
  (•) = basic_action

instance NominalSupport Double where
  support = basic_support

instance NominalShow Double where
  showsPrecSup = basic_showsPrecSup

instance Bindable Double where
  binding = basic_binding

An alternative to defining new basic type class instances is to wrap the corresponding types in the constructor Basic. The type Basic MyType is isomorphic to MyType, and is automatically an instance of the relevant type classes.

For recursive types, instances for nominal type classes can be defined by passing the relevant operations recursively down the term structure. We will use the type MyTree as a running example.

data MyTree a = Leaf | Branch a (MyTree a) (MyTree a)

Nominal

To define an instance of Nominal, we must specify how permutations of atoms act on the elements of the type. For example:

instance (Nominal a) => Nominal (MyTree a) where
  π • Leaf = Leaf
  π • (Branch a l r) = Branch (π • a) (π • l) (π • r)

NominalSupport

To define an instance of NominalSupport, we must compute the support of each term. This can be done by applying support to a tuple or list (or combination thereof) of immediate subterms. For example:

instance (NominalSupport a) => NominalSupport (MyTree a) where
  support Leaf = support ()
  support (Branch a l r) = support (a, l, r)

Here is another example showing additional possibilities:

instance NominalSupport Term where
  support (Var x) = support x
  support (App t s) = support (t, s)
  support (Abs t) = support t
  support (MultiApp t args) = support (t, [args])
  support Unit = support ()

If your nominal type uses additional constants, identifiers, or reserved keywords that are not implemented as Atoms, but whose names you don't want to clash with the names of bound variables, declare them with Literal applied to a string:

  support (Const str) = support (Literal str)

NominalShow

Custom NominalShow instances require a definition of the showsPrecSup function. This is very similar to the showsPrec function of the Show class, except that the function takes the term's support as an additional argument. Here is how it is done for the MyTree datatype:

instance (NominalShow a) => NominalShow (MyTree a) where
  showsPrecSup sup d Leaf = showString "Leaf"
  showsPrecSup sup d (Branch a l r) =
    showParen (d > 10) $
      showString "Branch "
      ∘ showsPrecSup sup 11 a
      ∘ showString " "
      ∘ showsPrecSup sup 11 l
      ∘ showString " "
      ∘ showsPrecSup sup 11 r

Bindable

The Bindable class requires a function binding, which maps a term to the corresponding pattern. The recursive cases use the Applicative structure of the NominalPattern type.

Here is how we could define a Bindable instance for the MyTree type. We use the "applicative do" notation for convenience, although this is not essential.

{-# LANGUAGE ApplicativeDo #-}

instance (Bindable a) => Bindable (MyTree a) where
  binding Leaf = do
    pure Leaf
  binding (Branch a l r) = do
    a' <- binding a
    l' <- binding l
    r' <- binding r
    pure (Branch a' l' r')

To embed non-binding sites within a pattern, replace binding by nobinding in the recursive call. For further discussion of non-binding patterns, see also NoBind. Here is an example:

{-# LANGUAGE ApplicativeDo #-}

data HalfBinder a b = HalfBinder a b

instance (Bindable a) => Bindable (HalfBinder a b) where
  binding (HalfBinder a b) = do
    a' <- binding a
    b' <- nobinding b
    pure (HalfBinder a' b')

The effect of this is that the a is bound and b is not bound in the term (HalfBinder a b).t,