FP with data abstraction and strong typing

ABSTRACT

This paper begins by presenting arguments for including data abstraction and compile time type checking in functional programming languages, and discussing in general terms the mechanisms required to provide support for these features. It then goes on to present brief introductions to the algebraic style of formally specifying abstract data types and to the FP style of writing functional programs. The middle section describes a version of FP that includes type checking and data abstraction. The key to this is the development of a framework for describing the FP type system in terms of the already existing algebra of FP programs. The paper concludes with an example program illustrating the style of FP programming made possible by our extensions.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: John Backus, The Algebra of Functional Programs: Function Level Reasoning, Linear Equations, and Extended Definitions, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.1-43, April 19-25, 1981
• 3: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 4: Ole-Johan Dahl, SIMULA 67 common base language, (Norwegian Computing Center. Publication), 1968
• 5: Demers, A. and Donahue, J. (1980) Report on the programming language Russell, Department of Computer Sci., Cornell University.
• 6: Goguen, J.A., and Tardo, J.J. (1979) An introduction to OBJ: a language for writing and testing formal algebraic program specifications. Specifications of Reliable Software Conf. Proc., Cambridge, MA. April.
• 7: Goguen, J.A., Thatcher, J.W., and Wagner, E.G. (1975) An initial algebra approach to the specification, correctness, and implementation of abstract data types. Current Trends in Programming Methodology, Ed. Yeh, R. Prentice-Hall.
• 8: Guttag, J.V. (1980) Notes on type abstraction (version 2). IEEE Transactions on Soft. Eng., Vol. SE.6, No. 1, pp. 13-23, January.
• 9: 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]
• 10: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 11: John Vogel Guttag, The specification and application to programming of abstract data types., 1975
• 12: Hoare, C.A.R. (1972) Proofs of correctness of data representations, Acta Informatica, Vol. 1, No. 1, pp.271. 280.
• 13: Knuth, D.E. and Bendix, P.B. (1970) Simple word problems in universal algebras, in Computational Problems in Abstract Algebras, Ed. Leech, J., pp. 263-297, New York: Pergamon.
• 14: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 15: 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]
• 16: 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]
• 17: 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]
• 18: U.S. Department of Defense (1980) Reference manual for the Ada programming language. July.
• 19: Williams, John (1980) On the development of the algebra of functional programs. Report No. RJ2983, IBM Research Laboratory, San Jose, California, October.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

General Terms:
Languages, Verification