What are the difference and relation between type checking and type reconstruction?

Question

In Types and Programming Languages by Pierce,

ML-style let-polymorphism was first described by Milner (1978). A num- ber of type reconstruction algorithms have been proposed, notably the clas- sic Algorithm W (Damas and Milner) of Damas and Milner (1982; also see Lee and Yi, 1998). The main difference between Algorithm W and the pre- sentation in this chapter is that the former is specialized for “pure type reconstruction”—assigning principal types to completely untyped lambda- terms—while we have mixed type checking and type reconstruction, permit- ting terms to include explicit type annotations that may, but need not, contain variables. This makes our technical presentation a bit more involved (espe- cially the proof of completeness, Theorem 22.3.7, where we must be careful to keep the programmer’s type variables separate from the ones introduced by the constraint generation rules), but it meshes better with the style of the other chapters.

What are the difference and relation between type checking and type reconstruction?

Does type checking apply only to terms with explicit type annotations which don't contain type variables?

Does type reconstruction apply only to terms either without explicit type annotations, or with explicit type annotations containing type variables?

Thanks.

Answer 1

What are the difference and relation between type checking and type reconstruction?

Type reconstruction is a class of problem that involves coming up with a type for a term. For example given a term $\lambda x. x$ can you find the type for this term. Or in general answering the question:

Does a $T$ exist such that the judgement $\Gamma \vdash M : T$ is derivable, where $M$ is the term and $\Gamma$ is the type environment.

Type checking on the other hand is a process where the question is:

Given a $T$ and an $M$ can $\Gamma \vdash M : T$ be a valid judgement.

Does type checking apply only to terms with explicit type annotations which don't contain type variables?

No. You can have a type checking problem that asks whether $\lambda x. x$ has a type $\tau \to \tau$ where $\tau$ is a type variable.

Does type reconstruction apply only to terms either without explicit type annotations, or with explicit type annotations containing type variables?

As type reconstruction problem is about computing the correct type for a term, if you have an explicit type annotation for a term, you would classify it as a type checking problem.