unbound-0.4.2: Generic support for programming with names and binders

PortabilityGHC only (-XKitchenSink)
Stabilityexperimental
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellNone

Unbound.LocallyNameless

Contents

Description

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

Names

data Name a Source

Names 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

(Rep a0, Sat (ctx0 (R a0)), Sat (ctx0 (String, Integer)), Sat (ctx0 Integer)) => Rep1 ctx0 (Name a0) 
Rep a => Subst b (Name a) 
Eq (Name a) 
Ord (Name a) 
Show (Name a) 
Rep a0 => Rep (Name a0) 
Rep a => Alpha (Name a) 

data AnyName Source

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.

Constructors

forall a . Rep a => AnyName (Name a) 

Constructing and destructing free names

integer2Name :: Rep a => Integer -> Name aSource

Create a free Name from an Integer.

string2Name :: Rep a => String -> Name aSource

Create a free Name from a String.

s2n :: Rep a => String -> Name aSource

Convenient synonym for string2Name.

makeName :: Rep a => String -> Integer -> Name aSource

Create a free Name from a String and an Integer index.

name2Integer :: Name a -> IntegerSource

Get the integer index of a Name.

name2String :: Name a -> StringSource

Get the string part of a Name.

anyName2Integer :: AnyName -> IntegerSource

Get the integer index of an AnyName.

anyName2String :: AnyName -> StringSource

Get the string part of an AnyName.

Dealing with name sorts

translate :: Rep b => Name a -> Name bSource

Change the sort of a name.

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 Names 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 Names 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

type Bind p t = GenBind StrictOrder StrictCard p tSource

Bind constructors

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

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 tSource

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] tSource

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] tSource

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 cSource

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 rSource

Unbind two terms with the same locally fresh names, provided the patterns have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

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 rSource

Unbind three terms with the same locally fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

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

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

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 rSource

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 rSource

Embed

newtype Embed t Source

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 Shifts at the same time.)

Constructors

Embed t 

Instances

(Rep t0, Sat (ctx0 t0)) => Rep1 ctx0 (Embed t0) 
Subst c a => Subst c (Embed a) 
Eq t => Eq (Embed t) 
Show a => Show (Embed a) 
Rep t0 => Rep (Embed t0) 
IsEmbed (Embed t) 
Alpha t => Alpha (Embed t) 

embed :: IsEmbed e => Embedded e -> eSource

Construct an embedded term, which is an instance of Embed with any number of enclosing Shifts. That is, embed can have any of the types

  • t -> Embed t
  • t -> Shift (Embed t)
  • t -> Shift (Shift (Embed t))

and so on.

unembed :: IsEmbed e => e -> Embedded eSource

Destruct an embedded term. unembed can have any of the types

  • Embed t -> t
  • Shift (Embed t) -> t

and so on.

Rebind

data Rebind p1 p2 Source

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

(Rep p10, Rep p20, Sat (ctx0 p10), Sat (ctx0 p20)) => Rep1 ctx0 (Rebind p10 p20) 
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) 
(Alpha p1, Alpha p2, Eq p2) => Eq (Rebind p1 p2)

Compare for alpha-equality.

(Show a, Show b) => Show (Rebind a b) 
(Rep p10, Rep p20) => Rep (Rebind p10 p20) 
(Alpha p, Alpha q) => Alpha (Rebind p q) 

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

Constructor for rebinding patterns.

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

Destructor for rebinding patterns. It does not need a monadic context for generating fresh names, since Rebind can only occur in the pattern of a Bind; hence a previous call to unbind (or something similar) must have already freshened the names at this point.

Rec

data Rec p Source

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

(Rep p0, Sat (ctx0 p0)) => Rep1 ctx0 (Rec p0) 
(Alpha a, Subst c a) => Subst c (Rec a) 
Show a => Show (Rec a) 
Rep p0 => Rep (Rec p0) 
Alpha p => Alpha (Rec p) 

rec :: Alpha p => p -> Rec pSource

Constructor for recursive patterns.

unrec :: Alpha p => Rec p -> pSource

Destructor for recursive patterns.

TRec

data TRec p Source

