bound-0.9.1.1: Making de Bruijn Succ Less

Portability portable experimental Edward Kmett Trustworthy

Bound.Scope

Description

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.

Synopsis

# Documentation

newtype Scope b f a Source

Scope b f a is an 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.

Constructors

 Scope Fieldsunscope :: f (Var b (f a))

Instances

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

fromScope :: Monad f => Scope b f a -> f (Var b a)Source

fromScope quotients out the possible placements of F in Scope by distributing them all to the leaves. This yields a more traditional de Bruijn indexing scheme for bound variables.

Since,

fromScope . toScopeid

we know that

fromScope . toScope . fromScopefromScope

and therefore (toScope . fromScope) is idempotent.

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

A version of mapScope that can be used when you only have the Monad instance

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

traverse_ the bound variables in a Scope.

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