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

Safe HaskellNone
LanguageHaskell2010

Bound.ScopeH

Contents

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 

Fields

Instances
(Functor f, Functor m) => Functor (ScopeH b f m) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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 Source # 
Instance details

Defined in Bound.ScopeH

Methods

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

(Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq (ScopeH b f m a) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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

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

Convert to 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 #

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 #

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