|Maintainer||Brent Yorgey <email@example.com>|
Special type combinators for specifying binding structure.
- data Bind p t = B 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
- rBind :: forall p[abAn] t[abAo]. (Rep p[abAn], Rep t[abAo]) => R (Bind p[abAn] t[abAo])
- rRebind :: forall p1[abAl] p2[abAm]. (Rep p1[abAl], Rep p2[abAm]) => R (Rebind p1[abAl] p2[abAm])
- rEmbed :: forall t[abAi]. Rep t[abAi] => R (Embed t[abAi])
- rRec :: forall p[abAk]. Rep p[abAk] => R (Rec p[abAk])
- rShift :: forall p[abAh]. Rep p[abAh] => R (Shift p[abAh])
The most fundamental combinator for expressing binding structure
Bind. The term type
Bind p t represents a pattern
paired with a term
t, where names in
p are bound within
|B p t|
|(Rep p[abAn], Rep t[abAo], Sat (ctx[abF0] p[abAn]), Sat (ctx[abF0] t[abAo])) => Rep1 ctx[abF0] (Bind p[abAn] t[abAo])|
|(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)|
|(Alpha a, Alpha b, Read a, Read b) => Read (Bind a b)|
|(Show a, Show b) => Show (Bind a b)|
|(Rep p[abAn], Rep t[abAo]) => Rep (Bind p[abAn] t[abAo])|
|(Alpha p, Alpha t) => Alpha (Bind p t)|
Rebind allows for nested bindings. If
pattern types, then
Rebind p1 p2 is also a pattern type,
similar to the pattern type
(p1,p2) except that
p2. That is, names within terms embedded in
may refer to binders in
|R p1 p2|
|(Rep p1[abAl], Rep p2[abAm], Sat (ctx[abEF] p1[abAl]), Sat (ctx[abEF] p2[abAm])) => Rep1 ctx[abEF] (Rebind p1[abAl] p2[abAm])|
|(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 p1[abAl], Rep p2[abAm]) => Rep (Rebind p1[abAl] p2[abAm])|
|(Alpha p, Alpha q) => Alpha (Rebind p q)|
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.
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.
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
additionally can construct or destruct any number of enclosing
Shifts at the same time.)
Shift the scope of an embedded term one level outwards.
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.