Bound.Scope

Documentation

newtype Scope b f a

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

Fields

unscope :: f (Var b (f a))

Instances

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)

Foldable f => Foldable (Scope b f)

toList is provides a list (with duplicates) of the free variables

Traversable f => Traversable (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)

(Monad f, Eq b, Eq1 f, Eq a) => Eq (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)

Abstraction

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

Capture some free variables in an expression to yield a Scope with bound variables in b

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

Abstract over a single variable

Instantiation

instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

Enter a scope, instantiating all bound variables

instantiate1 :: Monad f => f a -> Scope () f a -> f a

Enter a Scope that binds one variable, instantiating it

Traditional de Bruijn

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

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.

 fromScope . toScope = id
 fromScope . toScope . fromScope = fromScope

(toScope . fromScope) is idempotent

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

Bound variable manipulation

splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c

Perform substitution on both bound and free variables in a Scope

bindings :: Foldable f => Scope b f a -> [b]

mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a

Perform a change of variables on bound variables

mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c

Perform a change of variables, reassigning both bound and free variables.

liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a

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

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

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

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

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

mapM_ over the variables bound by this scope

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)