A Theory of Type Polymorphism in Programming

Robin Milner, 1978, Journal of Computer and System Sciences

About this paper

This paper is under a licence that does not allow it to be reproduced, so what is here is its front matter and a short abstract. Read it at the publisher's page.

English
Tiếng Việt

Edinburgh Research Explorer

A theory of type polymorphism in programming

Citation for published version: Milner, R 1978, 'A theory of type polymorphism in programming', Journal of Computer and System Sciences, vol. 17, no. 3, pp. 348-375. https://doi.org/10.1016/0022-0000(78)90014-4

Digital Object Identifier (DOI): 10.1016/0022-0000(78)90014-4

Link: Link to publication record in Edinburgh Research Explorer

Document Version: Publisher's PDF, also known as Version of record

Published In: Journal of Computer and System Sciences

General rights Copyright for the publications made accessible via the Edinburgh Research Explorer is retained by the author(s) and / or other copyright owners and it is a condition of accessing these publications that users recognise and abide by the legal requirements associated with these rights.

Take down policy The University of Edinburgh has made every reasonable effort to ensure that Edinburgh Research Explorer content complies with UK legislation. If you believe that the public display of this file breaches copyright please contact openaccess@ed.ac.uk providing details, and we will remove access to the work immediately and investigate your claim.

A Theory of Type Polymorphism in Programming

ROBIN MILNER

Computer Science Department, University of Edinburgh, Edinburgh, Scotland

Received October 10, 1977; revised April 19, 1978

The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W\mathcal{W} which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot "go wrong" and a Syntactic Soundness Theorem states that if W\mathcal{W} accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W\mathcal{W} is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.

Trích dẫn cho phiên bản đã xuất bản:

Milner, R 1978, 'A theory of type polymorphism in programming', Journal of Computer and System Sciences, vol. 17, no. 3, pp. 348-375. https://doi.org/10.1016/0022-0000(78)90014-4

Mã định danh đối tượng số (DOI):

10.1016/0022-0000(78)90014-4

Liên kết:

Liên kết tới bản ghi xuất bản trong Edinburgh Research Explorer

Phiên bản tài liệu:

PDF của nhà xuất bản, còn được gọi là phiên bản chính thức

Được xuất bản trong:

Journal of Computer and System Sciences

Quyền chung

Bản quyền đối với các ấn phẩm được cung cấp thông qua Edinburgh Research Explorer thuộc về tác giả và / hoặc các chủ sở hữu bản quyền khác và là điều kiện để người dùng các ấn phẩm này công nhận và tuân thủ các yêu cầu pháp lý liên quan đến các quyền này.

Chính sách gỡ xuống

Đại học Edinburgh đã nỗ lực hợp lý để đảm bảo rằng Edinburgh Research Explorer tuân thủ luật pháp Vương quốc Anh. Nếu bạn tin rằng việc công khai tệp này vi phạm bản quyền, vui lòng liên hệ openaccess@ed.ac.uk và cung cấp chi tiết, chúng tôi sẽ gỡ quyền truy cập và điều tra vấn đề.

ROBIN MILNER

Khoa Khoa học Máy tính, Đại học Edinburgh, Edinburgh, Scotland

Nhận ngày 10 tháng 10 năm 1977; sửa đổi ngày 19 tháng 4 năm 1978

Mục tiêu của công trình này phần lớn mang tính thực tiễn. Một phong cách lập trình được sử dụng rộng rãi, đặc biệt trong các ngôn ngữ xử lý cấu trúc không áp đặt kỷ luật về kiểu, bao hàm việc định nghĩa các thủ tục hoạt động tốt trên các đối tượng thuộc nhiều loại khác nhau. Chúng tôi trình bày một kỷ luật kiểu hình thức cho các thủ tục đa hình như vậy trong ngữ cảnh của một ngôn ngữ lập trình đơn giản, cùng với một thuật toán kiểm tra kiểu tại thời điểm biên dịch W\mathcal{W} thực thi kỷ luật này.

