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

PortabilityGHC only
Stabilityexperimental
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>

Unbound.LocallyNameless.Types

Contents

Description

Special type combinators for specifying binding structure.

Synopsis

Documentation

data Bind 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 p[a1eRq], Rep t[a1eRr], Sat (ctx[a1eW5] p[a1eRq]), Sat (ctx[a1eW5] t[a1eRr])) => Rep1 ctx[a1eW5] (Bind p[a1eRq] t[a1eRr]) 
(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[a1eRq], Rep t[a1eRr]) => Rep (Bind p[a1eRq] t[a1eRr]) 
(Alpha p, Alpha t) => Alpha (Bind p t) 

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.

Constructors

R p1 p2 

Instances

(Rep p1[a1eRo], Rep p2[a1eRp], Sat (ctx[a1eVK] p1[a1eRo]), Sat (ctx[a1eVK] p2[a1eRp])) => Rep1 ctx[a1eVK] (Rebind p1[a1eRo] p2[a1eRp]) 
(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[a1eRo], Rep p2[a1eRp]) => Rep (Rebind p1[a1eRo] p2[a1eRp]) 
(Alpha p, Alpha q) => Alpha (Rebind p q) 

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.

Constructors

Rec p 

Instances

(Rep p[a1eRn], Sat (ctx[a1eVC] p[a1eRn])) => Rep1 ctx[a1eVC] (Rec p[a1eRn]) 
(Alpha a, Subst c a) => Subst c (Rec a) 
Show a => Show (Rec a) 
Rep p[a1eRn] => Rep (Rec p[a1eRn]) 
Alpha p => Alpha (Rec p) 

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

Constructors

TRec (Bind (Rec p) ()) 

Instances

Show a => Show (TRec a) 

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 t[a1eRl], Sat (ctx[a1eVX] t[a1eRl])) => Rep1 ctx[a1eVX] (Embed t[a1eRl]) 
Subst c a => Subst c (Embed a) 
Eq t => Eq (Embed t) 
Show a => Show (Embed a) 
Rep t[a1eRl] => Rep (Embed t[a1eRl]) 
IsEmbed (Embed t) 
Alpha t => Alpha (Embed t) 

newtype Shift p Source

Shift the scope of an embedded term one level outwards.

Constructors

Shift p 

Instances

(Rep p[a1eRk], Sat (ctx[a1eVu] p[a1eRk])) => Rep1 ctx[a1eVu] (Shift p[a1eRk]) 
Eq p => Eq (Shift p) 
Show a => Show (Shift a) 
Rep p[a1eRk] => Rep (Shift p[a1eRk]) 
IsEmbed e => IsEmbed (Shift e) 
Alpha a => Alpha (Shift a) 

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.

rBind :: forall p[a1eRq] t[a1eRr]. (Rep p[a1eRq], Rep t[a1eRr]) => R (Bind p[a1eRq] t[a1eRr])Source

rRebind :: forall p1[a1eRo] p2[a1eRp]. (Rep p1[a1eRo], Rep p2[a1eRp]) => R (Rebind p1[a1eRo] p2[a1eRp])Source

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

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

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