TRec is a standalone variant of Rec: the only difference is that whereas Rec p is a pattern type, 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, Embed t corresponds to alpha-Caml's inner t, and Shift (Embed t) corresponds to alpha-Caml's outer t.

Instances

Show a => Show (TRec a) 

trec :: Alpha p => p -> TRec pSource

Constructor for recursive abstractions.

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

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

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

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

Shift

newtype Shift p Source

Shift the scope of an embedded term one level outwards.

Constructors

Shift p 

Instances

(Rep p0, Sat (ctx0 p0)) => Rep1 ctx0 (Shift p0) 
Eq p => Eq (Shift p) 
Show a => Show (Shift a) 
Rep p0 => Rep (Shift p0) 
IsEmbed e => IsEmbed (Shift e) 
Alpha a => Alpha (Shift a) 

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

aeq :: Alpha t => t -> t -> BoolSource

Determine the alpha-equivalence of two terms.

aeqBinders :: Alpha p => p -> p -> BoolSource

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 -> OrderingSource

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 AnyNameSource

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 AnyNameSource

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 AnyNameSource

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

Collections

class Foldable f => Collection f whereSource

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.

Methods

emptyC :: f aSource

An empty collection. Must be the identity for union.

singleton :: a -> f aSource

Create a singleton collection.

union :: Ord a => f a -> f a -> f aSource

An associative combining operation. The Ord constraint is in order to accommodate sets.

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

Collections must be functorial. The normal Functor class won't do because of the Ord constraint on sets.

Instances

Collection []

Lists are containers under concatenation. Lists preserve ordering and multiplicity of elements.

Collection Set

Sets are containers under union, which preserve only occurrence, not multiplicity or ordering.

Collection Multiset

Multisets are containers which preserve multiplicity but not ordering.

newtype Multiset a Source

A simple representation of multisets.

Constructors

Multiset (Map a Int) 

Instances

Foldable Multiset 
Collection Multiset

Multisets are containers which preserve multiplicity but not ordering.

Substitution

Capture-avoiding substitution.

class Rep1 (SubstD b) a => Subst b a whereSource

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.

Methods

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 -> aSource

subst nm sub tm substitutes sub for nm in tm. It has a default generic implementation in terms of isvar.

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

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

Instances

Subst b AnyName 
Subst b Double 
Subst b Float 
Subst b Integer 
Subst b Char 
Subst b () 
Subst b Bool 
Subst b Int 
(Alpha a, Subst c a) => Subst c (Rec a) 
Subst c a => Subst c (Embed a) 
Subst c a => Subst c (Maybe a) 
Subst c a => Subst c [a] 
Rep a => Subst b (Name a) 
Rep a => Subst b (R a) 
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) 
(Subst c a, Subst c b) => Subst c (Either a b) 
(Subst c a, Subst c b) => Subst c (a, b) 
(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) 
(Rep order, Rep card, Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (GenBind order card a b) 
(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) 
(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) 

data SubstName a b whereSource

See isvar.

Constructors

SubstName :: a ~ b => Name a -> SubstName a b 

Permutations

data Perm a Source

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.

Instances

Ord a => Eq (Perm a) 
Show a => Show (Perm a) 
Ord a => Monoid (Perm a)

Permutations form a monoid under composition.

Working with permutations

single :: Ord a => a -> a -> Perm aSource

Create a permutation which swaps two elements.

compose :: Ord a => Perm a -> Perm a -> Perm aSource

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

apply :: Ord a => Perm a -> a -> aSource

Apply a permutation to an element of the domain.

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

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

isid :: Ord a => Perm a -> BoolSource

Is this the identity permutation?

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.

empty :: Perm aSource

The empty (identity) permutation.

restrict :: Ord a => Perm a -> [a] -> Perm aSource

Restrict a permutation to a certain domain.

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

swaps :: Alpha t => Perm AnyName -> t -> tSource

Apply a permutation to a term.

swapsEmbeds :: Alpha p => Perm AnyName -> p -> pSource

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

swapsBinders :: Alpha p => Perm AnyName -> p -> pSource

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

freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)Source

Freshen a pattern by replacing all old binding Names with new fresh Names, returning a new pattern and a Perm Name specifying how Names were replaced.

