Safe Haskell | None |
---|---|

Language | Haskell2010 |

- class (Show1 o, Show v) => Abt v o t | t -> v o where
- into :: View v o n t -> t n
- out :: MonadVar v m => t n -> m (View v o n t)
- var :: v -> t Z
- (\\) :: v -> t n -> t (S n)
- ($$) :: o ns -> Rec t ns -> t Z
- subst :: MonadVar v m => t Z -> v -> t n -> m (t n)
- (//) :: MonadVar v m => t (S n) -> t Z -> m (t n)
- freeVars :: MonadVar v m => t n -> m [v]
- toString :: MonadVar v m => t n -> m String

# Documentation

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

between representations, many
operations can be defined generically for arbitrary operator sets, including
substitution and aggregation of free variables.`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`

.

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.