License | BSD-like (see LICENSE) |
---|---|

Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |

Stability | experimental |

Portability | GHC only (-XKitchenSink) |

Safe Haskell | None |

Language | Haskell2010 |

A generic implementation of standard functions dealing with names and binding structure (alpha equivalence, free variable calculation, capture-avoiding substitution, name permutation, ...) using a locally nameless representation.

Normal users of this library should only need to import this module. In particular, this module is careful to export only an abstract interface with various safety guarantees. Power users who wish to have access to the internals of the library (at the risk of shooting oneself in the foot) can directly import the various implementation modules such as Unbound.LocallyNameless.Name and so on.

*Ten-second tutorial*: use the type combinators `Bind`

, `Embed`

,
`Rebind`

, `Rec`

, `TRec`

, and `Shift`

to specify the binding
structure of your data types. Then use Template Haskell to derive
generic representations for your types:

$(derive [''Your, ''Types, ''Here])

Finally, declare `Alpha`

and `Subst`

instances for your types.
Then you can go to town using all the generically-derived
operations like `aeq`

, `fv`

, `subst`

, and so on.

For more information, see the more in-depth literate Haskell
tutorial in the `tutorial`

directory (which can be obtained as part
of the library source package: `cabal unpack unbound`

) and the
examples in the `example`

directory.

See also: Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.
*Binders Unbound*. ICFP'11, September 2011, Tokyo, Japan. http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf.

## Synopsis

- data Name a
- data AnyName = Rep a => AnyName (Name a)
- integer2Name :: Rep a => Integer -> Name a
- string2Name :: Rep a => String -> Name a
- s2n :: Rep a => String -> Name a
- makeName :: Rep a => String -> Integer -> Name a
- name2Integer :: Name a -> Integer
- name2String :: Name a -> String
- anyName2Integer :: AnyName -> Integer
- anyName2String :: AnyName -> String
- translate :: Rep b => Name a -> Name b
- toSortedName :: Rep a => AnyName -> Maybe (Name a)
- type Bind p t = GenBind StrictOrder StrictCard p t
- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t
- setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t
- setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t
- unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p, t)
- lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c
- unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1, t1, p2, t2))
- unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (Maybe (p1, t1, p2, t2, p3, t3))
- lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m r
- lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> (Maybe (p1, t1, p2, t2, p3, t3) -> m r) -> m r
- unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (p1, t1, p2, t2)
- unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (p1, t1, p2, t2, p3, t3)
- lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> ((p1, t1, p2, t2) -> m r) -> m r
- lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> ((p1, t1, p2, t2, p3, t3) -> m r) -> m r
- newtype Embed t = Embed t
- embed :: IsEmbed e => Embedded e -> e
- unembed :: IsEmbed e => e -> Embedded e
- data Rebind p1 p2
- rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
- unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
- data Rec p
- rec :: Alpha p => p -> Rec p
- unrec :: Alpha p => Rec p -> p
- data TRec p
- trec :: Alpha p => p -> TRec p
- untrec :: (Fresh m, Alpha p) => TRec p -> m p
- luntrec :: (LFresh m, Alpha p) => TRec p -> m p
- newtype Shift p = Shift p
- aeq :: Alpha t => t -> t -> Bool
- aeqBinders :: Alpha p => p -> p -> Bool
- acompare :: Alpha t => t -> t -> Ordering
- fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)
- fvAny :: (Alpha t, Collection f) => t -> f AnyName
- patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- patfvAny :: (Alpha p, Collection f) => p -> f AnyName
- binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- bindersAny :: (Alpha p, Collection f) => p -> f AnyName
- class Foldable f => Collection f where
- newtype Multiset a = Multiset (Map a Int)
- class Rep1 (SubstD b) a => Subst b a where
- data SubstName a b where
- substBind :: Subst a b => Bind (Name a) b -> a -> b
- data Perm a
- single :: Ord a => a -> a -> Perm a
- compose :: Ord a => Perm a -> Perm a -> Perm a
- apply :: Ord a => Perm a -> a -> a
- support :: Ord a => Perm a -> [a]
- isid :: Ord a => Perm a -> Bool
- join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
- empty :: Perm a
- restrict :: Ord a => Perm a -> [a] -> Perm a
- mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
- swaps :: Alpha t => Perm AnyName -> t -> t
- swapsEmbeds :: Alpha p => Perm AnyName -> p -> p
- swapsBinders :: Alpha p => Perm AnyName -> p -> p
- freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
- class Monad m => Fresh m where
- type FreshM = FreshMT Identity
- runFreshM :: FreshM a -> a
- data FreshMT m a
- runFreshMT :: Monad m => FreshMT m a -> m a
- lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
- class Monad m => LFresh m where
- type LFreshM = LFreshMT Identity
- runLFreshM :: LFreshM a -> a
- data LFreshMT m a
- runLFreshMT :: LFreshMT m a -> m a
- class Rep1 AlphaD a => Alpha a where
- module Generics.RepLib
- rName :: forall a. Rep a => R (Name a)
- rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t)
- rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2)
- rEmbed :: forall t. Rep t => R (Embed t)
- rRec :: forall p. Rep p => R (Rec p)
- rShift :: forall p. Rep p => R (Shift p)

