Safe Haskell | None |
---|---|
Language | Haskell98 |
Functions relating to skolemization used during typechecking
- newSkolemConstant :: UnifyT Type Check Int
- introduceSkolemScope :: Type -> UnifyT Type Check Type
- newSkolemScope :: UnifyT Type Check SkolemScope
- skolemize :: String -> Int -> SkolemScope -> Type -> Type
- skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr
- skolemEscapeCheck :: Expr -> Check ()
Documentation
introduceSkolemScope :: Type -> UnifyT Type Check Type Source
Introduce skolem scope at every occurence of a ForAll
newSkolemScope :: UnifyT Type Check SkolemScope Source
Generate a new skolem scope
skolemize :: String -> Int -> SkolemScope -> Type -> Type Source
Skolemize a type variable by replacing its instances with fresh skolem constants
skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr Source
This function has one purpose - to skolemize type variables appearing in a SuperClassDictionary placeholder. These type variables are somewhat unique since they are the only example of scoped type variables.
skolemEscapeCheck :: Expr -> Check () Source
Ensure skolem variables do not escape their scope