Safe Haskell  None 

Language  Haskell2010 
ScopeH
scope, which allows substitute f
into g
to get new g
.
Compare following signatures:
instantiate1
:: ... => m a >Scope
b m a > m ainstantiate1H
:: ... => m a >ScopeH
b f m a > f a
ScopeH
variant allows to encode e.g. HindleyMilner types, where
we diffentiate between Poly
and Mono
morphic types.
specialise :: Poly a > Mono a > Poly a
specialise (Forall p) m = instantiate1H
m p
specialise _ _ = error "illkinded"
Another applications are bidirectional typesystems or representing normal forms with normal and neutral terms, aka introduction and elimination terms.
Look into examples/
directory for System F and Bidirectional STLC
implemented with a help of ScopeH
.
Synopsis
 newtype ScopeH b f m a = ScopeH {}
 abstractH :: (Functor f, Monad m) => (a > Maybe b) > f a > ScopeH b f m a
 abstract1H :: (Functor f, Monad m, Eq a) => a > f a > ScopeH () f m a
 abstractHEither :: (Functor f, Monad m) => (a > Either b c) > f a > ScopeH b f m c
 abstractHName :: (Functor f, Monad m) => (a > Maybe b) > f a > ScopeH (Name a b) f m a
 abstract1HName :: (Functor f, Monad m, Eq a) => a > f a > ScopeH (Name a ()) f m a
 instantiateH :: Module f m => (b > m a) > ScopeH b f m a > f a
 instantiate1H :: Module f m => m a > ScopeH b f m a > f a
 instantiateHEither :: Module f m => (Either b a > m c) > ScopeH b f m a > f c
 fromScopeH :: Module f m => ScopeH b f m a > f (Var b a)
 toScopeH :: (Functor f, Monad m) => f (Var b a) > ScopeH b f m a
 lowerScopeH :: (Functor f, Functor f) => (forall x. f x > h x) > (forall x. m x > h x) > ScopeH b f m a > Scope b h a
 convertFromScope :: Scope b f a > ScopeH b f f a
 splatH :: Module f m => (a > m c) > (b > m c) > ScopeH b f m a > f c
 bindingsH :: Foldable f => ScopeH b f m a > [b]
 mapBoundH :: Functor f => (b > b') > ScopeH b f m a > ScopeH b' f m a
 mapScopeH :: (Functor f, Functor m) => (b > d) > (a > c) > ScopeH b f m a > ScopeH d f m c
 foldMapBoundH :: (Foldable f, Monoid r) => (b > r) > ScopeH b f m a > r
 foldMapScopeH :: (Foldable f, Foldable m, Monoid r) => (b > r) > (a > r) > ScopeH b f m a > r
 traverseBoundH_ :: (Applicative g, Foldable f) => (b > g d) > ScopeH b f m a > g ()
 traverseScopeH_ :: (Applicative g, Foldable f, Foldable m) => (b > g d) > (a > g c) > ScopeH b f m a > g ()
 traverseBoundH :: (Applicative g, Traversable f) => (b > g c) > ScopeH b f m a > g (ScopeH c f m a)
 traverseScopeH :: (Applicative g, Traversable f, Traversable m) => (b > g d) > (a > g c) > ScopeH b f m a > g (ScopeH d f m c)
 bitraverseScopeH :: (Applicative g, Bitraversable f, Bitraversable m) => (k > g k') > (l > g l') > (a > g a') > ScopeH b (f k) (m l) a > g (ScopeH b (f k') (m l') a')
 bitransverseScopeH :: Applicative g => (forall x x'. (x > g x') > f x > g (f' x')) > (forall x x'. (x > g x') > m x > g (m' x')) > (a > g a') > ScopeH b f m a > g (ScopeH b f' m' a')
