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

Bound.ScopeH

Description

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.

Synopsis

Documentation

newtype ScopeH b f m a Source #

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 FieldsunscopeH :: f (Var b (m a))
Instances

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.

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

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 #

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

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

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