This paper deals with the implementation of a type checker for the simply typed lambda calculus in the Standard ML language. A type system is generally defined via a set of predicates that are defined inductively following the structure of the language through a set of inference rules. Normally, some work needs to be done to show that the algorithm for type checking is correct. In this paper, the authors take a different route and define a reduction relation for the type system.

The authors prove that the proposed reduction semantics is sound and complete with respect to the semantics of the lambda calculus with types. The reduction relation for the type system is effectively a type checker, which excels over traditional algorithms because it can be naturally implemented in a functional language. The authors prove this concept by providing the code of the reduction semantics of the type system.

The authors seek to determine whether there exists a natural correspondence between the reduction relation for the type system and the inference system that avoids the need for soundness and completeness theorems. The answer seems to lie in the implementation presented in detail in the paper, but it is left unclear how this program answers the question without at least a proof that the presented code is correct.

In brief, the paper is concerned with an actual, yet elegant and intelligent implementation of type checking. While the example language of the paper was the simply typed lambda calculus, the techniques can be applied to other functional languages.

This is a interesting read for any person working in functional languages with sophisticated type systems such as F# or Scala.