Portability | portable |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Safe Haskell | Safe-Infered |
- newtype Scope b f a = Scope {}
- abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
- abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
- instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
- instantiate1 :: Monad f => f a -> Scope () f a -> f a
- splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c
- fromScope :: Monad f => Scope b f a -> f (Var b a)
- toScope :: Monad f => f (Var b a) -> Scope b f a
Documentation
Scope b f a
is a an f
expression with bound variables in b
, and free variables in a
This stores bound variables as their generalized de Bruijn representation,
in that the succ's for variable ids are allowed to occur anywhere within the tree
permitting O(1) weakening and allowing more sharing opportunities.
Here the deBruijn 0 is represented by the B
constructor of Var
, while the
de Bruijn succ
(which may be applied to an entire tree!) is handled by F
.
NB: equality and comparison quotient out the distinct F
placements allowed by
the choice of a generalized de Bruijn representation and return the same result as a traditional de Bruijn
representation would.
MonadTrans (Scope b) | |
Bound (Scope b) | |
Monad f => Monad (Scope b f) | The monad permits substitution on free variables, while preserving bound variables |
Functor f => Functor (Scope b f) | |
Foldable f => Foldable (Scope b f) |
|
Traversable f => Traversable (Scope b f) | |
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) | |
(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) | |
(Functor f, Show b, Show1 f) => Show1 (Scope b f) | |
(Functor f, Read b, Read1 f) => Read1 (Scope b f) | |
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) | |
(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) | |
(Functor f, Read b, Read1 f, Read a) => Read (Scope b f a) | |
(Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) |
Abstraction
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f aSource
Capture some free variables in an expression to yield a Scope with bound variables
Instantiation
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f aSource
Enter a scope, instantiating all bound variables
instantiate1 :: Monad f => f a -> Scope () f a -> f aSource
Enter a scope with one bound variable, instantiating it
Substitution
splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f cSource
Perform substitution on both bound and free variables in a scope
Quotienting
fromScope :: Monad f => Scope b f a -> f (Var b a)Source
fromScope
quotients out the possible placements of F in Scope
distributing them all to the leaves. This yields a traditional deBruijn
indexing scheme for bound variables.
fromScope . toScope = id fromScope . toScope . fromScope = fromScope
(toScope . fromScope)
is idempotent