The Fresh class

class Monad m => Fresh m whereSource

The Fresh type class governs monads which can generate new globally unique Names based on a given Name.

Methods

fresh :: Name a -> m (Name a)Source

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

Instances

Fresh m => Fresh (ListT m) 
Fresh m => Fresh (MaybeT m) 
Fresh m => Fresh (IdentityT m) 
Monad m => Fresh (FreshMT m) 
Fresh m => Fresh (ContT r m) 
(Error e, Fresh m) => Fresh (ErrorT e m) 
Fresh m => Fresh (ReaderT r m) 
Fresh m => Fresh (StateT s m) 
Fresh m => Fresh (StateT s m) 
(Monoid w, Fresh m) => Fresh (WriterT w m) 
(Monoid w, Fresh m) => Fresh (WriterT w m) 

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.

type FreshM = FreshMT IdentitySource

A convenient monad which is an instance of Fresh. It keeps track of a global index used for generating fresh names, which is incremented every time fresh is called.

runFreshM :: FreshM a -> aSource

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

data FreshMT m a Source

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.

runFreshMT :: Monad m => FreshMT m a -> m aSource

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 bSource

"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 whereSource

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.

Methods

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 aSource

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) 
LFresh m => LFresh (MaybeT m) 
LFresh m => LFresh (IdentityT m) 
Monad m => LFresh (LFreshMT m) 
LFresh m => LFresh (ContT r m) 
(Error e, LFresh m) => LFresh (ErrorT e m) 
LFresh m => LFresh (ReaderT r m) 
LFresh m => LFresh (StateT s m) 
LFresh m => LFresh (StateT s m) 
(Monoid w, LFresh m) => LFresh (WriterT w m) 
(Monoid w, LFresh m) => LFresh (WriterT w m) 

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 IdentitySource

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 -> aSource

Run a LFreshM computation in an empty context.

data LFreshMT m a Source

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.

runLFreshMT :: LFreshMT m a -> m aSource

Run an LFreshMT computation in an empty context.

The Alpha class

class (Show a, Rep1 AlphaD a) => Alpha a whereSource

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

Methods

swaps' :: AlphaCtx -> Perm AnyName -> a -> aSource

See swaps.

fv' :: Collection f => AlphaCtx -> a -> f AnyNameSource

See fv.

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

See lfreshen.

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

See freshen.

aeq' :: AlphaCtx -> a -> a -> BoolSource

See aeq.

acompare' :: AlphaCtx -> a -> a -> OrderingSource

See acompare.

close :: Alpha b => AlphaCtx -> b -> a -> aSource

Replace free names by bound names.

open :: Alpha b => AlphaCtx -> b -> a -> aSource

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 :: a -> BoolSource

isTerm x dynamically checks whether x can be used as a valid term. The default instance returns True if at all possible.

isEmbed :: a -> BoolSource

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 -> NthContSource

nthpatrec p n looks up the nth name in the pattern p (zero-indexed), returning the number of names encountered if not found.

findpatrec :: a -> AnyName -> FindResultSource

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

Instances

Alpha Bool 
Alpha Char 
Alpha Double 
Alpha Float 
Alpha Int 
Alpha Integer 
Alpha () 
Alpha AnyName 
Alpha a => Alpha [a] 
Alpha a => Alpha (Maybe a) 
Rep a => Alpha (R a) 
Rep a => Alpha (Name a) 
Alpha a => Alpha (Shift a) 
Alpha t => Alpha (Embed t) 
Alpha p => Alpha (Rec p) 
(Alpha a, Alpha b) => Alpha (Either a b) 
(Alpha a, Alpha b) => Alpha (a, b) 
(Alpha p, Alpha q) => Alpha (Rebind p q) 
(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) 
(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) 
(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) 
(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) 

Re-exported RepLib API for convenience

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.

rName :: forall a. Rep a => R (Name a)Source

rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t)Source

rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2)Source

rEmbed :: forall t. Rep t => R (Embed t)Source

rRec :: forall p. Rep p => R (Rec p)Source

rShift :: forall p. Rep p => R (Shift p)Source