| License | BSD-like (see LICENSE) |
|---|---|
| Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
| Stability | experimental |
| Portability | GHC only (-XKitchenSink) |
| Safe Haskell | None |
| Language | Haskell2010 |
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.
- 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
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.
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.
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
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, anyNames 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
Shifts at the same time.)
Constructors
| Embed t |
Instances
| (Rep t0, Sat (ctx0 t0)) => Rep1 ctx0 (Embed t0) Source # | |
| (Alpha t, Subst b t) => Subst b (Embed t) Source # | |
| Eq t => Eq (Embed t) Source # | |
| Show a => Show (Embed a) Source # | |
| Rep t0 => Rep (Embed t0) Source # | |
| Binary p => Binary (Embed p) Source # | |
| IsEmbed (Embed t) Source # | |
| Alpha t => Alpha (Embed t) Source # | |
| type Embedded (Embed t) Source # | |
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
| (Rep p10, Rep p20, Sat (ctx0 p10), Sat (ctx0 p20)) => Rep1 ctx0 (Rebind p10 p20) Source # | |
| (Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source # | |
| (Show a, Show b) => Show (Rebind a b) Source # | |
| (Rep p10, Rep p20) => Rep (Rebind p10 p20) Source # | |
| (Binary p1, Binary p2) => Binary (Rebind p1 p2) Source # | |
| (Alpha p, Alpha q) => Alpha (Rebind p q) Source # | |
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.
TRec
TRec is a standalone variant of Rec: the only difference is
that whereas Rec pTRec 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 tinner t, and 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.
Constructors
| Shift p |
Instances
| (Rep p0, Sat (ctx0 p0)) => Rep1 ctx0 (Shift p0) Source # | |
| (Alpha a, Subst b a) => Subst b (Shift a) Source # | |
| Eq p => Eq (Shift p) Source # | |
| Show a => Show (Shift a) Source # | |
| Rep p0 => Rep (Shift p0) Source # | |
| IsEmbed e => IsEmbed (Shift e) Source # | |
| Alpha a => Alpha (Shift a) Source # | |
| type Embedded (Shift e) Source # | |
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.
Methods
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.
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.
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 -> a Source #
subst nm sub tmsub 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
| Subst b AnyName Source # | |
| Subst b Double Source # | |
| Subst b Float Source # | |
| Subst b Integer Source # | |
| Subst b Char Source # | |
| Subst b () Source # | |
| Subst b Bool Source # | |
| Subst b Int Source # | |
| Subst c a => Subst c (Maybe a) Source # | |
| Subst c a => Subst c [a] Source # | |
| Rep a => Subst b (Name a) Source # | |
| Rep a => Subst b (R a) Source # | |
| (Alpha a, Subst b a) => Subst b (Shift a) Source # | |
| (Alpha t, Subst b t) => Subst b (Embed t) Source # | |
| (Alpha p, Subst b p) => Subst b (Rec p) Source # | |
| (Subst c a, Subst c b) => Subst c (Either a b) Source # | |
| (Subst c a, Subst c b) => Subst c (a, b) Source # | |
| (Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source # | |
| (Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) Source # | |
| (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) Source # | |
| (Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) Source # | |
| (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) Source # | |
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 Names based on a given Name.
Minimal complete definition
Methods
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 (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 (IdentityT * 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 # | |
| MonadError e m => MonadError e (FreshMT m) Source # | |
| MonadReader r m => MonadReader r (FreshMT m) Source # | |
| MonadState s m => MonadState s (FreshMT m) Source # | |
| MonadWriter w m => MonadWriter w (FreshMT m) Source # | |
| Monad m => Monad (FreshMT m) Source # | |
| Functor m => Functor (FreshMT m) Source # | |
| MonadFix m => MonadFix (FreshMT m) Source # | |
| Monad m => Applicative (FreshMT m) Source # | |
| MonadIO m => MonadIO (FreshMT m) Source # | |
| 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.
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 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 (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 (IdentityT * 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 # | |
| MonadError e m => MonadError e (LFreshMT m) Source # | |
| MonadReader r m => MonadReader r (LFreshMT m) Source # | |
| MonadState s m => MonadState s (LFreshMT m) Source # | |
| MonadWriter w m => MonadWriter w (LFreshMT m) Source # | |
| Monad m => Monad (LFreshMT m) Source # | |
| Functor m => Functor (LFreshMT m) Source # | |
| MonadFix m => MonadFix (LFreshMT m) Source # | |
| Applicative m => Applicative (LFreshMT m) Source # | |
| MonadIO m => MonadIO (LFreshMT m) Source # | |
| 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 Termwhere 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.
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.
Methods
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 #
nthpatrec p nnth 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
| Alpha Bool Source # | |
| Alpha Char Source # | |
| Alpha Double Source # | |
| Alpha Float Source # | |
| Alpha Int Source # | |
| Alpha Integer Source # | |
| Alpha () Source # | |
| Alpha AnyName Source # | |
| Alpha a => Alpha [a] Source # | |
| Alpha a => Alpha (Maybe a) Source # | |
| Rep a => Alpha (R a) Source # | |
| Rep a => Alpha (Name a) Source # | |
| Alpha a => Alpha (Shift a) Source # | |
| Alpha t => Alpha (Embed t) Source # | |
| Alpha p => Alpha (Rec p) Source # | |
| (Alpha a, Alpha b) => Alpha (Either a b) Source # | |
| (Alpha a, Alpha b) => Alpha (a, b) Source # | |
| (Alpha p, Alpha q) => Alpha (Rebind p q) Source # | |
| (Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) Source # | |
| (Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) Source # | |
| (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) Source # | |
| (Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) Source # | |
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.