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.
Synopsis
 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
 abstractEither :: Monad f => (a > Either b c) > f a > Scope b f c
 instantiate :: Monad f => (b > f a) > Scope b f a > f a
 instantiate1 :: Monad f => f a > Scope n f a > f a
 instantiateEither :: Monad f => (Either b a > 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
 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
.
Instances
MonadTrans (Scope b) Source #  
Defined in Bound.Scope  
Bound (Scope b) Source #  
MFunctor (Scope b :: (Type > Type) > Type > Type) Source #  
Functor f => Generic1 (Scope b f :: Type > Type) Source #  
Monad f => Monad (Scope b f) Source #  The monad permits substitution on free variables, while preserving bound variables 
Functor f => Functor (Scope b f) Source #  
(Functor f, Monad f) => Applicative (Scope b f) Source #  
Foldable f => Foldable (Scope b f) Source # 

Defined in Bound.Scope fold :: Monoid m => Scope b f m > m # foldMap :: Monoid m => (a > m) > Scope b f a > m # foldr :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldr' :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldl :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldl' :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldr1 :: (a > a > a) > Scope b f a > a # foldl1 :: (a > a > a) > Scope b f a > a # toList :: Scope b f a > [a] # length :: Scope b f a > Int # elem :: Eq a => a > Scope b f a > Bool # maximum :: Ord a => Scope b f a > a # minimum :: Ord a => Scope b f a > a #  
Traversable f => Traversable (Scope b f) Source #  
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) Source #  
(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) Source #  
Defined in Bound.Scope  
(Read b, Read1 f) => Read1 (Scope b f) Source #  
Defined in Bound.Scope  
(Show b, Show1 f) => Show1 (Scope b f) Source #  
(Serial b, Serial1 f) => Serial1 (Scope b f) Source #  
Defined in Bound.Scope serializeWith :: MonadPut m => (a > m ()) > Scope b f a > m () # deserializeWith :: MonadGet m => m a > m (Scope b f a) #  
(Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) Source #  
Defined in Bound.Scope  
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) Source #  
(Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a) Source #  
Defined in Bound.Scope gfoldl :: (forall d b0. Data d => c (d > b0) > d > c b0) > (forall g. g > c g) > Scope b f a > c (Scope b f a) # gunfold :: (forall b0 r. Data b0 => c (b0 > r) > c r) > (forall r. r > c r) > Constr > c (Scope b f a) # toConstr :: Scope b f a > Constr # dataTypeOf :: Scope b f a > DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) > Maybe (c (Scope b f a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) > Maybe (c (Scope b f a)) # gmapT :: (forall b0. Data b0 => b0 > b0) > Scope b f a > Scope b f a # gmapQl :: (r > r' > r) > r > (forall d. Data d => d > r') > Scope b f a > r # gmapQr :: (r' > r > r) > r > (forall d. Data d => d > r') > Scope b f a > r # gmapQ :: (forall d. Data d => d > u) > Scope b f a > [u] # gmapQi :: Int > (forall d. Data d => d > u) > Scope b f a > u # gmapM :: Monad m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) # gmapMp :: MonadPlus m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) # gmapMo :: MonadPlus m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) #  
(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) Source #  
(Read b, Read1 f, Read a) => Read (Scope b f a) Source #  
(Show b, Show1 f, Show a) => Show (Scope b f a) Source #  
Generic (Scope b f a) Source #  
(Binary b, Serial1 f, Binary a) => Binary (Scope b f a) Source #  
(Serial b, Serial1 f, Serial a) => Serial (Scope b f a) Source #  
Defined in Bound.Scope  
(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) Source #  
NFData (f (Var b (f a))) => NFData (Scope b f a) Source #  
Defined in Bound.Scope  
(Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) Source #  
Defined in Bound.Scope  
type Rep1 (Scope b f :: Type > Type) Source #  
type Rep (Scope b f a) Source #  
Defined in Bound.Scope 
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"]
abstractEither :: Monad f => (a > Either b c) > f a > Scope b f c Source #
Capture some free variables in an expression to yield
a Scope
with bound variables in b
. Optionally change the
types of the remaining free variables.
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"
instantiateEither :: Monad f => (Either b a > f c) > Scope b f a > f c Source #
Enter a scope, and instantiate all bound and free variables in one go.
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
foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > r Source #
Obtain a result by collecting information from bound 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 #
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 #
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
.