# Names

`Name`

s are things that get bound. This type is intentionally
abstract; to create a `Name`

you can use `string2Name`

or
`integer2Name`

. The type parameter is a tag, or *sort*, which
tells us what sorts of things this name may stand for. The sort
must be a *representable* type, *i.e.* an instance of the `Rep`

type class from the `RepLib`

generic programming framework.

To hide the sort of a name, use `AnyName`

.

## Instances

A name with a hidden (existentially quantified) sort. To hide
the sort of a name, use the `AnyName`

constructor directly; to
extract a name with a hidden sort, use `toSortedName`

.

## Instances

## Constructing and destructing free names

makeName :: Rep a => String -> Integer -> Name a Source #

Create a free `Name`

from a `String`

and an `Integer`

index.

## Dealing with name sorts

toSortedName :: Rep a => AnyName -> Maybe (Name a) Source #

Cast a name with an existentially hidden sort to an explicitly sorted name.

# Type combinators for specifying binding structure

`Bind`

, `Embed`

, `Rebind`

, `Rec`

, `TRec`

, and `Shift`

are
special types provided by Unbound for use in specifying the
binding structure of your data types.

An important distinction to keep in mind is the difference
between *term types* and *pattern types*.

*Term types*are normal types whose values represent data in your program. Any`Name`

s occurring in term types are either free variables, or*references*to binders.*Pattern types*are types which may be used on the left hand side of a`Bind`

. They*bind*names, that is, any`Name`

s occurring in pattern types are*binding sites*to which other names may refer.

`Name`

may be used as both a term type (where it represents a
free variable/reference) and a pattern type (where it
represents a binding site).

Any first-order algebraic data type (*i.e.* one containing no
functions) which contains only term types may be used as a
term type, and likewise for algebraic data types containing
only pattern types. For example,

(Name, [Name])

may be used as either a term type or a pattern type. On the other hand,

(Bind Name Name, Name)

may only be used as a term type, since `Bind Name Name`

is a
term type and not a pattern type.

We adopt the convention that the type variable `t`

stands for
term types, and the type variable `p`

stands for pattern
types. It would be nicer if we could actually use Haskell's
type system to enforce the distinction, but for various
technical reasons (involving the RepLib generic programming
framework which is used in the implementation), we cannot.
Or at least, we are not sufficiently clever to see how.

## Bind

### Bind constructors

bind :: (Alpha p, Alpha t) => p -> t -> Bind p t Source #

A smart constructor for binders, also sometimes referred to as "close". Free variables in the term are taken to be references to matching binders in the pattern. (Free variables with no matching binders will remain free.)

permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t Source #

Bind the pattern in the term "up to permutation" of bound variables.
For example, the following 4 terms are *all* alpha-equivalent:

permbind [a,b] (a,b) permbind [a,b] (b,a) permbind [b,a] (a,b) permbind [b,a] (b,a)

Note that none of these terms is equivalent to a term with a redundant pattern such as

