Bound.ScopeT

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

Consider using ScopeH, it might be clearer.

Documentation

newtype ScopeT b t f a

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

Fields

• unscopeT :: t f (Var b (f a))

Instances

(forall (f :: Type -> Type). Functor f => Functor (t f)) => Bound (ScopeT n t)

(>>>=) :: ... => ScopeT n t f a -> (a -> f b) -> ScopeT n t f b

Defined in Bound.ScopeT

Methods

(>>>=) :: Monad f => ScopeT n t f a -> (a -> f c) -> ScopeT n t f c

(Functor (t f), Functor f) => Functor (ScopeT b t f)

Defined in Bound.ScopeT

Methods

fmap :: (a -> b0) -> ScopeT b t f a -> ScopeT b t f b0

(<$) :: a -> ScopeT b t f b0 -> ScopeT b t f a

(Foldable (t f), Foldable f) => Foldable (ScopeT b t f)

Defined in Bound.ScopeT

Methods

fold :: Monoid m => ScopeT b t f m -> m

foldMap :: Monoid m => (a -> m) -> ScopeT b t f a -> m

foldr :: (a -> b0 -> b0) -> b0 -> ScopeT b t f a -> b0

foldr' :: (a -> b0 -> b0) -> b0 -> ScopeT b t f a -> b0

foldl :: (b0 -> a -> b0) -> b0 -> ScopeT b t f a -> b0

foldl' :: (b0 -> a -> b0) -> b0 -> ScopeT b t f a -> b0

foldr1 :: (a -> a -> a) -> ScopeT b t f a -> a

foldl1 :: (a -> a -> a) -> ScopeT b t f a -> a

toList :: ScopeT b t f a -> [a]

null :: ScopeT b t f a -> Bool

length :: ScopeT b t f a -> Int

elem :: Eq a => a -> ScopeT b t f a -> Bool

maximum :: Ord a => ScopeT b t f a -> a

minimum :: Ord a => ScopeT b t f a -> a

sum :: Num a => ScopeT b t f a -> a

product :: Num a => ScopeT b t f a -> a

(Traversable (t f), Traversable f) => Traversable (ScopeT b t f)

Defined in Bound.ScopeT

Methods

traverse :: Applicative f0 => (a -> f0 b0) -> ScopeT b t f a -> f0 (ScopeT b t f b0)

sequenceA :: Applicative f0 => ScopeT b t f (f0 a) -> f0 (ScopeT b t f a)

mapM :: Monad m => (a -> m b0) -> ScopeT b t f a -> m (ScopeT b t f b0)

sequence :: Monad m => ScopeT b t f (m a) -> m (ScopeT b t f a)

(Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f) => Eq1 (ScopeT b t f)

Defined in Bound.ScopeT

Methods

liftEq :: (a -> b0 -> Bool) -> ScopeT b t f a -> ScopeT b t f b0 -> Bool

(Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f) => Ord1 (ScopeT b t f)

Defined in Bound.ScopeT

Methods

liftCompare :: (a -> b0 -> Ordering) -> ScopeT b t f a -> ScopeT b t f b0 -> Ordering

(Read b, Read1 (t f), Read1 f) => Read1 (ScopeT b t f)

Defined in Bound.ScopeT

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ScopeT b t f a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ScopeT b t f a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (ScopeT b t f a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [ScopeT b t f a]

(Show b, Show1 (t f), Show1 f) => Show1 (ScopeT b t f)

Defined in Bound.ScopeT

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ScopeT b t f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ScopeT b t f a] -> ShowS

(Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f)) => Hashable1 (ScopeT b t f)

Defined in Bound.ScopeT

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> ScopeT b t f a -> Int

(Monad f, Functor (t f)) => Module (ScopeT b t f) f

Defined in Bound.ScopeT

Methods

(>>==) :: ScopeT b t f a -> (a -> f b0) -> ScopeT b t f b0

(Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f, Eq a) => Eq (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

(==) :: ScopeT b t f a -> ScopeT b t f a -> Bool

(/=) :: ScopeT b t f a -> ScopeT b t f a -> Bool

(Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f, Ord a) => Ord (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

compare :: ScopeT b t f a -> ScopeT b t f a -> Ordering

(<) :: ScopeT b t f a -> ScopeT b t f a -> Bool

(<=) :: ScopeT b t f a -> ScopeT b t f a -> Bool

(>) :: ScopeT b t f a -> ScopeT b t f a -> Bool

(>=) :: ScopeT b t f a -> ScopeT b t f a -> Bool

max :: ScopeT b t f a -> ScopeT b t f a -> ScopeT b t f a

min :: ScopeT b t f a -> ScopeT b t f a -> ScopeT b t f a

(Read b, Read1 (t f), Read1 f, Read a) => Read (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

readsPrec :: Int -> ReadS (ScopeT b t f a)

readList :: ReadS [ScopeT b t f a]

readPrec :: ReadPrec (ScopeT b t f a)

readListPrec :: ReadPrec [ScopeT b t f a]

(Show b, Show1 (t f), Show1 f, Show a) => Show (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

showsPrec :: Int -> ScopeT b t f a -> ShowS

show :: ScopeT b t f a -> String

showList :: [ScopeT b t f a] -> ShowS

NFData (t f (Var b (f a))) => NFData (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

rnf :: ScopeT b t f a -> ()

(Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f), Hashable a) => Hashable (ScopeT b t f a)

Defined in Bound.ScopeT

Methods

hashWithSalt :: Int -> ScopeT b t f a -> Int

hash :: ScopeT b t f a -> Int

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

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

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

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

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

Abstraction, capturing named bound variables.

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

Abstract over a single variable

Instantiation

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

Enter a ScopeT, instantiating all bound variables

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

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

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

Traditional de Bruijn

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

Convert to traditional de Bruijn.

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

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

Convert to Scope.

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

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

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

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

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

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

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

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

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

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)

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)

traverse both bound and free variables

bitransverseScopeT

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.