Type-checking systems with particular applications to functional languages

Abstract

J.Morris in his thesis discovered that conventional type-checking systems inhibit users of typed languages and he left two problems for future solution-parametric polymorphism and circular types. Any typed language is related to a type-checking system T. by a function. Consequently type-checking systems may be studied independently of particular languages. Therefore a logic to illustrate how such systems are intended to work must preserve language and machine independencies, and it must not be inhibited by Morris' two problems. We have therefore chosen the A-K Calculus. Fundamental concepts of types and type-checking are discussed and these include theorems of functionality, a set-theoretical approach to types, and intersection-types. After preliminary examination of previous type-checking systems, we propose two systems of our own.The first one we have implemented is System-F. In attempting to generalize it beyond the work of conventional type checkers we discovered that it is necessary to abandon the distinction between so-called statically- and dynamically-typed systems.In this way we alight on our most fundamental problem. This is how to design type-checking systems that permit declaration of arbitrary functions and functionals whose type declarations are incomplete or missing. We solve this by introducing a class of type expressions we call type abstractions. We have also introduced a way to describe type-checking processes by certain sets of equations, and shown how to solve them. These thoughts are implemented in our second system, the System-Y. Later, we explored further the nature of circular types in the light of lattice theory. Both our systems are adequate to handle Morris' problems.