permbind [a,b,c] (a,b)

For binding constructors which *do* render these equivalent,
see `setbind`

and `setbindAny`

.

setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t Source #

Bind the list of names in the term up to permutation and dropping of unused variables.

For example, the following 5 terms are *all* alpha-equivalent:

setbind [a,b] (a,b) setbind [a,b] (b,a) setbind [b,a] (a,b) setbind [b,a] (b,a) setbind [a,b,c] (a,b)

There is also a variant, `setbindAny`

, which ignores name sorts.

setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t Source #

Bind the list of (any-sorted) names in the term up to permutation
and dropping of unused variables. See `setbind`

.

### Bind destructors

Directly pattern-matching on `Bind`

values is not allowed,
but there are quite a few different ways to safely "open" a
binding. (If you want direct, unsafe access to the
components of a binding --- e.g. to write a function to
compute the size of terms that ignores all names --- you can
directly import Unbound.LocallyNameless.Ops and use the
`unsafeUnbind`

function.)

unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p, t) Source #

Unbind (also known as "open") is the simplest destructor for
bindings. It ensures that the names in the binding are globally
fresh, using a monad which is an instance of the `Fresh`

type
class.

lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c Source #

`lunbind`

opens a binding in an `LFresh`

monad, ensuring that the
names chosen for the binders are *locally* fresh. The components
of the binding are passed to a *continuation*, and the resulting
monadic action is run in a context extended to avoid choosing new
names which are the same as the ones chosen for this binding.

For more information, see the documentation for the `LFresh`

type
class.

### Simultaneous unbinding

Sometimes one may wish to open several bindings using *same*
names for their binding variables --- for example, when
checking equality of terms involving binders, so that the
free variables in the bodies will match appropriately during
recursive calls. Opening two bindings simultaneously is
accomplished with `unbind2`

(which picks globally fresh
names) and `lunbind2`

(which picks *locally* fresh names, see
the `LFresh`

documentation for more information). `unbind3`

and `lunbind3`

open three bindings simultaneously. In
principle, of course, `unbindN`

and `lunbindN`

can be easily
implemented for any `N`

; please let the maintainers know if
for some reason you would like an N > 3.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1, t1, p2, t2)) Source #

Unbind two terms with the *same* fresh names, provided the binders have
the same binding variables (both number and sort). If the patterns have
different binding variables, return `Nothing`

. Otherwise, return the
renamed patterns and the associated terms.

unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (Maybe (p1, t1, p2, t2, p3, t3)) Source #

Unbind three terms with the same fresh names, provided the
binders have the same number of binding variables. See the
documentation for `unbind2`

for more details.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m r Source #

lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> (Maybe (p1, t1, p2, t2, p3, t3) -> m r) -> m r Source #

unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (p1, t1, p2, t2) Source #

Unbind two binders with the same names, fail if the number of required
names and their sorts does not match. See `unbind2`

unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (p1, t1, p2, t2, p3, t3) Source #

Unbind three binders with the same names, fail if the number of required
names and their sorts does not match. See `unbind3`

lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> ((p1, t1, p2, t2) -> m r) -> m r Source #

See `lunbind2`

lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> ((p1, t1, p2, t2, p3, t3) -> m r) -> m r Source #

See `lunbind3`

## Embed

`Embed`

allows for terms to be *embedded* within patterns. Such
embedded terms do not bind names along with the rest of the
pattern. For examples, see the tutorial or examples directories.

If `t`

is a *term type*, then `Embed t`

is a *pattern type*.

`Embed`

is not abstract since it involves no binding, and hence
it is safe to manipulate directly. To create and destruct
`Embed`

terms, you may use the `Embed`

constructor directly.
(You may also use the functions `embed`

and `unembed`

, which
additionally can construct or destruct any number of enclosing
`Shift`

s at the same time.)

Embed t |

## Instances

unembed :: IsEmbed e => e -> Embedded e Source #

Destruct an embedded term. `unembed`

can have any of the types

Embed t -> t

Shift (Embed t) -> t

and so on.

## Rebind

`Rebind`

allows for *nested* bindings. If `p1`

and `p2`

