bound-0.5.1: Making de Bruijn Succ Less

Portability portable experimental Edward Kmett Safe-Inferred

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

 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 (Functor (Scope b f), Foldable (Scope b f), Traversable f) => Traversable (Scope b f) (Monad f, Eq b, Eq1 f) => Eq1 (Scope b 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) (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 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` `.` `toScope` ≡ `id``

we know that

``fromScope` `.` `toScope` `.` `fromScope` ≡ `fromScope``

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