| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Nominal
Contents
Description
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
DeriveGenericandDeriveAnyClass, 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
Termof untyped lambda terms. Here,Atomis 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 (a,t) of an atom and a term, modulo alpha-equivalence. We write aBindAtomTerm).t to denote such an alpha-equivalence class of pairs. - The next line declares that
Termis a nominal type, by deriving an instance of the type classNominal(and alsoGeneric, which enables the magic that allowsNominalinstances to be derived automatically). In a nutshell, a nominal type is a type that is aware of the existence of atoms. TheBindoperation 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 fresh name x and a term t are generated such that xBindAtomTerm).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.
Instances
| Eq Atom Source # | |
| Ord Atom Source # | User code should not explicitly compare atoms for relative
ordering, because this is not referentially transparent (can be
unsound). However, we define an |
| 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.
Methods
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
Instances
| 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>>>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?
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.
Methods
(•) :: 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.
Instances
data NominalPermutation Source #
The group of finitely supported permutations on atoms. This is an abstract type with no exposed structure.
Instances
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]Bool -> Boolπ • x = x for all 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, Basic StringNominal 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.
Constructors
| 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].
Instances
| (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, (x,y).t binds a pair of atoms in t. It is
roughly equivalent to x.y.t, except that it is of type
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, (x,x).(x,x) is equivalent
to either (x,y).(x,x) or (x,y).(y,y). Which of
the two alternatives is chosen is implementation specific and user
code should not rely on the order of abstractions in such cases.
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.
Methods
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.
Instances
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.
Instances
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 x.(x,
is alpha-equivalent to
NoBind x)y.(y, . Another way to say this is that NoBind y)NoBind
has a special behavior on the left, but not on the right of a dot.
Constructors
| NoBind t |
Instances
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:
>>>(with_fresh id :: Atom) == (with_fresh id :: Atom)False
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.
Methods
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.
Instances
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.
Methods
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.
Instances
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
Basic MyTypeMyType, 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 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 rBindable
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.