are
pattern types, then `Rebind p1 p2`

is also a pattern type,
similar to the pattern type `(p1,p2)`

except that `p1`

*scopes over* `p2`

. That is, names within terms embedded in `p2`

may refer to binders in `p1`

.

## Instances

rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2 Source #

Constructor for rebinding patterns.

## Rec

If `p`

is a pattern type, then `Rec p`

is also a pattern type,
which is *recursive* in the sense that `p`

may bind names in terms
embedded within itself. Useful for encoding e.g. lectrec and
Agda's dot notation.

## Instances

## TRec

`TRec`

is a standalone variant of `Rec`

: the only difference is
that whereas

is a pattern type, `Rec`

p`TRec p`

is a *term type*. It is isomorphic to

.`Bind`

(`Rec`

p) ()

Note that `TRec`

corresponds to Pottier's *abstraction* construct
from alpha-Caml. In this context,

corresponds to
alpha-Caml's `Embed`

t`inner t`

, and

corresponds to
alpha-Caml's `Shift`

(`Embed`

t)`outer t`

.

untrec :: (Fresh m, Alpha p) => TRec p -> m p Source #

Destructor for recursive abstractions which picks globally fresh names for the binders.

luntrec :: (LFresh m, Alpha p) => TRec p -> m p Source #

Destructor for recursive abstractions which picks *locally* fresh
names for binders (see `LFresh`

).

## Shift

Shift the scope of an embedded term one level outwards.

Shift p |

## Instances

# Generically derived operations

This section lists a number of operations which are derived generically for any types whose binding structure is specified via the type combinators described in the previous section.

## Alpha-equivalence

aeqBinders :: Alpha p => p -> p -> Bool Source #

Determine (alpha-)equivalence of patterns. Do they bind the same variables in the same patterns and have alpha-equivalent annotations in matching positions?

acompare :: Alpha t => t -> t -> Ordering Source #

An alpha-respecting total order on terms involving binders.

## Variable calculations

Functions for computing the free variables or binding
variables of a term or pattern. Note that all these
functions may return an arbitrary *collection*, which
includes lists, sets, and multisets.

fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a) Source #

Calculate the free variables of a particular sort contained in a term.

fvAny :: (Alpha t, Collection f) => t -> f AnyName Source #

Calculate the free variables (of any sort) contained in a term.

patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a) Source #

Calculate the variables of a particular sort that occur freely in terms embedded within a pattern (but are not bound by the pattern).

patfvAny :: (Alpha p, Collection f) => p -> f AnyName Source #

Calculate the variables (of any sort) that occur freely in terms embedded within a pattern (but are not bound by the pattern).

binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a) Source #

Calculate the binding variables (of a particular sort) in a pattern.

bindersAny :: (Alpha p, Collection f) => p -> f AnyName Source #

Calculate the binding variables (of any sort) in a pattern.

### Collections

class Foldable f => Collection f where Source #

Collections are foldable types that support empty, singleton, union, and map operations. The result of a free variable calculation may be any collection. Instances are provided for lists, sets, and multisets.

An empty collection. Must be the identity for `union`

.

singleton :: a -> f a Source #

Create a singleton collection.

union :: Ord a => f a -> f a -> f a Source #

An associative combining operation. The `Ord`

constraint is in
order to accommodate sets.

cmap :: (Ord a, Ord b) => (a -> b) -> f a -> f b Source #

Collections must be functorial. The normal `Functor`

class
won't do because of the `Ord`

constraint on sets.

## Instances

Collection [] Source # | Lists are containers under concatenation. Lists preserve ordering and multiplicity of elements. |

Collection Set Source # | Sets are containers under union, which preserve only occurrence, not multiplicity or ordering. |

Collection Multiset Source # | Multisets are containers which preserve multiplicity but not ordering. |

A simple representation of multisets.

## Instances

Foldable Multiset Source # | |

