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.