TypiCal

The type checking algorithm for simple type theory solves the problem whether an untyped lambda-term M has a type according to the rules of simple type theory. As usual, we distinguish between a type checking problem: M : A? (does the term M have type A?) and a type synthesis problem: M : ? (compute a type A for the term M). It is a classic result that for simple type theory, these problems are equivalent and decidable. The solution amounts to computing the principal type of M and then to check whether the given type A is an instance of it.

There is a (seemingly) different way to decide typing, due to Newman, already in 1943, and recently reviewed by Hindley. Newman's algorithm only decides whether a term is typable and does not compute a principal type. This is quite remarkable. We describe Newman's algorithm in a modern fashion as a manipulation of the tree that represents the lambda-term. We analyze Newman's algorithm and we show that it (implicitly) does compute a principal type, and that the way it computes it is actually quite close to Wand's version of the typing algorithm for simple type theory.