Type.Check.HM.Infer

Defines type-inference algorithm.

For type inference we have to define instance of the Lang class:

data NoPrim
  deriving (Show)

data TestLang

instance Lang TestLang where
  type Src  TestLang = ()              -- ^ define type for source code locations
  type Var  TestLang = Text            -- ^ define type for variables
  type Prim TestLang = NoPrim          -- ^ define type for primitive operators
  getPrimType _ _ = error "No primops"   -- ^ reports types for primitives

Also we define context for type inference that holds types for all known variables Often it defines types for all global variables or functions that are external.

context = Context $ Map.fromList [...]

Then we can use inference to derive type for given term with inferType or we can derive types for all sub-expressions of given term with inferTerm. See module in the test TM.Infer for examples of the usage.

termI,termK :: Term NoPrim () Text

-- I combinator
termI = lamE () "x" $ varE () "x"
-- K combinator
termK = lamE () "x" $ lamE () "y" $ varE () "x"

-- Let's infer types
typeI = inferType mempty termI
typeK = inferType mempty termK

There are functions to check that two types unify (unifyTypes) or that one type is subtype of another one (subtypeOf).

Context

data Context loc v

Context holds map of proven signatures for free variables in the expression.

Constructors

Context

Fields

• context'binds :: Map v (Signature loc v)

  known binds

• context'constructors :: Map v (Signature loc v)

  known constructors for user-defined types

Instances

CanApply Context

Defined in Type.Check.HM.Infer

Methods

apply :: Ord v => Subst loc v -> Context loc v -> Context loc v

(Eq v, Eq loc) => Eq (Context loc v)

Defined in Type.Check.HM.Infer

Methods

(==) :: Context loc v -> Context loc v -> Bool

(/=) :: Context loc v -> Context loc v -> Bool

(Show v, Show loc) => Show (Context loc v)

Defined in Type.Check.HM.Infer

Methods

showsPrec :: Int -> Context loc v -> ShowS

show :: Context loc v -> String

showList :: [Context loc v] -> ShowS

Ord v => Semigroup (Context loc v)

Defined in Type.Check.HM.Infer

Methods

(<>) :: Context loc v -> Context loc v -> Context loc v

sconcat :: NonEmpty (Context loc v) -> Context loc v

stimes :: Integral b => b -> Context loc v -> Context loc v

Ord v => Monoid (Context loc v)

Defined in Type.Check.HM.Infer

Methods

mempty :: Context loc v

mappend :: Context loc v -> Context loc v -> Context loc v

mconcat :: [Context loc v] -> Context loc v

insertCtx :: Ord v => v -> Signature loc v -> Context loc v -> Context loc v

Insert signature into context

lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)

Lookup signature by name in the context of inferred terms.

insertConstructorCtx :: Ord v => v -> Signature loc v -> Context loc v -> Context loc v

Insert signature into context

lookupConstructorCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)

Lookup signature by name in the context of inferred terms.

type ContextOf q = Context (Src q) (Var q)

Type synonym for context.

Inference

inferType :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TypeOf q)

Type-inference function. We provide a context of already proven type-signatures and term to infer the type.

inferTerm :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)

Infers types for all subexpressions of the given term. We provide a context of already proven type-signatures and term to infer the type.

inferTypeList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]

Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies. It returns only top-level types for all terms.

inferTermList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]

Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.

subtypeOf :: (IsVar v, Show loc, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)

Checks if first argument one type is subtype of the second one.

unifyTypes :: (Show loc, IsVar v, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)

Checks weather two types unify. If they do it returns substitution that unifies them.

Utils

closeSignature :: Ord var => [Type loc var] -> Signature loc var -> Type loc var

Substitutes all type arguments with given types.

printInfer :: PrettyLang q => Either [ErrorOf q] (TypeOf q) -> IO ()

Pretty printer for result of type-inference