Safe Haskell | None |
---|

- doSubst :: Bool -> Bool -> IdMap (Maybe E) -> E -> E
- doSubst' :: Bool -> Bool -> IdMap E -> (Id -> Bool) -> E -> E
- eAp :: E -> E -> E
- litSMapM :: Monad m => (a -> m t) -> Lit a a -> m (Lit t t)
- subst :: TVr -> E -> E -> E
- subst' :: TVr -> E -> E -> E
- substMap :: IdMap E -> E -> E
- substMap' :: IdMap E -> E -> E
- substMap'' :: IdMap (Maybe E) -> E -> E
- typeSubst :: IdMap (Maybe E) -> IdMap E -> E -> E
- typeSubst' :: IdMap E -> IdMap E -> E -> E

# Documentation

Basic substitution routine

subst' :: TVr -> E -> E -> ESource

Identitcal to `subst`

except that it substitutes inside the local types
for variables in expressions. This should not be used because it breaks the
sharing of types between a binding site of a variable and its uses and can
lead to inconsistant terms. However, it is sometimes useful to create
transient terms for typechecking.

:: IdMap (Maybe E) | substitution to carry out at term level as well as a list of in-scope variables |

-> IdMap E | substitution to carry out at type level |

-> E -> E | the substitution function |

substitution routine that can substitute different values at the term and type level. this is useful to enforce the invarient that let-bound variables must not occur at the type level, yet non-atomic values (even typelike ones) cannot appear in argument positions at the term level.