bound-extras-0: ScopeH and ScopeT extras for bound

Bound.ScopeT

Description

ScopeT scope, which allows substitute f into 't f' to get new 't f'.

Consider using ScopeH, it might be clearer.

Synopsis

# Documentation

newtype ScopeT b t f a Source #

Scope b f a is a t f expression abstracted over f, with bound variables in b, and free variables in a.

Scope n f a ~ ScopeT n IdentityT f a
ScopeT n t f a ~ t (Scope n f) a


Constructors

 ScopeT FieldsunscopeT :: t f (Var b (f a))
Instances

(>>>>=) :: (Monad f, Functor (t f)) => ScopeT b t f a -> (a -> f c) -> ScopeT b t f c Source #

We cannot write Bound (ScopeT n t) pre-GHC-8.6 (without an auxiliary type class).

# Abstraction

abstractT :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT b t f a Source #

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

abstract1T :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT () t f a Source #

Abstract over a single variable.

>>> abstract1T 'x' (MaybeT (Nothing : map Just "xyz"))
ScopeT (MaybeT [Nothing,Just (B ()),Just (F "y"),Just (F "z")])


abstractTEither :: (Functor (t f), Monad f) => (a -> Either b c) -> t f a -> ScopeT b t f c Source #

Capture some free variables in an expression to yield a ScopeT with bound variables in b. Optionally change the types of the remaining free variables.

## Name

abstractTName :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a Source #

Abstraction, capturing named bound variables.

abstract1TName :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT (Name a ()) t f a Source #

Abstract over a single variable

# Instantiation

instantiateT :: (Bound t, Monad f) => (b -> f a) -> ScopeT b t f a -> t f a Source #

Enter a ScopeT, instantiating all bound variables

instantiate1T :: (Bound t, Monad f) => f a -> ScopeT b t f a -> t f a Source #

Enter a ScopeT that binds one variable, instantiating it

instantiateTEither :: (Bound t, Monad f) => (Either b a -> f c) -> ScopeT b t f a -> t f c Source #

Enter a ScopeT, and instantiate all bound and free variables in one go.

fromScopeT :: (Bound t, Monad f) => ScopeT b t f a -> t f (Var b a) Source #

toScopeT :: (Functor (t f), Monad f) => t f (Var b a) -> ScopeT b t f a Source #

Convert from traditional de Bruijn to generalized de Bruijn indices.

# Bound variable manipulation

lowerScopeT :: (Functor (t f), Functor f) => (forall x. t f x -> g x) -> (forall x. f x -> g x) -> ScopeT b t f a -> Scope b g a Source #

Convert to Scope.

splatT :: (Bound t, Monad f) => (a -> f c) -> (b -> f c) -> ScopeT b t f a -> t f c Source #

Perform substitution on both bound and free variables in a ScopeT.

bindingsT :: Foldable (t f) => ScopeT b t f a -> [b] Source #

Return a list of occurences of the variables bound by this ScopeT.

mapBoundT :: Functor (t f) => (b -> b') -> ScopeT b t f a -> ScopeT b' t f a Source #

Perform a change of variables on bound variables.

mapScopeT :: (Functor (t f), Functor f) => (b -> d) -> (a -> c) -> ScopeT b t f a -> ScopeT d t f c Source #

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

foldMapBoundT :: (Foldable (t f), Monoid r) => (b -> r) -> ScopeT b t f a -> r Source #

Obtain a result by collecting information from bound variables

foldMapScopeT :: (Foldable f, Foldable (t f), Monoid r) => (b -> r) -> (a -> r) -> ScopeT b t f a -> r Source #

Obtain a result by collecting information from both bound and free variables

traverseBoundT_ :: (Applicative g, Foldable (t f)) => (b -> g d) -> ScopeT b t f a -> g () Source #

traverse_ the bound variables in a Scope.

traverseScopeT_ :: (Applicative g, Foldable f, Foldable (t f)) => (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g () Source #

traverse_ both the variables bound by this scope and any free variables.

traverseBoundT :: (Applicative g, Traversable (t f)) => (b -> g c) -> ScopeT b t f a -> g (ScopeT c t f a) Source #

traverse the bound variables in a Scope.

traverseScopeT :: (Applicative g, Traversable f, Traversable (t f)) => (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g (ScopeT d t f c) Source #

traverse both bound and free variables

Arguments

 :: Applicative f => (forall x x'. (x -> f x') -> t s x -> f (t' s' x')) traverse-like for t -> (forall x x'. (x -> f x') -> s x -> f (s' x')) traverse-like for s -> (a -> f a') -> ScopeT b t s a -> f (ScopeT b t' s' a')

If you are looking for bitraverseScopeT, this is the monster you need.