Robert L. Constable
Cornell University
This article approaches the subject of modern type theory from the familiar territory of logic. It starts with an account of pure typed predicate logic which is similar to the ordinary predicate calculus except that judgments of whether an expression is meaningful are explicit, and proofs are treated as mathematical objects (as opposed to metamathematical ones).
The pure typed predicate logic is extended with concrete types and type constructors creating an type theory. This theory is related back to Principia Mathematica and forward to modern proof development systems like NuprlNuprl (``new pearl''). The semantic basis of this theory is taken to be Martin-Löf's ``inductive semantics'' as opposed to Tarski's truth-value semantics.
The last section looks at the type systems of programming languages from the
viewpoint of Martin-Löf semantics. Programming types are seen as ``partial
types'', and their theories are considered to be partial axiomatizations of
mathematical types. The point is illustrated mainly for recursive types.
The notion that
is also explored.