Defined in Unbound.Util fold :: Monoid m => Multiset m -> m # foldMap :: Monoid m => (a -> m) -> Multiset a -> m # foldr :: (a -> b -> b) -> b -> Multiset a -> b # foldr' :: (a -> b -> b) -> b -> Multiset a -> b # foldl :: (b -> a -> b) -> b -> Multiset a -> b # foldl' :: (b -> a -> b) -> b -> Multiset a -> b # foldr1 :: (a -> a -> a) -> Multiset a -> a # foldl1 :: (a -> a -> a) -> Multiset a -> a # elem :: Eq a => a -> Multiset a -> Bool # maximum :: Ord a => Multiset a -> a # minimum :: Ord a => Multiset a -> a # | |

Collection Multiset Source # | Multisets are containers which preserve multiplicity but not ordering. |

## Substitution

Capture-avoiding substitution.

class Rep1 (SubstD b) a => Subst b a where Source #

The `Subst`

class governs capture-avoiding substitution. To
derive this class, you only need to indicate where the variables
are in the data type, by overriding the method `isvar`

.

isvar :: a -> Maybe (SubstName a b) Source #

This is the only method which normally needs to be implemented
explicitly. If the argument is a variable, return its name
wrapped in the `SubstName`

constructor. Return `Nothing`

for
non-variable arguments. The default implementation always
returns `Nothing`

.

isCoerceVar :: a -> Maybe (SubstCoerce a b) Source #

This is an alternative version to `isvar`

, useable in the case
that the substituted argument doesn't have *exactly* the same type
as the term it should be substituted into.
The default implementation always returns `Nothing`

.

subst :: Name b -> b -> a -> a Source #

substitutes `subst`

nm sub tm`sub`

for `nm`

in `tm`

. It has
a default generic implementation in terms of `isvar`

.

substs :: [(Name b, b)] -> a -> a Source #

Perform several simultaneous substitutions. This method also
has a default generic implementation in terms of `isvar`

.

substPat :: AlphaCtx -> b -> a -> a Source #

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a Source #

## Instances

substBind :: Subst a b => Bind (Name a) b -> a -> b Source #

Immediately substitute for a (single) bound variable in a binder, without first naming that variable.

## Permutations

A *permutation* is a bijective function from names to names
which is the identity on all but a finite set of names. They
form the basis for nominal approaches to binding, but can
also be useful in general.

### Working with permutations

compose :: Ord a => Perm a -> Perm a -> Perm a Source #

Compose two permutations. The right-hand permutation will be applied first.

support :: Ord a => Perm a -> [a] Source #

The *support* of a permutation is the set of elements which are
not fixed.

join :: Ord a => Perm a -> Perm a -> Maybe (Perm a) Source #

*Join* two permutations by taking the union of their relation
graphs. Fail if they are inconsistent, i.e. map the same element
to two different elements.

mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a) Source #

`mkPerm l1 l2`

creates a permutation that sends `l1`

to `l2`

.
Fail if there is no such permutation, either because the lists
have different lengths or because they are inconsistent (which
can only happen if `l1`

or `l2`

have repeated elements).

### Permuting terms

swapsEmbeds :: Alpha p => Perm AnyName -> p -> p Source #

Apply a permutation to the embedded terms in a pattern. Binding names are left alone by the permutation.

swapsBinders :: Alpha p => Perm AnyName -> p -> p Source #

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

# Freshness

When opening a term-level binding (`Bind`

or `TRec`

), fresh
names must be generated for the binders of its pattern.
Fresh names can be generated according to one of two
strategies: names can be *globally* fresh (not conflicting
with any other generated names, ever; see `Fresh`

) or
*locally* fresh (not conflicting only with a specific set of
"currently in-scope" names; see `LFresh`

). Generating
globally fresh names is simpler and suffices for many
applications. Generating locally fresh names tends to be
useful when the names are for human consumption, e.g. when
implementing a pretty-printer.

## Global freshness

### The `Fresh`

class

class Monad m => Fresh m where Source #

The `Fresh`

type class governs monads which can generate new
globally unique `Name`

s based on a given `Name`

.

fresh :: Rep a => Name a -> m (Name a) Source #

Generate a new globally unique name based on the given one.

## Instances

Fresh m => Fresh (ListT m) Source # | |

Fresh m => Fresh (MaybeT m) Source # | |

