| Copyright | disco team and contributors |
|---|---|
| License | BSD-3-Clause |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Disco.Typecheck.Unify
Description
Unification.
Synopsis
- unify :: TyDefCtx -> [(Type, Type)] -> Maybe S
- weakUnify :: TyDefCtx -> [(Type, Type)] -> Maybe S
- unify' :: (BaseTy -> BaseTy -> Bool) -> TyDefCtx -> [(Type, Type)] -> Maybe S
- equate :: TyDefCtx -> [Type] -> Maybe S
- occurs :: Name Type -> Type -> Bool
- unifyAtoms :: TyDefCtx -> [Atom] -> Maybe (Substitution Atom)
- unifyUAtoms :: TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom)
Documentation
unify :: TyDefCtx -> [(Type, Type)] -> Maybe S Source #
Given a list of equations between types, return a substitution which makes all the equations satisfied (or fail if it is not possible).
This is not the most efficient way to implement unification but it is simple.
weakUnify :: TyDefCtx -> [(Type, Type)] -> Maybe S Source #
Given a list of equations between types, return a substitution which makes all the equations equal *up to* identifying all base types. So, for example, Int = Nat weakly unifies but Int = (Int -> Int) does not. This is used to check whether subtyping constraints are structurally sound before doing constraint simplification/solving, to ensure termination.
unify' :: (BaseTy -> BaseTy -> Bool) -> TyDefCtx -> [(Type, Type)] -> Maybe S Source #
Given a list of equations between types, return a substitution which makes all the equations satisfied (or fail if it is not possible), up to the given comparison on base types.
unifyAtoms :: TyDefCtx -> [Atom] -> Maybe (Substitution Atom) Source #
unifyUAtoms :: TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom) Source #