Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Implements naive substitution functions for replacing type and term variables.
Synopsis
- substVarA ∷ Applicative f ⇒ (name → f (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → f (Term tyname name uni fun ann)
- substTyVarA ∷ Applicative f ⇒ (tyname → f (Maybe (Type tyname uni ann))) → Type tyname uni ann → f (Type tyname uni ann)
- typeSubstTyNames ∷ ∀ tyname (uni ∷ Type → Type) ann. (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann
- termSubstNames ∷ (name → Maybe (Term tyname name uni fun a)) → Term tyname name uni fun a → Term tyname name uni fun a
- termSubstNamesM ∷ Monad m ⇒ (name → m (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann)
- termSubstTyNames ∷ (tyname → Maybe (Type tyname uni a)) → Term tyname name uni fun a → Term tyname name uni fun a
- termSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann)
- bindingSubstNames ∷ (name → Maybe (Term tyname name uni fun a)) → Binding tyname name uni fun a → Binding tyname name uni fun a
- bindingSubstTyNames ∷ (tyname → Maybe (Type tyname uni a)) → Binding tyname name uni fun a → Binding tyname name uni fun a
Documentation
substVarA ∷ Applicative f ⇒ (name → f (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → f (Term tyname name uni fun ann) Source #
Applicatively replace a variable using the given function.
substTyVarA ∷ Applicative f ⇒ (tyname → f (Maybe (Type tyname uni ann))) → Type tyname uni ann → f (Type tyname uni ann) Source #
Applicatively replace a type variable using the given function.
typeSubstTyNames ∷ ∀ tyname (uni ∷ Type → Type) ann. (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann Source #
Naively substitute type names (i.e. do not substitute binders).
termSubstNames ∷ (name → Maybe (Term tyname name uni fun a)) → Term tyname name uni fun a → Term tyname name uni fun a Source #
Naively substitute names using the given functions (i.e. do not substitute binders).
termSubstNamesM ∷ Monad m ⇒ (name → m (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann) Source #
Naively monadically substitute names using the given function (i.e. do not substitute binders).
termSubstTyNames ∷ (tyname → Maybe (Type tyname uni a)) → Term tyname name uni fun a → Term tyname name uni fun a Source #
Naively substitute type names using the given functions (i.e. do not substitute binders).
termSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann) Source #
Naively monadically substitute type names using the given function (i.e. do not substitute binders).