bound-0.1.3: Combinators for manipulating 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 a an f expression with bound variables in b, and free variables in a

This stores bound variables as their generalized de Bruijn representation, in that the succ's for variable ids are allowed to occur anywhere within the tree permitting O(1) weakening and allowing 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 choice of a generalized de Bruijn representation and return the same result as a traditional de Bruijn representation would.

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 with one bound variable, instantiating it

# Substitution

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

# Quotienting

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