Portability | GHC only |
---|---|

Stability | experimental |

Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |

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.

B p t |

(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`

.

R p1 p2 |

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

Rec p |

`TRec`

is a standalone variant of `Rec`

: the only difference is
that whereas

is a pattern type, `Rec`

p`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,

corresponds to
alpha-Caml's `Embed`

t`inner t`

, and

corresponds to
alpha-Caml's `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
`Shift`

s at the same time.)

Embed t |

Shift the scope of an embedded term one level outwards.

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.