| Portability | GHC only |
|---|---|
| Stability | experimental |
| Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
| Safe Haskell | None |
Unbound.LocallyNameless.Types
Description
Special type combinators for specifying binding structure.
- data GenBind order card p t = B p t
- type Bind p t = GenBind StrictOrder StrictCard p t
- type SetBind p t = GenBind RelaxedOrder StrictCard p t
- type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t
- data Rebind p1 p2 = R p1 p2
- data Rec p = Rec p
- newtype TRec p = TRec (Bind (Rec p) ())
- newtype Embed t = Embed t
- newtype Shift p = Shift p
- module Unbound.LocallyNameless.Name
- 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)
Documentation
data GenBind order card p t Source
The most fundamental combinator for expressing binding structure
is Bind. The term type Bind p t represents a pattern p
paired with a term t, where names in p are bound within t.
Like Name, Bind is also abstract. You can create bindings
using bind and take them apart with unbind and friends.
Constructors
| B p t |
Instances
| (Rep order0, Rep card0, Rep p0, Rep t0, Sat (ctx0 p0), Sat (ctx0 t0)) => Rep1 ctx0 (GenBind order0 card0 p0 t0) | |
| (Rep order, Rep card, Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (GenBind order card a b) | |
| (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) | |
| (Show a, Show b) => Show (GenBind order card a b) | |
| (Rep order0, Rep card0, Rep p0, Rep t0) => Rep (GenBind order0 card0 p0 t0) | |
| (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) |
type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p tSource
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.
Constructors
| R p1 p2 |
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) |
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.
Constructors
| Rec p |
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.
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 |
Shift the scope of an embedded term one level outwards.
Constructors
| Shift p |
module Unbound.LocallyNameless.Name
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.