John C. Mitchell
Gordon D. Plotkin
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.
- 1 ARBIB, M. A., AND MANES, E.G. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press, Orlando, Fla., 1975.Google Scholar
- 2 BARENDREGT, H. P. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, The Netherlands, 1984 (revised edition).Google Scholar
- 3 BRUCE, K. B., AND MEYER, A. A completeness theorem for second-order polymorphic lambda calculus. In Proceedings of the International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 131-144. Google Scholar
- 4 BRUCE, K. B., MEYER, A. R., AND MITCHELL, J. C. The semantics of second-order lambda calculus. In Information and Computation (to be published), Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 7 BURSTALL, R., AND LAMPSON, B. A kernel language for abstract data types and modules. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 1-50. Google Scholar
- 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.Google Scholar
- 9 CONSTABLE, R. L., ET AL. Implementing Mathematics With The Nuprl Proof Development System. Graduate Texts in Mathematics, vol. 37, Prentice-Hall, Englewood Cliffs, N.J., 1986. Google Scholar
- 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.Google Scholar
- 11 COQUAND, T., AND HUET, G. The calculus of constructions. Inf. Comput. 76, 2/3 (Feb./Mar. 1988), 95-120. Google Scholar
- 12 CURRY, H. B., AND FEYS, R. Combinatory Logic L North-Holland, Amsterdam, 1958.Google Scholar
- 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.Google Scholar
- 14 DEMERS, A. J., AND DONAHUE, J.E. Data types, parameters and type checking. In 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Nev., Jan. 28-30, 1980). ACM, New York, 1980, pp. 12-23. Google Scholar
- 15 DEMERS, A. J., AND DONAHUE, J.E. 'Type-completeness' as a language principle. In 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Nev., Jan. 28-30, 1980). ACM, New York, 1980, pp. 234-244. Google Scholar
- 16 DEMERS, A. J., DONAHUE, J. E., AND SKINNER, G. Data types as values: polymorphism, typechecking, encapsulation. In 5th ACM Symposium on Principles of Programming Languages (Tucson, Ariz., Jan. 23-25, 1978). ACM, New York, 1978, pp. 23-30. Google Scholar
- 17 U.S. DEPARTMENT OF DEFENSE Reference Manual for the Ada Programming Language. GPO 008-000-00354-8, 1980.Google Scholar
- 18 DONAHUE, J. On the semantics of data type. SIAM J. Comput. 8 (1979), 546-560.Google Scholar
- 19 FITTING, M. C. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 1969.Google Scholar
- 20 FORTUNE, S., LEIVANT, D., AND O'DONNELL, M. The expressiveness of simple and second order type structures. J. ACM 30, I (1983), 151-185. Google Scholar
- 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.Google Scholar
- 22 GIRARD, J.~Y. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Univ. Paris VII, Paris, 1972.Google Scholar
- 23 GORDON, M. J., MILNER, R., AND WADSWORTH, C.P. Edinburgh Lecture Notes in Computer Science 78, Springer-Verlag, New York, 1979.Google Scholar
- 24 GRi4TZER G. Universal Algebra. Van Nostrand, New York, 1968.Google Scholar
- 25 GUTTAG, J. V., HOROWlTZ, E., AND MUSSER, D.R. Abstract data types and software validation. Commun. ACM 21, 12 (Dec. 1978), 1048-1064. Google Scholar
- 26 HAYNES, C.T. A theory of data type representation independence. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer- Verlag, New York, 1984, pp. 157-176. Google Scholar
- 27 HERRL1CH, H., AND STRECKER, G.E. Category Theory. Allyn and Bacon, Newton, Mass., 1973.Google Scholar
- 28 HOOK, J.G. Understanding Russell--A first attempt. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 69-85. Google Scholar
- 29 HOOK, J., AND HOWE, D. Impredicative strong existential equivalent to type:type. Tech. Rep. TR 86-760, Cornell Univ., Ithaca, N.Y., 1986. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 32 KAPUR, D. Towards a theory for abstract data types. Tech. Rep. MIT/LCS/TM-237, MIT, Cambridge, Mass., 1980. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 36 LANDIN, P.J. A correspondence between Algol 60 and Church's Lambda-notation. Commun.{ ACM 8, 2, 3 (Feb.-Mar. 1965), 89-101; 158-165. Google Scholar
- 37 LANDIN, P.J. The next 700 programming languages. Commun. ACM 9, 3 (Mar. 1966), 157-166. Google Scholar
- 38 L)/,UCHL1, H. Intuitionistic propositional calculus and definably non-empty terms. J. Symbolic Logic 30 (1965), 263.Google Scholar
- 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.Google Scholar
- 40 LEIVANT, D. Polymorphic type inference. In Proceedings of the lOth ACM Symposium on Principles of Programming Languages (Austin, Tex., Jan. 24-26, 1983). ACM, New York, 1983, pp. 88-98. Google Scholar
- 41 LISKOV, B., SNYDER, A., ATKINSON, R., AND SCHAFFERT, C. Abstraction mechanism in CLU. Commun. ACM 20, 8 (Aug. 1977), 564-576. Google Scholar
- 42 LISKOV, B. ET AL. CLU Reference Manual. Lecture Notes in Computer Science 114, Springer- Verlag, New York, 1981. Google Scholar
- 43 MAC LANE, S. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer-Verlag, New York, 1971.Google Scholar
- 44 MACQUEEN, D.B. Modules for standard ML. In Polymorphism 2, 2 (1985), 35 pages. An earlier version appeared in Proceedings of 1984 ACM Symposium on Lisp and Functional Programming. Google Scholar
- 45 MACQUEEN, D.B. Using dependent types to express modular structure. In Proceedings of the 13th A CM Symposium on Principles of Programming Languages (St. Petersburg Beach, Flu, Jan. 13-15, 1986). ACM, New York, 1986, pp. 277-286. Google Scholar
- 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.Google Scholar
- 47 MCCRACKEN, N. An investigation of a programming language with a polymorphic type structure. Ph.D. dissertation, Syracuse Univ., Syracuse, N.Y., 1979. Google Scholar
- 48 MCCRACKEN, N. The typechecking of programs with implicit type structure. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, 1984. Springer-Verlag, New York, pp. 301-316. Google Scholar
- 49 MEYER, A. R., AND REINHOLD, M. B. Type is not a type. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 13-15, 1986). ACM, New York, 1986. pp. 287-295. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 52 MITCHELL, J. C. Representation independence and data abstraction. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 13-15, 1986). ACM, New York, 1986, pp. 263-276. Google Scholar
- 53 MITCHELL, J.C. Polymo~phic type inference and containment. Inf. Comput. 76, 2/3 (Feb./Mar. 1988), 211-249. Google Scholar
- 54 MITCHELL, J. C., AND HARPER, R. The essence of ML. In Proceedings of the 15th ACM Symposium on Principles of Pragramming Languages (San Diego, Calif., Jan. 13-15, 1988). ACM, New York, 1988, pp. 28-46. Google Scholar
- 55 MITCHELL, J. C., AND MEYER, A. R. Second-order logical relations. In Logics of Programs. Lecture Notes in Computer Science 193, Springer-Verlag, New York, 1985, pp. 225-236. Google Scholar
- 56 MITCHELL, J. C., AND PLOTKIN, G.D. Abstract types have existential types. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan. 14-16, 1985). ACM, New York, 1985, pp. 37-51. Google Scholar
- 57 MITCHELL, J. G., MAYBERRY, W., AND SWEET, R. Mesa language manual. Tech. Rep. CSL- 79-3, Xerox PARC, Palo Alto, Calif., 1979.Google Scholar
- 58 MORRIS, J. H. Types are not sets. In 1st ACM Symposium on Principles of Programming Languages (Boston, Mass., Oct. 1-3, 1973). ACM, New York, 1973, pp. 120-124. Google Scholar
- 59 O'DONNELL, M. A practical programming theorem which is independent of Peano arithmetic. In 11th ACM Symposium on the Theory of Computation (Atlanta, Ga., Apr. 30-May 2, 1979). ACM, New York, 1979, pp. 176-188. Google Scholar
- 60 PRAWlTZ, D. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.Google Scholar
- 61 PRAWITZ, D. Ideas and results in proof theory. In 2nd Scandinavian Logic Symposium. North- Holland, Amsterdam, 1971, pp. 235-308.Google Scholar
- 62 REYNOLDS, J.C. Towards a theory of type structure. In Paris Colloquium on Programming. Lecture Notes in Computer Science 19, Springer-Verlag, New York, 1974, pp. 408-425. Google Scholar
- 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.Google Scholar
- 64 REYNOLDS, J.C. Types, abstraction, and parametric polymorphism. In IFIP Congress (Paris, Sept. 1983).Google Scholar
- 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.Google Scholar
- 66 SHAW, M. (Ed.) ALPHARD: Form and Content. Springer-Verlag, New York, 1981.Google Scholar
- 67 STATMAN, R. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9 (1979), 67-72.Google Scholar
- 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.Google Scholar
- 69 STENLUND, S. Combinators, ),-terms and Proof Theory. Reidel, Dordrecht, Holland, 1972.Google Scholar
- 70 TROELSTRA, A.S. Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer-Verlag, New York, 1973.Google Scholar
- 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.Google Scholar
Index Terms
- Abstract types have existential type
Recommendations
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Polymorphic type inference and abstract data types
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...
Reviews
David A. Watt
The title of this paper suggests a hot new discovery being rushed out of the laboratory and announced to the world. The reality is less exciting and says much about publication delays. The paper was first presented at a symposium in January 1985; it was submitted to TOPLAS in June 1986 and revised in March 1988. The delay should have provided an opportunity to polish the paper, but a number of careless errors have persisted, and the ML examples use syntax that is years out of date. The main theme of this paper is that existential types (which derive from constructive type theory) can be used to ascribe types to implementations of abstract types. For example, the omnipresent t-stack abstract type has the signature :.OC :.HB abstype tstack with empty: t-stack, push: t ? 9Tt-stack :2WZ t-stack, pop: t-stack :2WZ t ? 9Tt-stack :.HT :.OE and each of its implementations would have the existential type :.OC :.HB ? 9Ts. s ? 9T(t ? 9Ts :2WZ t)- ? 9T(s :2WZ t ? ).:.HT :.OE (the authors use ` ? for Cartesian product). Similarly, the t-queue abstract type might have the signature :.OC :.HB abstype t-queue with empty: t-queue insert: t ? 9Tt-queue:2WZ t-queue remove: t-queue :2WZ t ? t-queue, :.HT :.OE and the corresponding existential type would be :.OC :.HB ? Qq. q ? Q(t ? 9Tq :2WZ q)- ? q :2WZ t ? 9Tq).:.HT :.OE The above two existential types are equivalent; they are independent of the operations' names and of their intended semantics. Since abstract type implementations have types, they are first-class values and can be passed as parameters and returned as function results. The authors exploit these capabilities by presenting a tree-search function with a formal parameter of the above existential type. When the function is called with a stack implementation as an actual parameter, it performs a depth-first search. When called with a queue implementation, the function performs a breadth-first search (actually, right to left). This may not be useful in practice; the tree-search function is hard to understand. Another of the authors' examples is what must be the most opaque programming of the sieve algorithm ever published. This paper invites comparison with Cardelli and Wegner's 1985 survey paper on type theory [1]. The latter paper was more timely, more accurate, and more readable, yet it is not even referenced in this paper.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments