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.
We start with an introduction to the notions of types, subtypes and polymorphism. Then we
introduce a general framework, derived in part from constructive logic, into which most of the
known type systems can be accommodated and extended. The main part of the paper shows how
this framework can be adapted systematically to cope with actual programming constructs. For
concreteness we describe a particular programming language with advanced features; the emphasis
here is on the combination of subtyping and polymorphism. We then discuss how typing concepts
apply to large programs, made of collections of modules, and very large programs, made of
collections of large programs. We also sketch how typing applies to system programming; an area
which by nature escapes rigid typing. In summary, we compare the most common programming
styles, suggesting that many of them are compatible with, and benefit from, a typeful discipline.