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

In Types and Programming Languages by Pierce,

ML-style let-polymorphism was ﬁrst 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 diﬀerence 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.

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.

• Thanks. Which books do you use for studying programming languages?
– Tim
Nov 6 '19 at 23:00
• I have used TAPL, then there are (separate) books written by JC Reynolds, Carl Gunter. Also, check references/bibliography from TAPL. They are quite useful. Nov 7 '19 at 0:02
• Which books use "judgments" to present PLT? I think TAPL doesn't, correct?
– Tim
Nov 7 '19 at 1:46
• Martin-Löf’s type theory uses the term you can check it out here cse.chalmers.se/research/group/logic/book however it uses a little different notation than what I have used above. Nov 7 '19 at 4:19
• Thanks. I found that Harper's Practical Foundation of Programming Languages (cs.cmu.edu/~rwh/pfpl/2nded.pdf) use "judgments" to describe PLT. Not sure if that is a book comparable to TAPL and the one you linked. Is it the best book to learn for PLT? (I am a self learner, but that is probably an irrelevant fact)
– Tim
Nov 7 '19 at 17:07