Monad m => Fresh (FreshMT m) Source # | |

Fresh m => Fresh (IdentityT m) Source # | |

Fresh m => Fresh (ExceptT e m) Source # | |

Fresh m => Fresh (StateT s m) Source # | |

Fresh m => Fresh (StateT s m) Source # | |

(Monoid w, Fresh m) => Fresh (WriterT w m) Source # | |

(Monoid w, Fresh m) => Fresh (WriterT w m) Source # | |

Fresh m => Fresh (ContT r m) Source # | |

Fresh m => Fresh (ReaderT r m) Source # | |

### The `FreshM`

monad

The `FreshM`

monad provides a concrete implementation of the
`Fresh`

type class. The `FreshMT`

monad transformer variant
can be freely combined with other standard monads and monad
transformers from the `transformers`

library.

runFreshM :: FreshM a -> a Source #

Run a FreshM computation (with the global index starting at zero).

The `FreshM`

monad transformer. Keeps track of the lowest index
still globally unused, and increments the index every time it is
asked for a fresh name.

## Instances

MonadTrans FreshMT Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

MonadWriter w m => MonadWriter w (FreshMT m) Source # | |

MonadState s m => MonadState s (FreshMT m) Source # | |

MonadReader r m => MonadReader r (FreshMT m) Source # | |

