Using dependent types to express modular structure

ABSTRACT

Writing any large program poses difficult problems of organization. In many modern programming languages these problems are addressed by special linguistic constructs, variously known as modules, packages, or clusters, which provide for partitioning programs into manageable components and for securely combining these components to form complete programs. Some general purpose components are able to take on a life of their own, being separately compiled and stored in libraries of generic, reusable program units. Usually modularity constructs also support some form of information hiding, such as "abstract data types." "Programming in the large" is concerned with using such constructs to impose structure on large programs, in contrast to "programming in the small", which deals with the detailed implementation of algorithms in terms of data structures and control constructs. Our goal here is to examine some of the proposed linguistic notions with respect to how they meet the pragmatic requirements of programming in the large.

REFERENCES

• 1: Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985 [doi>10.1145/2363.2528]
• 2: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• 3: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 4: {Bur84} R. M. Burstall, <i>Programming with modules as typed functional programming,</i> Int'l Conf. on 5th Generation Computing Systems, Tokyo, Nov. 1984.
• 5: {Car85} L. Cardelli, <i>The impredicative typed &lambda;-calculus,</i> unpublished manuscript, 1985.
• 6: {CF58} H. B. Curry and R. Feys, <b>Combinatory Logic I,</b> North-Holland, 1958.
• 7: {CH85} T. Coquand and G. Huet, <i>A calculus of constructions,</i> Information and Control, to appear.
• 8: L. Cardelli , D. MacQueen, Persistence and type abstraction, Data types and persistence, Springer-Verlag, London, 1988
• 9: {CW85} L. Cardelli and P. Wegner. <i>On understanding types, data abstraction, and polymorphism.</i> Technical Report No. CS-85-14, Brown University, August 1985.
• 10: Robert L. Constable , Daniel R. Zlatin, The Type Theory of PL/CV3, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.94-117, Jan. 1984 [doi>10.1145/357233.357238]
• 11: {dcB80} N. G. de Bruijn. <i>A survey of project AUTOMATH,</i> in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Academic Press, 1980, pp. 579--607.
• 12: James Donahue , Alan Demers, Data types are values, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.426-445, July 1985 [doi>10.1145/3916.3987]
• 13: {Gir71} J. Y. Girard, <i>Une extension de l'interpretation de G&ouml;del &agrave; l'analyse, et son application &agrave; l'&eacute;limination des coupures dans l'analyse et la th&eacute;orie des types,</i> in Second Scandinavian Logic Symposium, J. E. Fenstad, Ed., North-Holland, 1971, pp. 63--92.
• 14: James G. Hook, Understanding Russell–a first attempt, Proc. of the international symposium on Semantics of data types, p.69-85, July 1984, Sophia-Antipolis, France
• 15: {How80} W. Howard, <i>The formulas-as-types notion of construction,</i> in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Academic Press, 1980, pp. 476--490. (written 1969)
• 16: {Mac85} D. B. MacQueen, <i>Modules for Standard ML (Revised),</i> Polymorphism Newsletter, ll, 2, Oct 1985.
• 17: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 18: {M-L71} P. Martin-L&ouml;f, <i>A theory of types,</i> unpublished manuscript, October 1971.
• 19: {M-L74} P. Martin-L&ouml;f, <i>An intuitionistic theory of types: predicative part,</i> Logic Colloquium 73, H. Rose and J. Shepherdson, Eds., North-Holland, 1974, pp. 73--118.
• 20: {M-L82} P. Martin-L&ouml;f, <i>Constructive mathematics and computer programming,</i> in <b>Logic, Methodology and Philosophy of Science, VI.</b> North-Holland, Amsterdam, 1982, pp. 153--175.
• 21: Albert R. Meyer , Mark B. Reinhold, "Type" is not a type, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.287-295, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512671]
• 22: {MIL78} R. Milner, <i>A theory of type polymorphism in programming,</i> JCSS, 17, 3, Dec 1978, pp. 348--375.
• 23: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 24: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential types, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.37-51, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318606]
• 25: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 26: {Sco70} D. Scott, <i>Constructive Validity,</i> in Symposium on Automatic Demonstration, Lecture Notes in Math., Vol 125, Springer-Verlag, 1970, pp. 237--275.