Type-checking systems with particular applications to functional languages

Yeung, Hock Kuen Francis


Yeung, Hock Kuen Francis (1976) Type-checking systems with particular applications to functional languages.

Our Full Text Deposits

Full text access: Open

10097426.pdf - 8.97 MB


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.

Information about this Version

This is a Accepted version
This version's date is: 1976
This item is not peer reviewed

Link to this Version


Item TypeThesis (Doctoral)
TitleType-checking systems with particular applications to functional languages
AuthorsYeung, Hock Kuen Francis
Uncontrolled KeywordsComputer Science; Applied Sciences; Applications; Checking; Functional; Languages; Particular; Systems; Type; Type Checking; Type Checking



Deposited by () on 01-Feb-2017 in Royal Holloway Research Online.Last modified on 01-Feb-2017


Digitised in partnership with ProQuest, 2015-2016. Institution: University of London, Royal Holloway College (United Kingdom).