17. Type Theory
Type theory studies formal systems in which expressions are classified by types, and it provides a foundation where logical propositions, mathematical objects, and computational programs can be treated in one unified language. The chapter begins with simple type theory, where each term has a fixed type and functions are assigned types describing the kinds of inputs they accept and the kinds of outputs they produce. Dependent types are then introduced,...