Copyright | (C) 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 |

`Scope`

provides a single traditional de Bruijn level
and is often used inside of the definition of binders.

- newtype Scope b f a = Scope {}
- abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a
- abstract1 :: (Functor 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 :: Scope b f a -> f (Var b a)
- toScope :: 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 :: (f (Var b a) -> g (Var b a)) -> 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')) -> forall a a'. (a -> f a') -> Scope b t a -> f (Scope b u a')
- transverseScope :: Functor f => (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`

This implements traditional de Bruijn indices, while `Scope`

implements generalized de Bruijn indices.

These traditional indices can be used to test the performance gain of generalized indices.

While this type `Scope`

is identical to `EitherT`

this module focuses on a drop-in replacement for `Scope`

.

Another use case is for syntaxes not stable under substitution,
therefore with only a `Functor`

instance and no `Monad`

instance.

# Abstraction

abstract :: Functor 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 :: (Functor f, Eq a) => a -> f a -> Scope () f a Source #

Abstract over a single variable

`>>>`

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

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

# Alternative names for 'unscope'/'Scope'

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

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')) -> forall a a'. (a -> f a') -> Scope b t a -> f (Scope b u a') Source #