John Guttag
James Horning
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.
- 1.Backus, John (1978) Can programming be liberated from the von Neumann style? A functional style and its algebra of programs, CACM, Vol. 21, No. 8, pp. 613-639, August. Google Scholar
Digital Library
- 2.Backus, John (1981) The algebra of functional programs: function level reasoning, linear equations, and extended definitions, in Formalization of Programming Concepts, Lecture Notes in Computer Science No. 107, Springer-Verlag, April. Google ScholarDigital Library
- 3.Burstall, R.M., MacQueen, DB., and Sannella, D.T. (1980) Hope: An experimental applicative language. Proc. of 1980 LISP Conference, pp. 136-143, Stanford, Ca. August. Google ScholarDigital Library
- 4.Dahl, O.J., Nygaard, K., and Myhrhuag, B. (1968) The SIMULA 67 common base language, Norwegian Computing Centre, Forskningsveien 1B, Oslo. Google ScholarDigital Library
- 5.Demers, A. and Donahue, J. (1980) Report on the programming language Russell, Department of Computer Sci., Cornell University.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 9.Guttag, J.V., Horowitz, E., and Musser, D.R. (1978) Abstract data types and software validation, Comm. ACM, Vol. 21, pp. 1048-1064, December; also USC Information Sciences Institute Tech. Rep., Aug. 1976. Google ScholarDigital Library
- 10.Guttag, J.V. (1977) Abstract data types and the development of data structures. Comm. ACM, Vol. 20, No. 6, pp. 396-404, June. Google ScholarDigital Library
- 11.Guttag, J.V. (1975) The specification and application to programming of abstract data types. Ph.D. dissertation, Univ. Toronto, Dept. Comput. Sci., 1975. Google ScholarDigital Library
- 12.Hoare, C.A.R. (1972) Proofs of correctness of data representations, Acta Informatica, Vol. 1, No. 1, pp.271. 280.Google ScholarDigital Library
- 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.Google Scholar
- 14.Lampson, B.W., Horning, J.J., London, R.L., Mitchell, J.G., and Popek, G.J. (1977) Revisod report on the programming language Euclid. Xerox Palo Alto Res. Centers, an earlier version appeared in SIGPLAN Notices, vol. 12, Feb. 1977. Google ScholarDigital Library
- 15.Landin, P.J. (1966) The next 700 programming languages. Comm. ACM, Vol. 9, No. 3 pp. 157-166, March. Google ScholarDigital Library
- 16.Liskov, B.H., Snyder, A., Atkinson, R., and Shaffert, C. (1977) Abstraction mechanisms in Clu. Comm. ACM, Vol. 20, No. 8 pp. 564-576, August. Google ScholarDigital Library
- 17.Morris, J.H. (1973) Types are not sets. Proc. ACM Symp. Principles of Programming Languages, pp. 120-124, October. Google ScholarDigital Library
- 18.U.S. Department of Defense (1980) Reference manual for the Ada programming language. July.Google Scholar
- 19.Williams, John (1980) On the development of the algebra of functional programs. Report No. RJ2983, IBM Research Laboratory, San Jose, California, October.Google Scholar
Index Terms
- FP with data abstraction and strong typing
Recommendations
Typing dynamic typing
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programmingEven when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...
Typing dynamic typing
Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...
Embedding polymorphic dynamic typing
WGP '11: Proceedings of the seventh ACM SIGPLAN workshop on Generic programmingDynamic typing in a statically typed functional language allows us to defer type unification until run time. This is typically useful when interacting with the 'outside' world where the type of values involved may not be known statically. Haskell has ...
Comments