Abt.Class.Abt

Documentation

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

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

Methods

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

Convert a View into a term.

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

Convert a term into a simple View.

var :: v -> t Z

The injection from variables to terms.

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

Construct an abstraction.

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

Construct an operator term.

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

Substitute a term for a variable.

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

Instantiate the bound variable of an abstraction.

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

Compute the free variables of a term.

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

Render a term into a human-readable string.

Instances

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