| 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.
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.
- 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
- 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 NominalPattern a
- newtype NoBind t = NoBind t
- nobinding :: a -> NominalPattern 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 -> NominalPattern a
- (∘) :: (b -> c) -> (a -> b) -> a -> c
- module Nominal.Generics
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 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
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 datatype is a type that is aware of the existence of atoms. TheBindoperation 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
(, is opened: this means that a fresh name y and a term s are generated such that body = yBindAtomTerm).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
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 the
documentation of with_fresh 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. For
soundness, the programmer must ensure that the atom created does
not escape the body of the with_fresh block. Thus, 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)
Technically, the correctness condition is that in an application
with_fresh (\a -> body),
we must have a # body (see [Pitts 2002] for more details on what this means). Haskell does not enforce this restriction, but if a program violates it, referential transparency may not hold, which may, in the worst case, lead to unsound compiler optimizations and undefined behavior.
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.
This function is subject to the same correctness condition as
with_fresh.
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.
This function is subject to the same correctness condition as
with_fresh.
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) 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?
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, and Float, 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 atom 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 2002].
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 # | |
(.) :: (Bindable a, Nominal t) => a -> t -> Bind a t infixr 5 Source #
Atom abstraction: 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 binder 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 a
is already defined to be some atom. Thus, binders are often used
in a context of with_fresh or open, such as the following:
with_fresh (\a -> a.a)
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 #
Destructor for atom abstraction. In an ideal programming idiom, we would be able to define a function on atom abstractions by pattern matching like this:
f (a.s) = body.
Haskell doesn't let us provide this syntax, but using the open
function, we can equivalently write:
f t = open t (\a s -> body).
Each time an abstraction is opened, a is guaranteed to be a fresh
atom. To guarantee soundness (referential transparency and
equivariance), the body is subject to the same restriction as
with_fresh, namely, a must be fresh for the body (in symbols
a # body).
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:
open (merge body body') (\x (e,s) -> .....)
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 x [A]S = [A](T x 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 atom 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 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.
class Nominal a => Bindable a where Source #
A type is Bindable if its elements can be abstracted by
binders. Such elements are also called 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 -> NominalPattern a Source #
A function that maps a term to a pattern. New patterns can be
constructed using the Applicative structure of NominalPattern.
See "Defining custom instances" for examples.
binding :: (Generic a, GBindable (Rep a)) => a -> NominalPattern a Source #
A function that maps a term to a pattern. New patterns can be
constructed using the Applicative structure of NominalPattern.
See "Defining custom instances" for examples.
Instances
| Bindable Bool Source # | |
| Bindable Char Source # | |
| Bindable Double Source # | |
| Bindable Float Source # | |
| Bindable Int Source # | |
| Bindable Integer Source # | |
| Bindable () Source # | |
| Bindable Atom Source # | |
| Bindable Literal Source # | |
| Bindable a => Bindable [a] Source # | |
| Bindable (Basic t) Source # | |
| Nominal t => Bindable (NoBind t) Source # | |
| AtomKind a => Bindable (AtomOfKind a) Source # | |
| (Bindable a, Bindable b) => Bindable (a, b) Source # | |
| (Bindable a, Bindable b, Bindable c) => Bindable (a, b, c) Source # | |
| (Bindable a, Bindable b, Bindable c, Bindable d) => Bindable (a, b, c, d) Source # | |
| (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e) => Bindable (a, b, c, d, e) Source # | |
| (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f) => Bindable (a, b, c, d, e, f) Source # | |
| (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f, Bindable g) => Bindable (a, b, c, d, e, f, g) Source # | |
data NominalPattern a Source #
A representation of patterns of type a. This is an abstract
type with no exposed structure. The only way to construct a value
of type NominalPattern 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 -> NominalPattern a Source #
Constructor for non-binding patterns. This can be used to mark
non-binding subterms when defining a Bindable instance. See
"Defining custom instances" for examples.
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.
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)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 -> NominalPattern 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 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,
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.Generics