Safe Haskell | Safe-Infered |
---|

Capture avoiding substitution of witnesses in expressions.

If a binder would capture a variable then it is anonymized to deBruijn form.

- class SubstituteWX c where
- substituteWithWX :: forall n. Ord n => Witness n -> Sub n -> c n -> c n

- substituteWX :: (Ord n, SubstituteWX c) => Bind n -> Witness n -> c n -> c n
- substituteWXs :: (Ord n, SubstituteWX c) => [(Bind n, Witness n)] -> c n -> c n

# Documentation

class SubstituteWX c whereSource

substituteWithWX :: forall n. Ord n => Witness n -> Sub n -> c n -> c nSource

Substitute a witness 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.

substituteWX :: (Ord n, SubstituteWX c) => Bind n -> Witness n -> c n -> c nSource

Wrapper for `substituteWithW`

that determines the set of free names in the
type being substituted, and starts with an empty binder stack.

substituteWXs :: (Ord n, SubstituteWX c) => [(Bind n, Witness n)] -> c n -> c nSource

Wrapper for `substituteW`

to substitute multiple things.