Infernu.InferState

Documentation

type Infer a = StateT InferState (EitherT TypeError Identity) a

Inference monad. Used as a stateful context for generating fresh type variable names.

emptyInferState :: InferState

runInferWith :: InferState -> Infer a -> Either TypeError a

runSubInfer :: Infer a -> Infer (Either TypeError a)

getState :: Infer InferState

setState :: InferState -> Infer ()

runInfer :: Infer a -> Either TypeError a

fresh :: Infer TVarName

freshVarId :: Infer VarId

throwError :: Source -> String -> Infer a

failWith :: Maybe a -> Infer a -> Infer a

failWithM :: Infer (Maybe a) -> Infer a -> Infer a

mapError :: (TypeError -> TypeError) -> Infer a -> Infer a

getVarSchemeByVarId :: VarId -> Infer (Maybe TypeScheme)

getVarId :: EVarName -> TypeEnv -> Maybe VarId

getVarScheme :: Source -> EVarName -> TypeEnv -> Infer (Maybe TypeScheme)

setVarScheme :: TypeEnv -> EVarName -> TypeScheme -> VarId -> Infer TypeEnv

addVarScheme :: TypeEnv -> EVarName -> TypeScheme -> Infer TypeEnv

addPendingUnification :: (Source, Type, (ClassName, Set TypeScheme)) -> Infer ()

getPendingUnifications :: Infer (Set (Source, Type, (ClassName, Set TypeScheme)))

setPendingUnifications :: Set (Source, Type, (ClassName, Set TypeScheme)) -> Infer ()

addVarInstance :: TVarName -> TVarName -> Infer ()

getFreeTVars :: TypeEnv -> Infer (Set TVarName)

addNamedType :: TypeId -> Type -> TypeScheme -> Infer ()

areEquivalentNamedTypes :: (Type, TypeScheme) -> (Type, TypeScheme) -> Bool

Compares schemes up to alpha equivalence including named type constructors equivalence (TCons TName...).

>>> let mkNamedType tid ts = Fix $ TCons (TName (TypeId tid)) ts

>>> areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (Fix $ TBody TNumber)) (mkNamedType 1 [], schemeEmpty (Fix $ TBody TString))
False
>>> areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (mkNamedType 0 [])) (mkNamedType 1 [], schemeEmpty (mkNamedType 1 []))
True
>>> :{
    areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (Fix $ TFunc [Fix $ TBody TNumber] (mkNamedType 0 [])))
                            (mkNamedType 1 [], schemeEmpty (Fix $ TFunc [Fix $ TBody TNumber] (mkNamedType 1 [])))
:}
True

>>> :{
    areEquivalentNamedTypes (mkNamedType 0 [Fix $ TBody $ TVar 10], TScheme [10] (qualEmpty $ Fix $ TFunc [Fix $ TBody $ TVar 10] (mkNamedType 0 [Fix $ TBody $ TVar 10])))
                            (mkNamedType 1 [Fix $ TBody $ TVar 11], TScheme [11] (qualEmpty $ Fix $ TFunc [Fix $ TBody $ TVar 11] (mkNamedType 1 [Fix $ TBody $ TVar 11])))
:}
True

replaceFixQual :: (Functor f, Eq (f (Fix f))) => f (Fix f) -> f (Fix f) -> TQual (Fix f) -> TQual (Fix f)

Returns a TQual with the src type replaced everywhere with the dest type.

isRecParamOnly :: (Num t, Enum t) => TVarName -> Maybe (TypeId, t) -> Type -> Maybe [(TypeId, t)]

dropAt :: Integral a => a -> [b] -> [b]

replaceRecType :: TypeId -> TypeId -> Int -> Type -> Type

allocNamedType :: TVarName -> Type -> Infer Type

resolveSimpleMutualRecursion :: TVarName -> Type -> TypeId -> Int -> Infer Type

getNamedType :: TVarName -> Type -> Infer Type

unrollNameByScheme :: Substable a => [Type] -> [TVarName] -> a -> a

unrollName :: Source -> TypeId -> [Type] -> Infer QualType

Unrolls (expands) a TName recursive type by plugging in the holes from the given list of types. Similar to instantiation, but uses a pre-defined set of type instances instead of using fresh type variables.

applySubstInfer :: TSubst -> Infer ()

Applies a subsitution onto the state (basically on the variable -> scheme map).

>>> :{
runInfer $ do
    let t = TScheme [0] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))
    let tenv = Map.empty
    tenv' <- addVarScheme tenv "x" t
    applySubstInfer $ Map.singleton 0 (Fix $ TBody TString)
    varSchemes <$> get
:}
Right (fromList [(VarId 3,TScheme {schemeVars = [], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody TString)] Fix (TBody (TVar 1)))}})])

instantiateScheme :: Bool -> TypeScheme -> Infer QualType

Instantiate a type scheme by giving fresh names to all quantified type variables.

For example:

>>> runInferWith (emptyInferState { nameSource = NameSource 2 }) . instantiate $ TScheme [0] (TQual { qualPred = [], qualType = Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1)) })
Right (TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 3))] Fix (TBody (TVar 1)))})

In the above example, type variable 0 has been replaced with a fresh one (3), while the unqualified free type variable 1 has been left as-is.

>>> :{
runInfer $ do
    let t = TScheme [0] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))
    let tenv = Map.empty
    tenv' <- addVarScheme tenv "x" t
    instantiateVar emptySource "x" tenv'
:}
Right (TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 4))] Fix (TBody (TVar 1)))})

instantiate :: TypeScheme -> Infer QualType

instantiateVar :: Source -> EVarName -> TypeEnv -> Infer QualType

unsafeGeneralize :: TypeEnv -> QualType -> Infer TypeScheme

Generalizes a type to a type scheme, i.e. wraps it in a "forall" that quantifies over all type variables that are free in the given type, but are not free in the type environment.

Example:

>>> runInfer $ generalize (ELit "bla" LitUndefined) Map.empty $ qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))
Right (TScheme {schemeVars = [0,1], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 1)))}})

>>> :{
runInfer $ do
    let t = TScheme [1] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))
    tenv <- addVarScheme Map.empty "x" t
    generalize (ELit "bla" LitUndefined) tenv (qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 2)))
:}
Right (TScheme {schemeVars = [2], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 2)))}})

In this example the steps were:

1. Environment: { x :: forall 0. 0 -> 1 }
2. generalize (1 -> 2)
3. result: forall 2. 1 -> 2

>>> let expr = ELit "foo" LitUndefined

>>> runInfer $ generalize expr Map.empty (qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 0)))
Right (TScheme {schemeVars = [0], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 0)))}})

>>> runInfer $ generalize expr Map.empty (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody (TVar 1))] (Fix $ TBody (TVar 0)))
Right (TScheme {schemeVars = [0,1], schemeType = TQual {qualPred = [TPredIsIn {predClass = ClassName "Bla", predType = Fix (TBody (TVar 1))}], qualType = Fix (TBody (TVar 0))}})

TODO add tests for monotypes

isExpansive :: Exp a -> Bool

generalize :: Exp a -> TypeEnv -> QualType -> Infer TypeScheme

minifyVarsFunc :: VarNames a => a -> TVarName -> TVarName

minifyVars :: VarNames a => a -> a

getVarInstances :: Infer (Gr QualType ())

getMainSubst :: Infer TSubst

applyMainSubst :: Substable b => b -> Infer b

substVar :: TSubst -> TVarName -> TVarName

lookupClass :: ClassName -> Infer (Maybe (Class Type))