Data-types as Objects Revisited: Insights and Proofs

This thesis is concerned with an approach to giving the semantics of data-types in simple functional programming languages. The material is a thoroughly rewritten version of [SW77] completed with proofs and insights, which were largely absent in the original paper. The approach of [SW77] has been influential in several subsequent works and has been the basis for the development of the so-called ideal-model for recursive polymorphic types. The main idea of the aforementioned paper is to treat data-types as objects of the programming language; to do this, the authors developed a formal system in which substantial computation with data-types can be performed, including the recursive definition of data-types or their application to functions: in view of the Curry-Howard Isomorphism, this is to say that one can actually use computation with data-types to prove properties of programs. The resulting model allows the existence of subtypes and supertypes, as well as of logically qualified types and a limited form of dependent type families, notions which are much harder to define in traditional type systems. In the thesis we explore the formal definitions of the notions involved and present (with complete proofs) their basic properties, both at an abstract level, as well as at that of applications in type-checking real-world programs. To supplement the reader’s understanding of the latter, scattered among the collection of theorems and the described techniques are a few illuminating examples, showing the flexibility and power of the theory under consideration.