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

Portability GHC only experimental Brent Yorgey None

Unbound.LocallyNameless.Types

Description

Special type combinators for specifying binding structure.

Synopsis

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) (Binary p, Binary t) => Binary (GenBind order card p t) (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 Bind p t = GenBind StrictOrder StrictCard p tSource

type SetBind p t = GenBind RelaxedOrder StrictCard p tSource

type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p tSource

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 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) (Binary p1, Binary p2) => Binary (Rebind p1 p2) (Rep p10, Rep p20) => Rep (Rebind p10 p20) (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 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)

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 `Shift`s 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) Binary p => Binary (Embed p) Rep t0 => Rep (Embed t0) 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 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)

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.

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