Bound.ScopeH

ScopeH scope, which allows substitute f into g to get new g.

Compare following signatures:

instantiate1  :: ... => m a -> Scope  b   m a -> m a
instantiate1H :: ... => m a -> ScopeH b f m a -> f a

ScopeH variant allows to encode e.g. Hindley-Milner 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 "ill-kinded"

Another applications are bidirectional type-systems 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.

Documentation

newtype ScopeH b f m a

ScopeH b f m a is a f expression abstracted over g, with bound variables in b, and free variables in a.

Scope b f a ~ ScopeH n f f a
ScopeT b t f a ~ ScopeH b (t f) f a

Constructors

ScopeH

Fields

• unscopeH :: f (Var b (m a))

Instances

(Functor f, Functor m) => Functor (ScopeH b f m)

Defined in Bound.ScopeH

Methods

fmap :: (a -> b0) -> ScopeH b f m a -> ScopeH b f m b0

(<$) :: a -> ScopeH b f m b0 -> ScopeH b f m a

(Foldable f, Foldable m) => Foldable (ScopeH b f m)

Defined in Bound.ScopeH

Methods

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

sum :: Num a => ScopeH b f m a -> a

product :: Num a => ScopeH b f m a -> a

(Traversable f, Traversable m) => Traversable (ScopeH b f m)

Defined in Bound.ScopeH

Methods

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)

Defined in Bound.ScopeH

Methods

liftEq :: (a -> b0 -> Bool) -> ScopeH b f m a -> ScopeH b f m b0 -> Bool

(Module f m, Ord b, Ord1 f, Ord1 m) => Ord1 (ScopeH b f m)

Defined in Bound.ScopeH

Methods

liftCompare :: (a -> b0 -> Ordering) -> ScopeH b f m a -> ScopeH b f m b0 -> Ordering

(Read b, Read1 f, Read1 m) => Read1 (ScopeH b f m)

Defined in Bound.ScopeH

Methods

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)

Defined in Bound.ScopeH

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ScopeH b f m a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ScopeH b f m a] -> ShowS

(Hashable b, Module f m, Hashable1 f, Hashable1 m) => Hashable1 (ScopeH b f m)

Defined in Bound.ScopeH

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> ScopeH b f m a -> Int

(Functor f, Monad m) => Module (ScopeH b f m) m

Defined in Bound.ScopeH

Methods

(>>==) :: ScopeH b f m a -> (a -> m b0) -> ScopeH b f m b0

(Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

(==) :: ScopeH b f m a -> ScopeH b f m a -> Bool

(/=) :: ScopeH b f m a -> ScopeH b f m a -> Bool

(Module f m, Ord b, Ord1 f, Ord1 m, Ord a) => Ord (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

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

max :: ScopeH b f m a -> ScopeH b f m a -> ScopeH b f m a

min :: ScopeH b f m a -> ScopeH b f m a -> ScopeH b f m a

(Read b, Read1 f, Read1 m, Read a) => Read (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

readsPrec :: Int -> ReadS (ScopeH b f m a)

readList :: ReadS [ScopeH b f m a]

readPrec :: ReadPrec (ScopeH b f m a)

readListPrec :: ReadPrec [ScopeH b f m a]

(Show b, Show1 f, Show1 m, Show a) => Show (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

showsPrec :: Int -> ScopeH b f m a -> ShowS

show :: ScopeH b f m a -> String

showList :: [ScopeH b f m a] -> ShowS

NFData (f (Var b (m a))) => NFData (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

rnf :: ScopeH b f m a -> ()

(Hashable b, Module f m, Hashable1 f, Hashable1 m, Hashable a) => Hashable (ScopeH b f m a)

Defined in Bound.ScopeH

Methods

hashWithSalt :: Int -> ScopeH b f m a -> Int

hash :: ScopeH b f m a -> Int

Abstraction

abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a

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

Abstract over a single variable.

abstractHEither :: (Functor f, Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c

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

Abstraction, capturing named bound variables.

abstract1HName :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH (Name a ()) f m a

Abstract over a single variable

Instantiation

instantiateH :: Module f m => (b -> m a) -> ScopeH b f m a -> f a

Enter a ScopeH, instantiating all bound variables

instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a

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

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

Traditional de Bruijn

fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a)

Convert to traditional de Bruijn.

toScopeH :: (Functor f, Monad m) => f (Var b a) -> ScopeH b f m a

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

Convert to Scope.

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

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

bindingsH :: Foldable f => ScopeH b f m a -> [b]

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

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

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

foldMapBoundH :: (Foldable f, Monoid r) => (b -> r) -> ScopeH b f m a -> r

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

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

traverse_ the bound variables in a Scope.

traverseScopeH_ :: (Applicative g, Foldable f, Foldable m) => (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g ()

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)

traverse the bound variables in a Scope.

traverseScopeH :: (Applicative g, Traversable f, Traversable m) => (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g (ScopeH d f m c)

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

bitransverseScopeH

Arguments

:: Applicative g

=> (forall x x'. (x -> g x') -> f x -> g (f' x'))

traverse-like for f

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

traverse-like for m

-> (a -> g a')

-> ScopeH b f m a

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