1 INTRODUCTION

This section is missing here.

2 ILLUSTRATIONS OF THE TYPE DISCIPLINE

This section is missing here.

3 A Simple Applicative Language and Its Types

This section is missing here.

4 A Well-Typing Algorithm and Its Correctness

This section is missing here.

5 Types in Extended Languages

This section is missing here.

6 Conclusion

This section is missing here.

Acknowledgments

This section is missing here.

References

  1. W. H. Burge, "Recursive Programming Techniques," Addison-Wesley, Reading, Mass., 1975.
  2. M. Gordon, R. Milner, and C. Wadsworth, "Edinburgh LCF," CSR-11-77, Computer Science Dept., Edinburgh University, 1977.
  3. M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth, A metalanguage for interactive proof in LCF, in "Proc. 5th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Tucson, Arizona, 1978."
  4. D. Gries and N. Gehani, Some ideas on data type in high-level languages, Comm. ACM. 20 (1977), 414–420.
  5. R. Hindley, The principal type-scheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969), 29–60.
  6. B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, and G. L. Popek, Report on the programming language Euclid, SIGPLAN Notices (ACM) 12, 2 (1977).
  7. P. J. Landin, The next 700 programming languages, Comm. ACM 9 (1966), 157–164.
  8. B. H. Liskov and S. Zilles, Programming with abstract data types, in “Proc. of ACM SIGPLAN conference on Very High Level Languages,” SIGPLAN Notices (ACM) 9 (1974), 50–59.
  9. R. Milner, “Models of LCF,” Mathematical Centre, Amsterdam, Tracts, Vol. 82, pp. 49–63, 1976.
  10. J. H. Morris, “Lambda-Calculus Models of Programming Languages,” Ph.D. Thesis, MAC-TR-57, MIT, 1968.
  11. G. Plotkin, A power-domain construction, SIAM J. Comput. 5 (1976), 452–487.
  12. J. C. Reynolds, “Towards a Theory of Type Structure,” Systems and Inform. Sci., Syracuse University, 1974.
  13. J. C. Reynolds, Syntactic control of interference, in “Proc. 5th ACM Symposium on Principles of Programming Languages, Tucson, Arizona, 1978,” pp. 39–46.
  14. J. A. Robinson, A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach. 12 (1965), 23–41.
  15. D. Scott, Lattice theoretic models for various type-free calculi, in “Proc. 4th International Congress for Logic, Methodology and Philosophy of Science, Bucharest, Rumania, 1972.”
  16. D. Scott and C. Strachey, Towards a mathematical semantics for computer languages, in “Proc. Symposium on Computers and Automata,” Vol. 21, Microwave Res. Inst. Symposia Series, Polytech. Inst. of Brooklyn, 1971.
  17. D. Scott, Data types as lattices, SIAM J. Comput. 5 (1976), 522–587.
  18. A. Shamir and W. Wadge, Data types as objects, in “Proc. 4th ICALP Conference, Turku, Finland, 1977.”
  19. C. Strachey, Fundamental concepts in programming languages, Notes for the International Summer School in Computer Programming, Copenhagen, 1967.
  20. R. D. Tennent, On a new approach to representation-independent data classes, Acta Inform. 8 (1977), 315–324.
  21. B. Wegbreit, The treatment of types in EL1, Comm. ACM 17 (1974), 251–264.
  22. A. van Wijngaarden et al., Revised report on the algorithmic language ALGOL 68, Acta Informatica 5 (1975), 1–236.
  23. R. A. Wulf, R. L. London, and M. Shaw, “Abstraction and Verification in ALPHARD: Introduction to Language and Methodology,” ISI/RR-76-46, Univ. of California, 1976.

Read off the page by a vision model reading the page images using olmOCR-2-7B-1025-FP8.

Read off the page by a vision model reading the page images using olmOCR-2-7B-1025-FP8. Translated into Tiếng Việt by gpt-5, against glossary version 7. Translated from the English.