Here’s the syntax for the simply-typed lambda calculus (STLC):

Here are the typing rules, written in the usual natural deduction style:

It turns out that these rules are not only enough to provide typechecking but also type inference if you feed them into Prolog, though that’s far from a coincidence. Type inference for STLC is possible, and Prolog was the result of decades of research into finding proofs (in this case a *typing* – a proof that a given term has a given type) for problems stated in this style. It’s even less of a coincidence because STLC admits principal typings – so all proofs that a term has a given type are equivalent.

## Rewriting the Rules

Suppose we deliberately ignore the existance of Prolog (but not of unification, as it’ll turn out) – how can we write the rules to make it more obvious what to do?