Documentation
newtype ScopeH b f m a Source #
is a ScopeH
b f m af
expression abstracted over g
,
with bound variables in b
, and free variables in a
.
Scope
b f a ~ScopeH
n f f aScopeT
b t f a ~ScopeH
b (t f) f a
Instances
(Functor f, Functor m) => Functor (ScopeH b f m) Source #  
(Foldable f, Foldable m) => Foldable (ScopeH b f m) Source #  
Defined in Bound.ScopeH fold :: Monoid m0 => ScopeH b f m m0 > m0 # foldMap :: Monoid m0 => (a > m0) > ScopeH b f m a > m0 # foldr :: (a > b0 > b0) > b0 > ScopeH b f m a > b0 # foldr' :: (a > b0 > b0) > b0 > ScopeH b f m a > b0 # foldl :: (b0 > a > b0) > b0 > ScopeH b f m a > b0 # foldl' :: (b0 > a > b0) > b0 > ScopeH b f m a > b0 # foldr1 :: (a > a > a) > ScopeH b f m a > a # foldl1 :: (a > a > a) > ScopeH b f m a > a # toList :: ScopeH b f m a > [a] # null :: ScopeH b f m a > Bool # length :: ScopeH b f m a > Int # elem :: Eq a => a > ScopeH b f m a > Bool # maximum :: Ord a => ScopeH b f m a > a # minimum :: Ord a => ScopeH b f m a > a #  
(Traversable f, Traversable m) => Traversable (ScopeH b f m) Source #  
Defined in Bound.ScopeH traverse :: Applicative f0 => (a > f0 b0) > ScopeH b f m a > f0 (ScopeH b f m b0) # sequenceA :: Applicative f0 => ScopeH b f m (f0 a) > f0 (ScopeH b f m a) # mapM :: Monad m0 => (a > m0 b0) > ScopeH b f m a > m0 (ScopeH b f m b0) # sequence :: Monad m0 => ScopeH b f m (m0 a) > m0 (ScopeH b f m a) #  
(Module f m, Eq b, Eq1 f, Eq1 m) => Eq1 (ScopeH b f m) Source #  
(Module f m, Ord b, Ord1 f, Ord1 m) => Ord1 (ScopeH b f m) Source #  
Defined in Bound.ScopeH  
(Read b, Read1 f, Read1 m) => Read1 (ScopeH b f m) Source #  
Defined in Bound.ScopeH liftReadsPrec :: (Int > ReadS a) > ReadS [a] > Int > ReadS (ScopeH b f m a) # liftReadList :: (Int > ReadS a) > ReadS [a] > ReadS [ScopeH b f m a] # liftReadPrec :: ReadPrec a > ReadPrec [a] > ReadPrec (ScopeH b f m a) # liftReadListPrec :: ReadPrec a > ReadPrec [a] > ReadPrec [ScopeH b f m a] #  
(Show b, Show1 f, Show1 m) => Show1 (ScopeH b f m) Source #  
(Hashable b, Module f m, Hashable1 f, Hashable1 m) => Hashable1 (ScopeH b f m) Source #  
Defined in Bound.ScopeH  
(Functor f, Monad m) => Module (ScopeH b f m) m Source #  
(Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq (ScopeH b f m a) Source #  
(Module f m, Ord b, Ord1 f, Ord1 m, Ord a) => Ord (ScopeH b f m a) Source #  
Defined in Bound.ScopeH compare :: ScopeH b f m a > ScopeH b f m a > Ordering # (<) :: ScopeH b f m a > ScopeH b f m a > Bool # (<=) :: ScopeH b f m a > ScopeH b f m a > Bool # (>) :: ScopeH b f m a > ScopeH b f m a > Bool # (>=) :: ScopeH b f m a > ScopeH b f m a > Bool #  
(Read b, Read1 f, Read1 m, Read a) => Read (ScopeH b f m a) Source #  
(Show b, Show1 f, Show1 m, Show a) => Show (ScopeH b f m a) Source #  
NFData (f (Var b (m a))) => NFData (ScopeH b f m a) Source #  
Defined in Bound.ScopeH  
(Hashable b, Module f m, Hashable1 f, Hashable1 m, Hashable a) => Hashable (ScopeH b f m a) Source #  
Defined in Bound.ScopeH 
Abstraction
abstractH :: (Functor f, Monad m) => (a > Maybe b) > f a > ScopeH b f m a Source #
Capture some free variables in an expression to yield a ScopeH
with bound variables in b
.
abstract1H :: (Functor f, Monad m, Eq a) => a > f a > ScopeH () f m a Source #
Abstract over a single variable.
abstractHEither :: (Functor f, Monad m) => (a > Either b c) > f a > ScopeH b f m c Source #
Capture some free variables in an expression to yield a ScopeH
with bound variables in b
. Optionally change the types of the remaining free variables.
Name
abstractHName :: (Functor f, Monad m) => (a > Maybe b) > f a > ScopeH (Name a b) f m a Source #
Abstraction, capturing named bound variables.
abstract1HName :: (Functor f, Monad m, Eq a) => a > f a > ScopeH (Name a ()) f m a Source #
Abstract over a single variable
Instantiation
instantiateH :: Module f m => (b > m a) > ScopeH b f m a > f a Source #
Enter a ScopeH
, instantiating all bound variables
instantiate1H :: Module f m => m a > ScopeH b f m a > f a Source #
Enter a ScopeH
that binds one variable, instantiating it
instantiateHEither :: Module f m => (Either b a > m c) > ScopeH b f m a > f c Source #
Enter a ScopeH
, and instantiate all bound and free variables in one go.
Traditional de Bruijn
toScopeH :: (Functor f, Monad m) => f (Var b a) > ScopeH b f m a Source #
Convert from traditional de Bruijn to generalized de Bruijn indices.
Bound variable manipulation
lowerScopeH :: (Functor f, Functor f) => (forall x. f x > h x) > (forall x. m x > h x) > ScopeH b f m a > Scope b h a Source #
Convert to Scope
.
convertFromScope :: Scope b f a > ScopeH b f f a Source #
splatH :: Module f m => (a > m c) > (b > m c) > ScopeH b f m a > f c Source #
Perform substitution on both bound and free variables in a ScopeH
.
bindingsH :: Foldable f => ScopeH b f m a > [b] Source #
Return a list of occurences of the variables bound by this ScopeH
.
mapBoundH :: Functor f => (b > b') > ScopeH b f m a > ScopeH b' f m a Source #
Perform a change of variables on bound variables.
mapScopeH :: (Functor f, Functor m) => (b > d) > (a > c) > ScopeH b f m a > ScopeH d f m c Source #
Perform a change of variables, reassigning both bound and free variables.
foldMapBoundH :: (Foldable f, Monoid r) => (b > r) > ScopeH b f m a > r Source #
Obtain a result by collecting information from bound variables
foldMapScopeH :: (Foldable f, Foldable m, Monoid r) => (b > r) > (a > r) > ScopeH b f m a > r Source #
Obtain a result by collecting information from both bound and free variables
traverseBoundH_ :: (Applicative g, Foldable f) => (b > g d) > ScopeH b f m a > g () Source #
traverseScopeH_ :: (Applicative g, Foldable f, Foldable m) => (b > g d) > (a > g c) > ScopeH b f m a > g () Source #
traverse_
both the variables bound by this scope and any free variables.
traverseBoundH :: (Applicative g, Traversable f) => (b > g c) > ScopeH b f m a > g (ScopeH c f m a) Source #
traverseScopeH :: (Applicative g, Traversable f, Traversable m) => (b > g d) > (a > g c) > ScopeH b f m a > g (ScopeH d f m c) Source #
traverse
both bound and free variables
bitraverseScopeH :: (Applicative g, Bitraversable f, Bitraversable m) => (k > g k') > (l > g l') > (a > g a') > ScopeH b (f k) (m l) a > g (ScopeH b (f k') (m l') a') Source #
:: Applicative g  
=> (forall x x'. (x > g x') > f x > g (f' x')) 

> (forall x x'. (x > g x') > m x > g (m' x')) 

> (a > g a')  
> ScopeH b f m a  
> g (ScopeH b f' m' a') 