MonadError e m => MonadError e (FreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh throwError :: e -> FreshMT m a # catchError :: FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a # | |

Monad m => Monad (FreshMT m) Source # | |

Functor m => Functor (FreshMT m) Source # | |

MonadFix m => MonadFix (FreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

Monad m => Applicative (FreshMT m) Source # | |

MonadIO m => MonadIO (FreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

MonadPlus m => Alternative (FreshMT m) Source # | |

MonadPlus m => MonadPlus (FreshMT m) Source # | |

MonadCont m => MonadCont (FreshMT m) Source # | |

Monad m => Fresh (FreshMT m) Source # | |

runFreshMT :: Monad m => FreshMT m a -> m a Source #

Run a `FreshMT`

computation (with the global index starting at zero).

## Local freshness

lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b Source #

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

### The `LFresh`

class

class Monad m => LFresh m where Source #

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, not necessarily globally fresh.

lfresh :: Rep a => Name a -> m (Name a) Source #

Pick a new name that is fresh for the current (implicit) scope.

avoid :: [AnyName] -> m a -> m a Source #

Avoid the given names when freshening in the subcomputation, that is, add the given names to the in-scope set.

getAvoids :: m (Set AnyName) Source #

Get the set of names currently being avoided.

## Instances

LFresh m => LFresh (ListT m) Source # | |

LFresh m => LFresh (MaybeT m) Source # | |

Monad m => LFresh (LFreshMT m) Source # | |

LFresh m => LFresh (IdentityT m) Source # | |

LFresh m => LFresh (ExceptT e m) Source # | |

LFresh m => LFresh (StateT s m) Source # | |

LFresh m => LFresh (StateT s m) Source # | |

(Monoid w, LFresh m) => LFresh (WriterT w m) Source # | |

(Monoid w, LFresh m) => LFresh (WriterT w m) Source # | |

LFresh m => LFresh (ContT r m) Source # | |

LFresh m => LFresh (ReaderT r m) Source # | |

### The `LFreshM`

monad

The `LFreshM`

monad provides a concrete implementation of the
`LFresh`

type class. The `LFreshMT`

monad transformer variant
can be freely combined with other standard monads and monad
transformers from the `transformers`

library.

type LFreshM = LFreshMT Identity Source #

A convenient monad which is an instance of `LFresh`

. It keeps
track of a set of names to avoid, and when asked for a fresh one
will choose the first unused numerical name.

runLFreshM :: LFreshM a -> a Source #

Run a LFreshM computation in an empty context.

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first numeric prefix of the given name which is currently unused.

## Instances

MonadTrans LFreshMT Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

MonadWriter w m => MonadWriter w (LFreshMT m) Source # | |

MonadState s m => MonadState s (LFreshMT m) Source # | |

MonadReader r m => MonadReader r (LFreshMT m) Source # | |

MonadError e m => MonadError e (LFreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh throwError :: e -> LFreshMT m a # catchError :: LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a # | |

Monad m => Monad (LFreshMT m) Source # | |

Functor m => Functor (LFreshMT m) Source # | |

MonadFix m => MonadFix (LFreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

Applicative m => Applicative (LFreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

MonadIO m => MonadIO (LFreshMT m) Source # | |

Defined in Unbound.LocallyNameless.Fresh | |

Alternative m => Alternative (LFreshMT m) Source # | |

MonadPlus m => MonadPlus (LFreshMT m) Source # | |

MonadCont m => MonadCont (LFreshMT m) Source # | |

Monad m => LFresh (LFreshMT m) Source # | |

runLFreshMT :: LFreshMT m a -> m a Source #

Run an `LFreshMT`

computation in an empty context.

# The `Alpha`

class

class Rep1 AlphaD a => Alpha a where Source #

The `Alpha`

type class is for types which may contain names. The
`Rep1`

constraint means that we can only make instances of this
class for types that have generic representations (which can be
automatically derived by RepLib.)

Note that the methods of `Alpha`

should almost never be called
directly. Instead, use other methods provided by this module
which are defined in terms of `Alpha`

methods.

Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring

instance Alpha MyType

Occasionally, however, it may be useful to override the default
implementations of one or more `Alpha`

methods for a particular
type. For example, consider a type like

data Term = ... | Annotation Stuff Term

where the `Annotation`

constructor of `Term`

associates some sort
of annotation with a term --- say, information obtained from a
parser about where in an input file the term came from. This
information is needed to produce good error messages, but should
not be taken into consideration when, say, comparing two `Term`

s
for alpha-equivalence. In order to make `aeq`

ignore
annotations, you can override the implementation of `aeq'`

like
so:

instance Alpha Term where aeq' c (Annotation _ t1) t2 = aeq' c t1 t2 aeq' c t1 (Annotation _ t2) = aeq' c t1 t2 aeq' c t1 t2 = aeqR1 rep1 t1 t2

Note how the call to `aeqR1`

handles all the other cases generically.

If you use Abstract types (i.e. those with representations derived via derive_abstract) then you must provide a definition of aeq' and acompare'. In these cases, Unbound has no information about the structure of the type and cannot do anything sensible.

swaps' :: AlphaCtx -> Perm AnyName -> a -> a Source #

See `swaps`

.

fv' :: Collection f => AlphaCtx -> a -> f AnyName Source #

See `fv`

.

lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b Source #

See `lfreshen`

.

freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName) Source #

See `freshen`

.

aeq' :: AlphaCtx -> a -> a -> Bool Source #

See `aeq`

.

acompare' :: AlphaCtx -> a -> a -> Ordering Source #

See `acompare`

.

close :: Alpha b => AlphaCtx -> b -> a -> a Source #

Replace free names by bound names.

open :: Alpha b => AlphaCtx -> b -> a -> a Source #

Replace bound names by free names.

isPat :: a -> Maybe [AnyName] Source #

`isPat x`

dynamically checks whether `x`

can be used as a valid
pattern. The default instance returns `Just`

if at all
possible. If successful, returns a list of names bound by the
pattern.

`isTerm x`

dynamically checks whether `x`

can be used as a
valid term. The default instance returns `True`

if at all
possible.

`isEmbed`

is needed internally for the implementation of
`isPat`

. `isEmbed`

is true for terms wrapped in `Embed`

and zero
or more occurrences of `Shift`

. The default implementation
simply returns `False`

.

nthpatrec :: a -> NthCont Source #

looks up the `nthpatrec`

p n`n`

th name in the pattern `p`

(zero-indexed), returning the number of names encountered if not
found.

findpatrec :: a -> AnyName -> FindResult Source #

Find the (first) index of the name in the pattern if one exists; otherwise, return the number of names encountered instead.

## Instances

# Re-exported RepLib API for convenience

module Generics.RepLib

# Pay no attention to the man behind the curtain

These type representation objects are exported so they can be referenced by auto-generated code. Please pretend they do not exist.