Copyright	(C) 2012-2013 Edward Kmett
License	BSD-style (see the file LICENSE)
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	portable
Safe Haskell	Trustworthy
Language	Haskell98

Bound.Scope

Contents

Abstraction
Instantiation
Traditional de Bruijn
Bound variable manipulation

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

newtype Scope b f a = Scope {
- unscope :: f (Var b (f a))
}
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
instantiate1 :: Monad f => f a -> Scope n f a -> f a
instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c
fromScope :: Monad f => Scope b f a -> f (Var b a)
toScope :: Monad f => f (Var b a) -> Scope b f a
splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c
bindings :: Foldable f => Scope b f a -> [b]
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a
mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c
liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a
liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c
foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r
foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> r
traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()
traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()
mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()
mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()
traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)
traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)
mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)
mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)
hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a
bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c')
transverseScope :: (Applicative f, Monad f, Traversable g) => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a)
instantiateVars :: Monad t => [a] -> Scope Int t a -> t a

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
Fields unscope :: f (Var b (f a))

Instances

MonadTrans (Scope b) Source #
Instance details Defined in Bound.Scope Methods lift :: Monad m => m a -> Scope b m a #
Bound (Scope b) Source #
Instance details Defined in Bound.Scope Methods (>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c Source #
MFunctor (Scope b :: (Type -> Type) -> Type -> Type) Source #
Instance details Defined in Bound.Scope Methods hoist :: Monad m => (forall a. m a -> n a) -> Scope b m b0 -> Scope b n b0 #
Functor f => Generic1 (Scope b f :: Type -> Type) Source #
Instance details Defined in Bound.Scope Associated Types type Rep1 (Scope b f) :: k -> Type # Methods from1 :: Scope b f a -> Rep1 (Scope b f) a # to1 :: Rep1 (Scope b f) a -> Scope b f a #
Monad f => Monad (Scope b f) Source #	The monad permits substitution on free variables, while preserving bound variables
Instance details Defined in Bound.Scope Methods (>>=) :: Scope b f a -> (a -> Scope b f b0) -> Scope b f b0 # (>>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 # return :: a -> Scope b f a # fail :: String -> Scope b f a #
Functor f => Functor (Scope b f) Source #
Instance details Defined in Bound.Scope Methods fmap :: (a -> b0) -> Scope b f a -> Scope b f b0 # (<$) :: a -> Scope b f b0 -> Scope b f a #
(Functor f, Monad f) => Applicative (Scope b f) Source #
Instance details Defined in Bound.Scope Methods pure :: a -> Scope b f a # (<>) :: Scope b f (a -> b0) -> Scope b f a -> Scope b f b0 # liftA2 :: (a -> b0 -> c) -> Scope b f a -> Scope b f b0 -> Scope b f c # (>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 # (<*) :: Scope b f a -> Scope b f b0 -> Scope b f a #
Foldable f => Foldable (Scope b f) Source #	`toList` is provides a list (with duplicates) of the free variables
Instance details Defined in Bound.Scope Methods fold :: Monoid m => Scope b f m -> m # foldMap :: Monoid m => (a -> m) -> Scope b f a -> m # foldr :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 # foldr' :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 # foldl :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 # foldl' :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 # foldr1 :: (a -> a -> a) -> Scope b f a -> a # foldl1 :: (a -> a -> a) -> Scope b f a -> a # toList :: Scope b f a -> [a] # null :: Scope b f a -> Bool # length :: Scope b f a -> Int # elem :: Eq a => a -> Scope b f a -> Bool # maximum :: Ord a => Scope b f a -> a # minimum :: Ord a => Scope b f a -> a # sum :: Num a => Scope b f a -> a # product :: Num a => Scope b f a -> a #
Traversable f => Traversable (Scope b f) Source #
Instance details Defined in Bound.Scope Methods traverse :: Applicative f0 => (a -> f0 b0) -> Scope b f a -> f0 (Scope b f b0) # sequenceA :: Applicative f0 => Scope b f (f0 a) -> f0 (Scope b f a) # mapM :: Monad m => (a -> m b0) -> Scope b f a -> m (Scope b f b0) # sequence :: Monad m => Scope b f (m a) -> m (Scope b f a) #
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods liftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool #
(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods liftCompare :: (a -> b0 -> Ordering) -> Scope b f a -> Scope b f b0 -> Ordering #
(Read b, Read1 f) => Read1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Scope b f a) # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Scope b f a] # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Scope b f a) # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Scope b f a] #
(Show b, Show1 f) => Show1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS #
(Serial b, Serial1 f) => Serial1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods serializeWith :: MonadPut m => (a -> m ()) -> Scope b f a -> m () # deserializeWith :: MonadGet m => m a -> m (Scope b f a) #
(Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) Source #
Instance details Defined in Bound.Scope Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Scope b f a -> Int #
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods (==) :: Scope b f a -> Scope b f a -> Bool # (/=) :: Scope b f a -> Scope b f a -> Bool #
(Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Scope b f a -> c (Scope b f a) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scope b f a) # toConstr :: Scope b f a -> Constr # dataTypeOf :: Scope b f a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scope b f a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scope b f a)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Scope b f a -> Scope b f a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r # gmapQ :: (forall d. Data d => d -> u) -> Scope b f a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope b f a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) #
(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods compare :: Scope b f a -> Scope b f a -> Ordering # (<) :: Scope b f a -> Scope b f a -> Bool # (<=) :: Scope b f a -> Scope b f a -> Bool # (>) :: Scope b f a -> Scope b f a -> Bool # (>=) :: Scope b f a -> Scope b f a -> Bool # max :: Scope b f a -> Scope b f a -> Scope b f a # min :: Scope b f a -> Scope b f a -> Scope b f a #
(Read b, Read1 f, Read a) => Read (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods readsPrec :: Int -> ReadS (Scope b f a) # readList :: ReadS [Scope b f a] # readPrec :: ReadPrec (Scope b f a) # readListPrec :: ReadPrec [Scope b f a] #
(Show b, Show1 f, Show a) => Show (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods showsPrec :: Int -> Scope b f a -> ShowS # show :: Scope b f a -> String # showList :: [Scope b f a] -> ShowS #
Generic (Scope b f a) Source #
Instance details Defined in Bound.Scope Associated Types type Rep (Scope b f a) :: Type -> Type # Methods from :: Scope b f a -> Rep (Scope b f a) x # to :: Rep (Scope b f a) x -> Scope b f a #
(Binary b, Serial1 f, Binary a) => Binary (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods put :: Scope b f a -> Put # get :: Get (Scope b f a) # putList :: [Scope b f a] -> Put #
(Serial b, Serial1 f, Serial a) => Serial (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods serialize :: MonadPut m => Scope b f a -> m () # deserialize :: MonadGet m => m (Scope b f a) #
(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods put :: Putter (Scope b f a) # get :: Get (Scope b f a) #
NFData (f (Var b (f a))) => NFData (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods rnf :: Scope b f a -> () #
(Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) Source #
Instance details Defined in Bound.Scope Methods hashWithSalt :: Int -> Scope b f a -> Int # hash :: Scope b f a -> Int #
type Rep1 (Scope b f :: Type -> Type) Source #
Instance details Defined in Bound.Scope type Rep1 (Scope b f :: Type -> Type) = D1 (MetaData "Scope" "Bound.Scope" "bound-2.0.1-AtZsY3yZaEKLBfeR1JA5NI" True) (C1 (MetaCons "Scope" PrefixI True) (S1 (MetaSel (Just "unscope") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (f :.: (Var b :.: Rec1 f))))
type Rep (Scope b f a) Source #
Instance details Defined in Bound.Scope type Rep (Scope b f a) = D1 (MetaData "Scope" "Bound.Scope" "bound-2.0.1-AtZsY3yZaEKLBfeR1JA5NI" True) (C1 (MetaCons "Scope" PrefixI True) (S1 (MetaSel (Just "unscope") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f (Var b (f a))))))

Abstraction

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a Source #

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 a Source #

Abstract over a single variable

>>> abstract1 'x' "xyz"
Scope [B (),F "y",F "z"]

abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c Source #

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

Instantiation

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

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 a Source #

Enter a Scope that binds one variable, instantiating it

>>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
"xyz"

instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c Source #

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

Traditional de Bruijn

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 a Source #

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 c Source #

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 a Source #

Perform a change of variables on bound variables.

mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c Source #

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

liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a Source #

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 c Source #

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 -> r Source #

Obtain a result by collecting information from bound variables

foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> r Source #

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 the bound variables in a Scope.

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

serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m () Source #

deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v) Source #

hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a Source #

Lift a natural transformation from f to g into one between scopes.

bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a') Source #

This allows you to bitraverse a Scope.

bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c') Source #

transverseScope :: (Applicative f, Monad f, Traversable g) => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a) Source #

This is a higher-order analogue of traverse.

instantiateVars :: Monad t => [a] -> Scope Int t a -> t a Source #

instantiate bound variables using a list of new variables