The essence of ML

ABSTRACT

Standard ML is a useful programming language with polymorphic expressions and a flexible module facility. One notable feature of the expression language is an algorithm which allows type information to be omitted. We study the implicitly-typed expression language by giving a “syntactically isomorphic” explicitly-typed, polymorphic function calculus. Unlike the Girard-Reynolds polymorphic calculus, for example, the types of our ML calculus may be built-up by induction on type levels (universes). For this reason, the pure ML calculus has straightforward set-theoretic, recursion-theoretic and domain-theoretic semantics, and operational properties such as the termination of all recursion-free programs may be proved relatively simply. The signatures, structures, and functors of the module language are easily incorporated into the typed ML calculus, providing a unified framework for studying the major features of the language (including the novel “sharing constraints” on functor parameters). We show that, in a precise sense, the language becomes inconsistent if restrictions imposed by type levels are relaxed. More specifically, we prove that the important programming features of ML cannot be added to any impredicative language, such as the Girard-Reynolds calculus, without implicitly assuming a type of all types.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	ABL86	R. Amadio, K. Bruce, and G. Longo. The finitary projection model for second order lambda calculus and solutions to higher order domain, equations. In IEEE Symp. Logic in Computer Science, pages }22- 130, 1986.
	Bar84	H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 198,i. (revised edition).
	BM84	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
	BMM88	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]
	C*86	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
	Car84	Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
	Car85	Robert Cartwright, Types as intervals, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.22-36, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318604]
	CH84	T. Coquand and G. Huet. A theory of constructions. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), Springer LNCS 173, June 1984. Paper does not appear in proceedings.
	Coq86	T. Coquand. An analysis of girard's paradox. In Proc. IEEE Symp. on Logic in Computer Science, pages 227-236, June 1986.
	CW86	Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
	CZ86	M. Coppo and M. Zacchi. Type inference and logical relations. In Proc. IEEE Syrup. on Logic in Computer Science, pages 218-226, June 1986.
	DB80	N.G. De Bruijn. A survey of the project automath. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 579-607, Academic Press, 1980.
	DM82	Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
	FS87	P. Freyd and A. Scedrov. Some semantic aspects of polymorphic lambda calculus. In IEEE Syrup. Logic in Computer Science, pages 315-319, June } 987.
	Gir71	J.-Y. Girard. Une extension de l'interpretation de G6del ~ l'analyse, et son application l'~limination des coupures dans l'analyse et la th@orie des types. In J.E. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 63-92, North-Holland, 1971.
	Gir72	J.-Y. Girard. Interpretation fonctionelte et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Universite Paris VII, }972.
	GMW79	M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, } 979.
	Gor79	Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
	HH86	James G. Hook , Douglas J. Howe, Impredicative Strong Existential Equivalent to Type:Type, Cornell University, Ithaca, NY, 1986
	HMM86	R. Harper, D.B. MacQueen, and R. Milnet. Standard ML. Technical Report ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science, Edinburgh University, March }986.
	HMT87a	R. Harper, R. Milner, and M. Tof~e. The Semantics of Standard ML. Technical Report ECS-LFCS-87-36, Laboratory for the Foundations of Computer Science, Edinburgh University, August 1987.
	HMT87b	R. Harper , R. Milner , M. Tofte, A type discipline for Program modules, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.308-319, March 1987, Pisa, Italy
	How80	W. Howard. The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda- Calculus and Formalism, pages 479-490, Academic Press, 1980.
	How87	D.J. Howe. The computational behavior of girard's paradox. In IEEE Symp. Logic in Computer Science, pages 205- 214, June 1987.
	Lei83	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]
	LS86	J. Lambek , P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, New York, NY, 1986
	Mac71	S. MacLane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathematics, Springer-Verlag, 1971.
	Mac85	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]
	Mac86	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]
	Mar73	P. Martin-LSf. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium, '73, pages 73-118, North-Holland, Amsterdam, 1973.
	Mar82	P. Martin-LSf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175, North-Holland, Amsterdam, 1982.
	McC79	Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
	Mil77	R. Milner. Fully abstract models of typed lambda calculi. Theoretical Computer Science, 4 (1), 1977.
	Mil78	R. Milner. A theory of type polymorphism in programming. JCSS, 17, 1978. pages 348-375.
	Mil85	R. Milner. The standard ml core language. Polymorphism, 2(2), 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.
	Mit86a	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]
	Mit86b	John C. Mitchell, A type-inference approach to reduction properties and semantics of polymorphic expressions (summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.308-319, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319872]
	Mit87	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]
	MM85	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
	MP85	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]
	MPS86	David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
	MR86	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]
	Mul84	K. Mulmuley. A semantic characterization of full abstraction for typed lambda calculus. In Proc. 25-th IEEE Syrup. on Foundations of Computer Science, pages 279-288, 1984.
	Plo75	G.D. Plotkin. Call-by-name, call-byvalue, and the lambda calculus. Theoretical Computer Science, 1:125-159, } 975.
	Plo77	G.D. Plotkin. Lcf considered as a programming language. Theoretical Computer oczence, 1"3~ 1977.
	Rey74	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	Rey81	J.C. Reynolds. The essence of algol. In de Bakker and van Vliet, editors, Algorithmic Languages, pages 345-372, IFIP, North Holland, 1981.
	Rey83	J.C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing '83, pages 513-523, North-Holland, Amsterdam, 1983.
	Rey84	J.C. Reynolds. Polymorphism is not settheoretic. In Proc. Int. Symp. on Semantics of Data Types, Sophia-A ntipolis (France), Springer LNCS 173, pages 145- 156, Springer-Verlag, 1984.
	Sco80	D.S. Scott. Relating theories of the lambda calculus. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 403-450, Academic Press, 1980.
	Sol78	Marvin Solomon, Type definitions with parameters, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.31-38, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512765]
	Sta85	R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85-97, 1985.
	Tro73	A.S. Troelstra. Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Volume 344 of Lecture Notes in Mathematics, Springer-Vertag, 1973.
	Wan84	Mitchell Wand, A types-as-sets semantics for milner-style polymorphism, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.158-164, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800527]