Portability  portable 

Stability  experimental 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Safe Haskell  None 
This is the workhorse of the bound
library.
Scope
provides a single generalized de Bruijn level
and is often used inside of the definition of binders.
 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 n f a > f a
 fromScope :: Monad f => Scope b f a > f (Var b a)
 toScope :: Monad f => f (Var b a) > Scope b f a
 splat :: Monad f => (a > f c) > (b > f c) > Scope b f a > f c
 bindings :: Foldable f => Scope b f a > [b]
 mapBound :: Functor f => (b > b') > Scope b f a > Scope b' f a
 mapScope :: Functor f => (b > d) > (a > c) > Scope b f a > Scope d f c
 liftMBound :: Monad m => (b > b') > Scope b m a > Scope b' m a
 liftMScope :: Monad m => (b > d) > (a > c) > Scope b m a > Scope d m c
 foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > r
 foldMapScope :: (Foldable f, Monoid r) => (b > r) > (a > r) > Scope b f a > r
 traverseBound_ :: (Applicative g, Foldable f) => (b > g d) > Scope b f a > g ()
 traverseScope_ :: (Applicative g, Foldable f) => (b > g d) > (a > g c) > Scope b f a > g ()
 mapMBound_ :: (Monad g, Foldable f) => (b > g d) > Scope b f a > g ()
 mapMScope_ :: (Monad m, Foldable f) => (b > m d) > (a > m c) > Scope b f a > m ()
 traverseBound :: (Applicative g, Traversable f) => (b > g c) > Scope b f a > g (Scope c f a)
 traverseScope :: (Applicative g, Traversable f) => (b > g d) > (a > g c) > Scope b f a > g (Scope d f c)
 mapMBound :: (Monad m, Traversable f) => (b > m c) > Scope b f a > m (Scope c f a)
 mapMScope :: (Monad m, Traversable f) => (b > m d) > (a > m c) > Scope b f a > m (Scope d f c)
Documentation
is an Scope
b f af
expression with bound variables in b
,
and free variables in a
We store bound variables as their generalized de Bruijn
representation in that we're allowed to lift
(using F
) an entire
tree rather than only succ individual variables, but we're still
only allowed to do so once per Scope
. Weakening trees permits
O(1) weakening and permits 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 generalized de Bruijn representation and return the
same result as a traditional de Bruijn representation would.
Logically you can think of this as if the shape were the traditional
f (Var b a)
, but the extra f a
inside permits us a cheaper lift
.
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 in b
>>>
:m + Data.List
>>>
abstract (`elemIndex` "bar") "barry"
Scope [B 0,B 1,B 2,B 2,F "y"]
abstract1 :: (Monad f, Eq a) => a > f a > Scope () f aSource
Abstract over a single variable
>>>
abstract1 'x' "xyz"
Scope [B (),F "y",F "z"]
Instantiation
instantiate :: Monad f => (b > f a) > Scope b f a > f aSource
Enter a scope, instantiating all bound variables
>>>
:m + Data.List
>>>
instantiate (\x > [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
"abccy"
instantiate1 :: Monad f => f a > Scope n f a > f aSource
Enter a Scope
that binds one variable, instantiating it
>>>
instantiate1 "x" $ Scope [B (),F "y",F "z"]
"xyz"
Traditional de Bruijn
toScope :: Monad f => f (Var b a) > Scope b f aSource
Convert from traditional de Bruijn to generalized de Bruijn indices.
This requires a full tree traversal
Bound variable manipulation
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
.
bindings :: Foldable f => Scope b f a > [b]Source
Return a list of occurences of the variables bound by this Scope
.
mapBound :: Functor f => (b > b') > Scope b f a > Scope b' f aSource
Perform a change of variables on bound variables.
mapScope :: Functor f => (b > d) > (a > c) > Scope b f a > Scope d f cSource
Perform a change of variables, reassigning both bound and free variables.
liftMBound :: Monad m => (b > b') > Scope b m a > Scope b' m aSource
Perform a change of variables on bound variables given only a Monad
instance
liftMScope :: Monad m => (b > d) > (a > c) > Scope b m a > Scope d m cSource
foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > rSource
Obtain a result by collecting information from both bound and free variables
foldMapScope :: (Foldable f, Monoid r) => (b > r) > (a > r) > Scope b f a > rSource
Obtain a result by collecting information from both bound and free variables
traverseBound_ :: (Applicative g, Foldable f) => (b > g d) > Scope b f a > g ()Source
traverseScope_ :: (Applicative g, Foldable f) => (b > g d) > (a > g c) > Scope b f a > g ()Source
traverse
both the variables bound by this scope and any free variables.
mapMBound_ :: (Monad g, Foldable f) => (b > g d) > Scope b f a > g ()Source
mapM_ over the variables bound by this scope
mapMScope_ :: (Monad m, Foldable f) => (b > m d) > (a > m c) > Scope b f a > m ()Source
A traverseScope_
that can be used when you only have a Monad
instance
traverseBound :: (Applicative g, Traversable f) => (b > g c) > Scope b f a > g (Scope c f a)Source
Traverse both bound and free variables
traverseScope :: (Applicative g, Traversable f) => (b > g d) > (a > g c) > Scope b f a > g (Scope d f c)Source
Traverse both bound and free variables
mapMBound :: (Monad m, Traversable f) => (b > m c) > Scope b f a > m (Scope c f a)Source
mapM over both bound and free variables
mapMScope :: (Monad m, Traversable f) => (b > m d) > (a > m c) > Scope b f a > m (Scope d f c)Source
A traverseScope
that can be used when you only have a Monad
instance