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.

REFERENCES

• 1: Alan Demers , James Donahue , Glenn Skinner, Data types as values: polymorphism, type-checking, encapsulation, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-30, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512764]
• 2: {Demers79} Demers, A. and J. Donahue. Revised Report on Russell. Report TR79-389, Computer Science Department, Cornell University, September 1979.
• 3: Alan Demers , James Donahue, "Type-completeness" as a language principle, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-244, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567469]
• 4: {Demers80b} Demers, A. and J. Donahue. A Formal Semantics for Russell. (in preparation)
• 5: {Goguen76} Goguen, J. A., J. W. Thatcher and E. G. Wagner. An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. Report RC6487, IBM Thomas J. Watson Research Center, Yorktown Heights, N. Y., 1976.
• 6: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 7: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 8: James H. Morris, Jr., Types are not sets, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.120-124, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512938]
• 9: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 10: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 11: {Wulf78} Wulf, W. A. (ed.) An Informal Definition of Alphard. CMU-CS-78-105, Department of Computer Science, Carnegie-Mellon University, 1978.