bound-0.4: Haskell 98/2010 Locally-Nameless Generalized de Bruijn Terms

Portability portable experimental Edward Kmett Safe-Infered

Bound.Scope

Description

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

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 aSource

Abstract over a single variable

# Instantiation

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

Enter a scope, instantiating all bound variables

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

Enter a `Scope` that binds one variable, instantiating it

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.

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

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

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

traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()Source

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

mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)Source

mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)Source