Copyright  (C) 20122013 Edward Kmett 

License  BSDstyle (see the file LICENSE) 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Stability  experimental 
Portability  portable 
Safe Haskell  Trustworthy 
Language  Haskell98 
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)
 serializeScope :: (Serial1 f, MonadPut m) => (b > m ()) > (v > m ()) > Scope b f v > m ()
 deserializeScope :: (Serial1 f, MonadGet m) => m b > m v > m (Scope b f v)
 hoistScope :: Functor f => (forall x. f x > g x) > Scope b f a > Scope b g a
 bitraverseScope :: (Bitraversable t, Applicative f) => (k > f k') > (a > f a') > Scope b (t k) a > f (Scope b (t k') a')
 bitransverseScope :: Applicative f => (forall a a'. (a > f a') > t a > f (u a')) > (c > f c') > Scope b t c > f (Scope b u c')
 transverseScope :: (Applicative f, Monad f, Traversable g) => (forall r. g r > f (h r)) > Scope b g a > f (Scope b h a)
 instantiateVars :: Monad t => [a] > Scope Int t a > t a
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)  
(Functor f, Monad f) => Applicative (Scope b f)  
Foldable f => Foldable (Scope b f) 

Traversable f => Traversable (Scope b f)  
(Serial b, Serial1 f) => Serial1 (Scope b f)  
(Hashable b, Monad f, Hashable1 f) => Hashable1 (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)  
Typeable (* > (* > *) > * > *) Scope  
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a)  
(Typeable * b, Typeable (* > *) f, Data a, Data (f (Var b (f a)))) => Data (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)  
(Binary b, Serial1 f, Binary a) => Binary (Scope b f a)  
(Serial b, Serial1 f, Serial a) => Serial (Scope b f a)  
(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a)  
(Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) 
Abstraction
abstract :: Monad f => (a > Maybe b) > f a > Scope b f a Source
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 a Source
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 a Source
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 a Source
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 a Source
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 c Source
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 a Source
Perform a change of variables on bound variables.
mapScope :: Functor f => (b > d) > (a > c) > Scope b f a > Scope d f c Source
Perform a change of variables, reassigning both bound and free variables.
liftMBound :: Monad m => (b > b') > Scope b m a > Scope b' m a Source
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 c Source
foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > r Source
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 > r Source
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
serializeScope :: (Serial1 f, MonadPut m) => (b > m ()) > (v > m ()) > Scope b f v > m () Source
deserializeScope :: (Serial1 f, MonadGet m) => m b > m v > m (Scope b f v) Source
hoistScope :: Functor f => (forall x. f x > g x) > Scope b f a > Scope b g a Source
Lift a natural transformation from f
to g
into one between scopes.
bitraverseScope :: (Bitraversable t, Applicative f) => (k > f k') > (a > f a') > Scope b (t k) a > f (Scope b (t k') a') Source
This allows you to bitraverse
a Scope
.
bitransverseScope :: Applicative f => (forall a a'. (a > f a') > t a > f (u a')) > (c > f c') > Scope b t c > f (Scope b u c') Source
transverseScope :: (Applicative f, Monad f, Traversable g) => (forall r. g r > f (h r)) > Scope b g a > f (Scope b h a) Source
This is a higherorder analogue of traverse
.
instantiateVars :: Monad t => [a] > Scope Int t a > t a Source
instantiate bound variables using a list of new variables