The type-checking problem

Type-checking refers to the following problem:

Given a context \Gamma, a term M, and a type A, is it the case that \Gamma \vdash M : A?

Decidability

Whereas for simple systems type-checking is decidable, this is not so in more complicated ones: see for example Martin-Löf extensional type theory.

Complexity

For simply-typed systems there is a simple rule of thumb: if your term has enough annotations, type-checking takes O(n) time in the length of the term n: one looks at M, and tries to match its structure to the given typing rules. Of course this might not be true if the system is very complicated.

For example, what happens with subtyping and recursive types? Please expand.

However, this is not true for dependently-typed systems. Checking the type of a dependently-typed term implicitly involves deciding equality (of both types and terms). Thus, dependent type checking depends on normalization, and so its complexity can become extremely high.

If a term is not fully annotated with types, we are no longer discussing type checking, but type inference.

References

• Some pointers are given in Neel Krishnaswami's answer to this stackexchange question.

Please expand.