Copyright | (C) 2012-2013 Edward Kmett |
---|---|

License | BSD-style (see the file LICENSE) |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Stability | experimental |

Portability | portable |

Safe Haskell | Trustworthy |

Language | Haskell98 |

This is the work-horse 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
- 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 a`f`

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`

.

# 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`

`>>>`

Scope [B 0,B 1,B 2,B 2,F "y"]`abstract (`elemIndex` "bar") "barry"`

abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a Source #

Abstract over a single variable

`>>>`

Scope [B (),F "y",F "z"]`abstract1 'x' "xyz"`

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`

`>>>`

"abccy"`instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"`

instantiate1 :: Monad f => f a -> Scope n f a -> f a Source #

Enter a `Scope`

that binds one variable, instantiating it

`>>>`

"xyz"`instantiate1 "x" $ Scope [B (),F "y",F "z"]`

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 higher-order analogue of `traverse`

.