Abstract types have existential type

ABSTRACT

Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite “value” we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.

REFERENCES

• 1: ARBIB, M. A., AND MANES, E.G. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press, Orlando, Fla., 1975.
• 2: BARENDREGT, H. P. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, The Netherlands, 1984 (revised edition).
• 3: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 4: Kim B. Bruce , Albert R. Meyer , John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, v.85 n.1, p.76-134, March 1990 [doi>10.1016/0890-5401(90)90044-I]
• 5: BURSTALL, R. M., AND GOGUEN, J. Putting theories together to make specifications. In Fifth International Joint Conference on Artificial Intelligence, 1977, pp. 1045-1958.
• 6: BURSTALL, a. M., AND GOGUEN, J. An informal introduction to specification using CLEAR. In The Correctness Problem in Computer Science, Boyer and Moore, Eds. Academic Press, Orlando, Fla., 1981, pp. 185-213.
• 7: 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
• 8: CONSTABLE, R.L. Programs and types. In 21st IEEE Symposium on Foundations of Computer Science (Syracuse, N.Y., Oct. 1980). IEEE, New York, 1980, pp. 118-128.
• 9: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 10: COQUAND, T. An analysis of Girard's paradox. In Proceedings of the IEEE Symposium on Logic in Computer Science (June 1986). IEEE, New York, 1986, pp. 227-236.
• 11: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 12: CURRY, H. B., AND FEYS, R. Combinatory Logic L North-Holland, Amsterdam, 1958.
• 13: DEBRUIJN, N. G. A survey of the project Automath. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 579-607.
• 14: Alan J. Demers , James E. Donahue, Data types, parameters and type checking, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-23, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567448]
• 15: 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]
• 16: 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]
• 17: U.S. DEPARTMENT OF DEFENSE Reference Manual for the Ada Programming Language. GPO 008-000-00354-8, 1980.
• 18: DONAHUE, J. On the semantics of data type. SIAM J. Comput. 8 (1979), 546-560.
• 19: FITTING, M. C. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 1969.
• 20: Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
• 21: GIRARD, J.-Y. Une extension de l'interpretation de GSdel ~ l'analyse, et son application l'~limination des coupures dans l'analyse et la th~orie des types. In 2nd Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, Amsterdam, 1971, pp. 63-92.
• 22: GIRARD, J.~Y. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Univ. Paris VII, Paris, 1972.
• 23: GORDON, M. J., MILNER, R., AND WADSWORTH, C.P. Edinburgh Lecture Notes in Computer Science 78, Springer-Verlag, New York, 1979.
• 24: GRi4TZER G. Universal Algebra. Van Nostrand, New York, 1968.
• 25: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 26: Christopher T. Haynes, A theory of data type representation independence., Proc. of the international symposium on Semantics of data types, p.157-175, July 1984, Sophia-Antipolis, France
• 27: HERRL1CH, H., AND STRECKER, G.E. Category Theory. Allyn and Bacon, Newton, Mass., 1973.
• 28: 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
• 29: James G. Hook , Douglas J. Howe, Impredicative Strong Existential Equivalent to Type:Type, Cornell University, Ithaca, NY, 1986
• 30: HOWARD, W. The formulas-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 479-490.
• 31: HOWE, D.J. The computational behavior of Girard's paradox. In IEEE Symposium on Logic in Computer Science (June 1987). IEEE, New York, 1987, pp. 205-214.
• 32: D. Kapur, TOWARDS A THEORY FOR ABSTRACT DATA TYPES, Massachusetts Institute of Technology, Cambridge, MA, 1980
• 33: KLEENE, S.C. Realizability: A retrospective survey. In Cambridge Summer School in Mathematical Logic. Lecture Notes in Mathematics 337, Springer-Verlag, New York, 1971, pp. 95-112.
• 34: KRIPKE, S.A. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions. Proceedings of the 8th Logic Colloquium (Oxford, 1963). North-Holland, Amsterdam, 1965, pp. 92-130.
• 35: LAMBEK, J. From lambda calculus to Cartesian closed categories. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 375-402.
• 36: P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
• 37: 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]
• 38: L)/,UCHL1, H. Intuitionistic propositional calculus and definably non-empty terms. J. Symbolic Logic 30 (1965), 263.
• 39: L~.UCHLI, H. An abstract notion of realizability for which intuitionistic predicate calculus is complete. In Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. (1968). North-Holland, Amsterdam, 1970, pp. 227-234.
• 40: Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567077]
• 41: 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]
• 42: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 43: MAC LANE, S. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer-Verlag, New York, 1971.
• 44: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 45: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 46: MARTIN-LOF, P. Constructive mathematics and computer programming. Paper presented at The 6th International Congress for Logic, Methodology and Philosophy of Science. Preprint, Univ. of Stockholm, Dept. of Mathematics, Stockholm, 1979.
• 47: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 48: Nancy McCracken, The typechecking of programs with implicit type structure., Proc. of the international symposium on Semantics of data types, p.301-315, July 1984, Sophia-Antipolis, France
• 49: 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]
• 50: MILNER, R. The standard ML core language. Polymorphism 2, 2 (1985), 28 pages. An earlier version appeared in Proceedings of 1984 ACM Symposium on Lisp and Functional Programming.
• 51: MITCHELL, J. C. Semantic models for second-order Lambda calculus. In Proceedings of the 25th IEEE Symposium on Foundations of Computer Science (1984). IEEE, New York, 1984, pp. 289-299.
• 52: 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]
• 53: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 54: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• 55: John C. Mitchell , Albert R. Meyer, Second-Order Logical Relations (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.225-236, June 17-19, 1985
• 56: 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]
• 57: MITCHELL, J. G., MAYBERRY, W., AND SWEET, R. Mesa language manual. Tech. Rep. CSL- 79-3, Xerox PARC, Palo Alto, Calif., 1979.
• 58: 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]
• 59: Michael O'Donnell, A programming language theorem which is independent of Peano Arithmetic, Proceedings of the eleventh annual ACM symposium on Theory of computing, p.176-188, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804411]
• 60: PRAWlTZ, D. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.
• 61: PRAWITZ, D. Ideas and results in proof theory. In 2nd Scandinavian Logic Symposium. North- Holland, Amsterdam, 1971, pp. 235-308.
• 62: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 63: REYNOLDS, J.C. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, Eds. IFIP, North-Holland, Amsterdam, 1981, pp. 345-372.
• 64: REYNOLDS, J.C. Types, abstraction, and parametric polymorphism. In IFIP Congress (Paris, Sept. 1983).
• 65: REYNOLDS, J.C. Polymorphism is not set-theoretic. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 145-156.
• 66: SHAW, M. (Ed.) ALPHARD: Form and Content. Springer-Verlag, New York, 1981.
• 67: STATMAN, R. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9 (1979), 67-72.
• 68: STATMAN, R. Number theoretic functions computable by polymorphic programs. In 22nd IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1981, pp. 279-282.
• 69: STENLUND, S. Combinators, ),-terms and Proof Theory. Reidel, Dordrecht, Holland, 1972.
• 70: TROELSTRA, A.S. Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer-Verlag, New York, 1973.
• 71: WULF, W. W., LONDON, R., AND SHAW, M. An introduction to the construction and verification of Alphard programs. IEEE Trans. Softw. Eng. SE-2 (1976), 253-264.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Theory