|
While we are on the topic of types (see the disucssion on units of measure for example).
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques.
This typeful programming style is in a sense independent of the language it is embedded in; it adapts equally well to functional, imperative, object-oriented, and algebraic programming, and it is not incompatible with relational and concurrent programming.
The main purpose of this paper is to show how typeful programming is best supported by sophisticated type systems, and how these systems can help in clarifying programming issues and in adding power and regularity to languages.
Among other things this paper contains some software enginerring perspective (programming in the large etc.), and a comparison withother programming styles (e.g., typelss prograaming, functional programming, imperative programming).
Warning: The paper is quite long at 67 pages. However there are many details and notation sections that can be skimmed.
Posted to theory by Ehud Lamm on 2/15/01; 12:22:51 PM
|
Typeful Programming
