Data Types, Parameters, and Type Checking

Abstract

In statically typed programming languages, each variable and expression in a program is assigned a unique "type" and the program is checked to ensure that the arguments in each application are "type-compatible" with the corresponding parameters. The rules by which this "type-checking" is performed must be carefully considered for modern languages that allow the programmer to define his own data types and allow parameterized types or types as parameters. (Such languages include Alphard [Wulf78], CLU [Liskov77], Euclid [Lampson77] and Russell [Demers79].) These features increase the expressive power of the languages, but also increase the difficulty of type-checking them.In this paper, we describe a treatment of type-checking that makes it possible to do completely static checking with a general parameterization mechanism allowing parameterized types, types as parameters, and even a disciplined form of self-application. Our method defines a calculus of "signatures," where signatures are similar to the "program types" of [Reynolds78]. Each identifier and expression is given a signature, and applications are type-correct when argument and parameter signatures are equivalent under a simple set of signature transformation rules. Below we present the signature calculus of Russell; we also present a semantic justification of this calculus and specify the language constraints necessary for us to justify our purely static approach to type-checking.