FP with data abstraction and strong typing
John V. Guttag, James J. Horning, John H. P. Williams · 1981
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.