Safe Haskell  Safe 

Language  Haskell98 
Capture avoiding substitution of types in types.
 substituteT :: (SubstituteT c, Ord n) => Bind n > Type n > c n > c n
 substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] > c n > c n
 substituteBoundT :: (SubstituteT c, Ord n) => Bound n > Type n > c n > c n
 class SubstituteT c where
 data BindStack n = BindStack {
 stackBinds :: ![Bind n]
 stackAll :: ![Bind n]
 stackAnons :: !Int
 stackNamed :: !Int
 pushBind :: Ord n => Set n > BindStack n > Bind n > (BindStack n, Bind n)
 pushBinds :: Ord n => Set n > BindStack n > [Bind n] > (BindStack n, [Bind n])
 substBound :: Ord n => BindStack n > Bound n > Bound n > Either (Bound n) Int
Documentation
substituteT :: (SubstituteT c, Ord n) => Bind n > Type n > c n > c n Source #
substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] > c n > c n Source #
Wrapper for substituteT
to substitute multiple things.
substituteBoundT :: (SubstituteT c, Ord n) => Bound n > Type n > c n > c n Source #
class SubstituteT c where Source #
substituteWithT :: forall n. Ord n => Bound n > Type n > Set n > BindStack n > c n > c n Source #
Substitute a type into some thing. In the target, if we find a named binder that would capture a free variable in the type to substitute, then we rewrite that binder to anonymous form, avoiding the capture.
Stack of anonymous binders that we've entered under during substitution.
BindStack  

:: Ord n  
=> Set n  Names that need to be rewritten. 
> BindStack n  Current bind stack. 
> Bind n  Bind to push. 
> (BindStack n, Bind n)  New stack and possibly anonymised bind. 
Push a bind onto a bind stack, anonymizing it if need be to avoid variable capture.