Safe Haskell | None |
---|---|

Language | Haskell2010 |

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.

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.

- data Atom
- class AtomKind a where
- data AtomOfKind a
- class (Nominal a, NominalSupport a, Eq a, Ord a, Show a, Bindable a) => Atomic a
- type NameSuggestion = [String]
- with_fresh :: Atomic a => (a -> t) -> t
- with_fresh_named :: Atomic a => String -> (a -> t) -> t
- with_fresh_namelist :: Atomic a => NameSuggestion -> (a -> t) -> t
- fresh :: Atomic a => IO a
- fresh_named :: Atomic a => String -> IO a
- fresh_namelist :: Atomic a => NameSuggestion -> IO a
- class Nominal t where
- data NominalPermutation
- newtype Basic t = Basic t
- data Bind a t
- (.) :: (Bindable a, Nominal t) => a -> t -> Bind a t
- pattern (:.) :: (Nominal b, Bindable a) => a -> b -> Bind a b
- abst :: (Bindable a, Nominal t) => a -> t -> Bind a t
- open :: (Bindable a, Nominal t) => Bind a t -> (a -> t -> s) -> s
- merge :: (Atomic a, Nominal t, Nominal s) => Bind a t -> Bind a s -> Bind a (t, s)
- bind :: (Atomic a, Nominal t) => (a -> t) -> Bind a t
- bind_named :: (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t
- bind_namelist :: (Atomic a, Nominal t) => NameSuggestion -> (a -> t) -> Bind a t
- class Nominal a => Bindable a where
- data NominalBinder a
- newtype NoBind t = NoBind t
- nobinding :: a -> NominalBinder a
- open_for_printing :: (Bindable a, Nominal t) => Support -> Bind a t -> (a -> t -> Support -> s) -> s
- class Nominal t => NominalSupport t where
- data Support
- newtype Literal = Literal String
- class NominalSupport t => NominalShow t where
- nominal_show :: NominalShow t => t -> String
- nominal_showsPrec :: NominalShow t => Int -> t -> ShowS
- basic_action :: NominalPermutation -> t -> t
- basic_support :: t -> Support
- basic_showsPrecSup :: Show t => Support -> Int -> t -> ShowS
- basic_binding :: a -> NominalBinder a
- (∘) :: (b -> c) -> (a -> b) -> a -> c
- module Nominal.Generic

# Overview

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 z (Var x) | x == z = m | otherwise = Var x subst m z (App t s) = App (subst m z t) (subst m z s) subst m z (Abs (x :. t)) = Abs (x . subst m z t)

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`(`

is defined by the Nominal library and represents pairs (`Bind`

`Atom`

Term)*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 type is a type that is aware of the existence of atoms. The`Bind`

operation can only be applied to nominal types, because otherwise alpha-equivalence would not make sense. - The substitution function inputs a term
*m*, a variable*z*, and a term*t*, and outputs the term*t*[*m*/*z*] that is obtained from*t*by replacing all occurrences of the variable*z*by*m*. The clauses for variables and application are straightforward. Note that atoms can be compared for equality. In the clause for abstraction,`(x :. t)`

is an*abstraction pattern*. It matches any abstraction of the form*y*`.`

*s*, which is of type`(`

. Moreover, each time the abstraction pattern is used, a`Bind`

`Atom`

Term)*fresh*name*x*and a term*t*are generated such that*x*`.`

*t*=*y*`.`

*s*. Since the name*x*resulting from the pattern matching is always guaranteed to be fresh, the substitution can be recursively applied to*t*without the possibility that*x*may be captured in*m*or that*x*=*z*. In other words, abstraction patterns implement what is informally known as*Barendregt's variable convention*, i.e., the names of bound variables are always assumed to be fresh.

See the folder "examples" for additional examples.

# Atoms

## Atom types

*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`

.

An atom is a globally unique, opaque value.

Eq Atom Source # | |

Ord Atom Source # | User code should |

Show Atom Source # | |

Nominal Atom Source # | |

NominalSupport Atom Source # | |

Bindable Atom Source # | |

Atomic Atom Source # | |

NominalShow Atom Source # | |

class AtomKind a where Source #

An atom kind is a type-level constant (typically an empty type)
that is an instance of the `AtomKind`

class. An atom kind is
optionally equipped with a list of suggested names for this kind of
atom. For example:

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

data TypeName instance AtomKind TypeName where suggested_names _ = ["a", "b", "c"]

It is possible to have infinitely many atom kinds, for example:

data Zero data Succ a instance AtomKind Zero instance AtomKind (Succ a)

Then Zero, Succ Zero, Succ (Succ Zero), etc., will all be atom kinds.

suggested_names :: a -> NameSuggestion Source #

An optional list of default names for this kind of atom.

expand_names :: a -> NameSuggestion -> [String] Source #

An optional function for generating infinitely many distinct
names from a finite list of suggestions. The default behavior is
to append numerical subscripts. For example, the names
`[x, y, z]`

are by default expanded to ```
[x, y, z, x₁, y₁, z₁,
x₂, y₂, …]
```

, using Unicode for the subscripts. To use a a
different naming convention, redefine `expand_names`

.

It is not strictly necessary for all of the returned names to be distinct; it is sufficient that there are infinitely many distinct ones.

Example: the following generates new variable names by appending primes instead of subscripts:

expand_names _ xs = ys where ys = xs ++ map (++ "'") ys

data AtomOfKind a Source #

The type of atoms of a given kind. For example:

type Variable = AtomOfKind VarName type Type = AtomOfKind TypeName

Eq (AtomOfKind a) Source # | |

Ord (AtomOfKind a) Source # | |

AtomKind a => Show (AtomOfKind a) Source # | |

Generic (AtomOfKind a) Source # | |

AtomKind a => Nominal (AtomOfKind a) Source # | |

AtomKind a => NominalSupport (AtomOfKind a) Source # | |

AtomKind a => Bindable (AtomOfKind a) Source # | |

AtomKind a => Atomic (AtomOfKind a) Source # | |

AtomKind a => NominalShow (AtomOfKind a) Source # | |

type Rep (AtomOfKind a) Source # | |

class (Nominal a, NominalSupport a, Eq a, Ord a, Show a, Bindable a) => Atomic a Source #

A type class for atom types.

The suggested way to define a 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 new atoms can be provided. (These
will be used as the names of bound variables unless otherwise
specified). Then `AtomOfKind`

*t* is a new type of atoms.

data VarName instance AtomKind VarName where suggested_names = ["x", "y", "z"] newtype Variable = AtomOfKind VarName

type NameSuggestion = [String] Source #

A name suggestion is a list of possible names. When an atom must
be renamed, the first useable name from the list is chosen. If the
list is finite and contains no useable names, then additional names
will be generated by appending numerical subscripts. To override
this behavior, redefine `expand_names`

for the given
`AtomKind`

instance, or specify an infinite list of names.

## Creation of fresh atoms in a scope

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
"Pitts's freshness condition" for examples
of what is and is not permitted, and a more precise statement of
the correctness condition.

with_fresh :: Atomic a => (a -> t) -> t Source #

Perform a computation in the presence of a fresh atom.

The correct use of this function is subject to Pitts's freshness condition. Thus, for example, the following uses are permitted:

with_fresh (\a -> f a == g a) with_fresh (\a -> a . f a b c)

Here is an example of what is *not* permitted:

with_fresh (\a -> a)

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

with_fresh_named :: Atomic a => String -> (a -> t) -> t Source #

A version of `with_fresh`

that permits a suggested name to be
given to the atom. The name is only a suggestion, and will be
changed, if necessary, to avoid clashes.

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

with_fresh_namelist :: Atomic a => NameSuggestion -> (a -> t) -> t Source #

A version of `with_fresh`

that permits a list of suggested names
to be specified. The first suitable name in the list will be used
if possible.

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

## Creation of fresh atoms globally

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) are *not* subject to
Pitts's freshness condition.

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`

`>>>`

x . y . (x,y)`a.b.(a,b)`

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?

fresh_named :: Atomic a => String -> IO a Source #

A version of `fresh`

that that permits a suggested name to be
given to the atom. The name is only a suggestion, and will be
changed, if necessary, when the atom is bound.

fresh_namelist :: Atomic a => NameSuggestion -> IO a Source #

A version of `with_fresh`

that permits a list of suggested names
to be specified. The first suitable name in the list will be used
if possible.

# Nominal types

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.

class Nominal t where Source #

A type is nominal if the group of finitely supported permutations of atoms acts on it.

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.

(•) :: NominalPermutation -> t -> t Source #

Apply a permutation of atoms to a term.

(•) :: (Generic t, GNominal (Rep t)) => NominalPermutation -> t -> t Source #

Apply a permutation of atoms to a term.

data NominalPermutation Source #

The group of finitely supported permutations on atoms. This is an abstract type with no exposed structure.

A *basic* or *non-nominal* type is a type whose elements cannot
contain any atoms. Typical examples are base types, such as `Integer`

or `Bool`

, and other types constructed exclusively from them,
such as `[`

or `Integer`

]

. On such types, the
nominal structure is trivial, i.e., `Bool`

-> `Bool`

`π • `

for all *x* = *x**x*.

For convenience, we define `Basic`

as a wrapper around such types,
which will automatically generate appropriate instances of
`Nominal`

, `NominalSupport`

, `NominalShow`

, and `Bindable`

. You can
use it, for example, like this:

type Term = Var Atom | Const (Basic Int) | App Term Term

Some common base types, including `Bool`

, `Char`

, `Int`

, `Integer`

,
`Double`

, `Float`

, and `Ordering`

are already instances of the
relevant type classes, and do not need to be wrapped in `Basic`

.

The use of `Basic`

can sometimes have a performance advantage. For
example,

is a more efficient `Basic`

`String`

`Nominal`

instance
than `String`

. Although they are semantically equivalent, the use
of `Basic`

prevents having to traverse the string to check each
character for atoms that are clearly not there.

Basic t |

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

(Nominal a, Nominal t, Eq a, Eq t) => Eq (Bind a t) Source # | |

(Bindable a, Nominal t) => Nominal (Bind a t) Source # | |

(Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) Source # | |

(Bindable a, NominalShow a, NominalShow t) => NominalShow (Bind a t) Source # | |

## Basic operations

(.) :: (Bindable a, Nominal t) => a -> t -> Bind a t infixr 5 Source #

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`

.

pattern (:.) :: (Nominal b, Bindable a) => a -> b -> Bind a b infixr 5 Source #

A pattern matching syntax for abstractions. The pattern
`(x :. t)`

is called an *abstraction pattern*. It matches any term
of type `(`

. The result of matching the pattern
`Bind`

*a* *b*)`(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.

abst :: (Bindable a, Nominal t) => a -> t -> Bind a t Source #

An alternative non-infix notation for `(`

`.`

`)`

. This can be
useful when using qualified module names, because "̈`Nominal..`

" is not
valid syntax.

open :: (Bindable a, Nominal t) => Bind a t -> (a -> t -> s) -> s Source #

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.

merge :: (Atomic a, Nominal t, Nominal s) => Bind a t -> Bind a s -> Bind a (t, s) Source #

Sometimes, it is necessary to open two abstractions, using the
*same* fresh name for both of them. An example of this is the
typing rule for lambda abstraction in dependent type theory:

Gamma, x:t |- e : s ------------------------------------ Gamma |- Lam (x.e) : Pi t (x.s)

In the bottom-up reading of this rule, we are given the terms `Lam`

*body* and `Pi`

*t* *body'*, and we require a fresh name *x* and
terms *e*, *s* such that *body* = (*x*.*e*) and
*body'* = (*x*.*s*). Crucially, the same atom *x* should be used
in both *e* and *s*, because we subsequently need to check that *e*
has type *s* in some scope that is common to *e* and *s*.

The `merge`

primitive permits us to deal with such situations. Its
defining property is

merge (x.e) (x.s) = (x.(e,s)).

We can therefore solve the above problem:

let (x :. (e,s)) = merge body body' in ....

Moreover, the `merge`

primitive can be used to define other
merge-like functionality. For example, it is easy to define a
function

merge_list :: (Atomic a, Nominal t) => [Bind a t] -> Bind a [t]

in terms of it.

Semantically, the `merge`

operation implements the isomorphism of
nominal sets [*A*]*T* × [*A*]*S* = [*A*](*T* × *S*).

If *x* and *y* are atoms with user-suggested concrete names and

(z.(t',s')) = merge (x.t) (y.s),

then *z* will be preferably given the concrete name of *x*, but the
concrete name of *y* will be used if the name of *x* would cause a
clash.

## Convenience functions

bind :: (Atomic a, Nominal t) => (a -> t) -> Bind a t Source #

A convenience function for constructing binders. We can write

bind (\x -> t)

to denote the abstraction (x.t), where *x* is a fresh atom.

bind_named :: (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t Source #

A version of `bind`

that also takes a suggested name for the bound atom.

bind_namelist :: (Atomic a, Nominal t) => NameSuggestion -> (a -> t) -> Bind a t Source #

A version of `bind`

that also take a list of suggested names for
the bound atom.

## The Bindable class

The `Bindable`

class contains things that can be abstracted. More
precisely, *x* is *bindable*, or a *binder*, if abstractions of the
form *x*.*t* can be formed. Sometimes binders are also called
*patterns*, but we avoid this terminology here, to avoid confusion
with pattern matching, which is a separate operation from binding.

In addition to atoms, binders include pairs of atoms, lists of
atoms, and so on. In most cases, new instances of `Bindable`

can
be derived automatically.

For example, `(`

binds a pair of atoms in *x*,*y*).*t**t*. It is
roughly equivalent to

, except that it is of type
*x*.*y*.*t*`Bind`

(`Atom`

, `Atom`

) *t* instead of
`Bind`

`Atom`

(`Bind`

`Atom`

*t*).

When a binder contains repeated atoms, they are regarded as
distinct, and are bound one at a time, in some fixed but
unspecified order. For example, `(`

is equivalent
to either *x*,*x*).(*x*,*x*)`(`

or *x*,*y*).(*x*,*x*)`(`

. Which of
the two alternatives is chosen is implementation specific and user
code should not rely on the order of abstractions in such cases.*x*,*y*).(*y*,*y*)

class Nominal a => Bindable a where Source #

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.

binding :: a -> NominalBinder a Source #

A function that maps a term to a binder. New binders can be
constructed using the `Applicative`

structure of `NominalBinder`

.
See "Defining custom instances" for examples.

binding :: (Generic a, GBindable (Rep a)) => a -> NominalBinder a Source #

A function that maps a term to a binder. New binders can be
constructed using the `Applicative`

structure of `NominalBinder`

.
See "Defining custom instances" for examples.

data NominalBinder a Source #

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`

.

## Non-binding patterns

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

is alpha-equivalent to
*x*.(*x*,
`NoBind`

*x*)

. Another way to say this is that *y*.(*y*, `NoBind`

*y*)`NoBind`

has a special behavior on the left, but not on the right of a dot.

NoBind t |

nobinding :: a -> NominalBinder a Source #

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.

# Pitt's freshness condition

To ensure soundness (referential transparency and equivariance),
all functions that generate a fresh name in a local scope must
satisfy a certain condition known as Pitts's *freshness*
*condition* *for* *binders* (see Chapter 4.5 of
[Pitts 2013]).

Informally, this condition means that the fresh atom must not escape the body of the block in which it was created. Thus, for example, the following are permitted:

with_fresh (\a -> f a == g a) with_fresh (\a -> a . f a b c)

Here is an example of what is *not* permitted:

with_fresh (\a -> a)

In more technical terms, the correctness condition is that in an application

with_fresh (\a -> body),

we must have *a* # *body*. See [Pitts 2003] or
[Pitts 2013] for more information on what this
means.

The following exported functions are subject to the freshness condition:
`with_fresh`

,
`with_fresh_named`

,
`with_fresh_namelist`

,
`open`

,
`open_for_printing`

,
as well as the use of abstraction patterns `(`

`:.`

`)`

.

Haskell does not enforce this restriction. But if a program
violates it, referential transparency may not hold, which could in
theory lead to unsound compiler optimizations and undefined
behavior. Here is an example of an incorrect use of `with_fresh`

that violates referential transparency:

`>>>`

False`(with_fresh id :: Atom) == (with_fresh id :: Atom)`

# Printing of nominal values

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.

open_for_printing :: (Bindable a, Nominal t) => Support -> Bind a t -> (a -> t -> Support -> s) -> s Source #

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.

class Nominal t => NominalSupport t where Source #

`NominalSupport`

is a subclass of `Nominal`

consisting of those
types for which the support can be calculated. With the notable
exception of function types, most `Nominal`

types are also
instances of `NominalSupport`

.

In most cases, instances of `NominalSupport`

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.

support :: t -> Support Source #

Compute a set of atoms and strings that should not be used as the names of bound variables.

support :: (Generic t, GNominalSupport (Rep t)) => t -> Support Source #

Compute a set of atoms and strings that should not be used as the names of bound variables.

A wrapper around strings. This is used to denote any literal
strings whose values should not clash with the names of bound
variables. For example, if a term contains a constant symbol *c*,
the name *c* should not also be used as the name of a bound
variable. This can be achieved by marking the string with
`Literal`

, like this

data Term = Var Atom | Const (Literal String) | ...

Another way to use `Literal`

is in the definition of custom
`NominalSupport`

instances. See
"Defining custom instances" for an example.

# The NominalShow class

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.

class NominalSupport t => NominalShow t where Source #

`NominalShow`

is similar to `Show`

, but with support for renaming
of bound variables. With the exception of function types, most
`Nominal`

types are also instances of `NominalShow`

.

In most cases, instances of `NominalShow`

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.

showsPrecSup :: Support -> Int -> t -> ShowS Source #

A nominal version of `showsPrec`

. This function takes as its
first argument the support of *t*. This is then passed into the
subterms, making printing O(*n*) instead of O(*n*²).

It is recommended to define a `NominalShow`

instance, rather than
a `Show`

instance, for each nominal type, and then either
automatically derive the `Show`

instance, or define it using
`nominal_showsPrec`

. For example:

instance Show MyType where showsPrec = nominal_showsPrec

Please note: in defining `showsPrecSup`

, neither `show`

nor `nominal_show`

should be used for the recursive cases, or
else the benefit of fast printing will be lost.

nominal_showList :: Support -> [t] -> ShowS Source #

The method `nominal_showList`

is provided to allow the
programmer to give a specialized way of showing lists of values,
similarly to `showList`

. The principal use of this is in the
`NominalShow`

instance of the `Char`

type, so that strings are
shown in double quotes, rather than as character lists.

showsPrecSup :: (Generic t, GNominalShow (Rep t)) => Support -> Int -> t -> ShowS Source #

A nominal version of `showsPrec`

. This function takes as its
first argument the support of *t*. This is then passed into the
subterms, making printing O(*n*) instead of O(*n*²).

It is recommended to define a `NominalShow`

instance, rather than
a `Show`

instance, for each nominal type, and then either
automatically derive the `Show`

instance, or define it using
`nominal_showsPrec`

. For example:

instance Show MyType where showsPrec = nominal_showsPrec

Please note: in defining `showsPrecSup`

, neither `show`

nor `nominal_show`

should be used for the recursive cases, or
else the benefit of fast printing will be lost.

nominal_show :: NominalShow t => t -> String Source #

Like `show`

, but for nominal types. Normally all instances of
`NominalShow`

are also instances of `Show`

, so `show`

can usually
be used instead of `nominal_show`

.

nominal_showsPrec :: NominalShow t => Int -> t -> ShowS Source #

This function can be used in the definition of `Show`

instances for nominal types, like this:

instance Show MyType where showsPrec = nominal_showsPrec

# Deriving generic instances

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)

## Deriving instances for existing types

Sometimes it may be necessary to derive an instance of `Nominal`

or
one of the other type classes for an already existing datatype.
This can be done by specifying an instance declaration without any
body. For example, here is how the instances would be specified for
the `Maybe`

type:

instance (Nominal a) => Nominal (Maybe a) instance (NominalSupport a) => NominalSupport (Maybe a) instance (NominalShow a) => NominalShow (Maybe a) instance (Bindable a) => Bindable (Maybe a)

# Defining custom instances

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.

## Basic types

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
`[`

or `Integer`

]

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

is isomorphic to `Basic`

MyType`MyType`

, and is automatically an
instance of the relevant type classes.

basic_action :: NominalPermutation -> t -> t Source #

A helper function for defining `Nominal`

instances
for non-nominal types.

basic_support :: t -> Support Source #

A helper function for defining `NominalSupport`

instances
for non-nominal types.

basic_showsPrecSup :: Show t => Support -> Int -> t -> ShowS Source #

A helper function for defining `NominalShow`

instances
for non-nominal types. This requires an existing `Show`

instance.

basic_binding :: a -> NominalBinder a Source #

A helper function for defining `Bindable`

instances
for non-nominal types.

## Recursive types

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 `Atom`

s, 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 binder. The recursive cases use the
`Applicative`

structure of the `NominalBinder`

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 binder, replace `binding`

by
`nobinding`

in the recursive call. For further discussion of
non-binding binders, 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*

# Miscellaneous

(∘) :: (b -> c) -> (a -> b) -> a -> c Source #

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.

module Nominal.Generic

We re-export the Generic type class for convenience, so that users do not have to import GHC.Generics.

# Related Work

[Cheney 2005] and [Weirich, Yorgey, and Sheard 2011] describe Haskell implementations of binders using generic programming. While there are many similarities, these implementations differ from the Nominal library in several respects.

*Higher-order nominal types.*Weirich et al.'s "Unbound" library is based on the locally nameless approach, and therefore function types cannot appear under binders. Although Cheney's library is based on the nominal approach, it requires the relation*a*#*t*to be decidable for all nominal types, and therefore function types cannot be nominal. In the Nominal library, function types are nominal and can occur under binders.*Freshness monad vs. scoped freshness.*Both the libraries of Cheney and Weirich et al. use a freshness monad; all operations that create fresh names (such as`open`

) take place in this monad. While this is semantically sound, it has some disadvantages: (a) Every computation with binders must be threaded through the monad. When this is done deeply within a nested expression, this gives rise to an unnatural programming style. (b) Computations must be threaded through the monad even though the user is aware, in the relevant use cases, that the defined functions are in fact pure (i.e., the freshness state is inessential). (c) The use of a freshness monad precludes the use of abstraction patterns. The Nominal library uses*scoped freshness*instead of a freshness monad. This lends itself to a more natural programming style. The price to pay for this is that the user must ensure that fresh names are only used in the local scope in which they were generated. Formally, the user must adhere to a correctness criterion (Pitts's freshness condition) that cannot be checked by the compiler.*Simplicity.*Weirich et al.'s "Unbound" library has many advanced features, such as set-binders, recursive patterns, nested bindings, and an exposed interface for certain low-level atom manipulations. The Nominal library currently lacks these features. Instead, it focuses on ease of use and an efficient implementation of a core set of functionalities. The hope is that these are sufficiently general and robust to permit more advanced features to be implemented in user space on top of the library. It remains to be seen whether this is the case.

[Shinwell, Pitts, and Gabbay 2003] describe FreshML, an extension of ML with binders. This was later implemented by [Shinwell and Pitts 2005] as an extension of Objective Caml. The functionality and philosophy of the Nominal library is essentially similar to that of FreshML. Since ML is a side-effecting language, the issue of a freshness monad does not arise, but users must still adhere to Pitts's freshness condition to guarantee that programs define equivariant functions. However, since ML lacks Haskell's support for generic programming and custom patterns, the FreshML implementation requires patching the compiler. It is therefore harder to deploy than a library.

# Acknowledgements

Thanks to Frank Fu for stress-testing the library and insisting on efficiency. Thanks to Andrew Pitts for helpful suggestions, and especially for nudging me to implement abstraction patterns.

# References

- J. Cheney. "Scrap your nameplate (functional pearl)". Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), pages 180–191, 2005.

- M. J. Gabbay and A. M. Pitts. "A new approach to abstract syntax involving binders". Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pages 214–224, 1999.

- M. Pitts. "Nominal logic, a first order theory of names and binding". Information and Computation 186:165–193, 2003.

- M. Pitts. "Nominal sets: names and symmetry in computer science". Cambridge University Press, 2013.

- M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. "FreshML: programming with binders made simple". Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), pages 263–274, 2003.

- M. R. Shinwell and A. M. Pitts. "Fresh Objective Caml user manual". Technical Report 621, University of Cambridge Computer Laboratory, February 2005. Implementation at https://www.cl.cam.ac.uk/~amp12/fresh-ocaml/.

- S. Weirich, B. A. Yorgey, and T. Sheard. "Binders unbound". Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), pages 333–345, 2011. Implementation at http://hackage.haskell.org/package/unbound.