abt- Abstract binding trees for Haskell

Safe HaskellNone




class (Show1 o, Show v) => Abt v o t | t -> v o where Source

The Abt signature represents mediation between an arbitrary (possibly nameless) term representaion, and a simple one (the View). Based on the (effectful) ismorphism into / out between representations, many operations can be defined generically for arbitrary operator sets, including substitution and aggregation of free variables.

Minimal complete definition

into, out


into :: View v o n t -> t n Source

Convert a View into a term.

out :: MonadVar v m => t n -> m (View v o n t) Source

Convert a term into a simple View.

var :: v -> t Z Source

The injection from variables to terms.

(\\) :: v -> t n -> t (S n) Source

Construct an abstraction.

($$) :: o ns -> Rec t ns -> t Z infixl 1 Source

Construct an operator term.

subst :: MonadVar v m => t Z -> v -> t n -> m (t n) Source

Substitute a term for a variable.

(//) :: MonadVar v m => t (S n) -> t Z -> m (t n) Source

Instantiate the bound variable of an abstraction.

freeVars :: MonadVar v m => t n -> m [v] Source

Compute the free variables of a term.

toString :: MonadVar v m => t n -> m String Source

Render a term into a human-readable string.


Show1 [Nat] o => Abt Var o (Tm o)