Types and Data Structures

Abstract

So far, we have assumed a fixed collection of types, type operators, constants and axioms in the logic. We next consider how to extend our theories to model new domains of discourse by defining new types with associated constants and inference rules. Either we can postulate a new type by giving a collection of axioms and inference rules that determine the properties of the type, or we can construct a new type as being isomorphic to a subset of some existing type. We describe both these methods below. We use the axiomatic approach to introduce the important type of natural numbers. As another example, we show how to define lists and disjoint sums. The latter can be seen as the category-theoretic dual to Cartesian products. The constructive approach is illustrated by showing an alternative definition of natural numbers.