Modules have a boundary which separate a server (the
implementation) from its clients. Clients most commonly are other
modules. The boundary itself is expressed as a type, a set of related
assertions, together building up a contract (for the concept of
contract, see again [Meyer88]).
Ideally, types are abstract in both a restrictive and a generative meaning:
Any user of a resource becomes dependent on it, and thus, on the
implementation of this one's type. Paradoxically, this constrains the
server since, in the context of incremental development, it is not
affordable to invalidate existing client code by changing the
implementation.
The consequence is that potential new implementations are bound to
satisfy every prior use! We saw that developers cannot rely on
exhaustive regression testing. They have yet to face this
responsibility.
Static type checking actually splits the dependency into two
parts: between the clients and the type, between the server and the
type. By constraining the clients more, it takes part of the
developer's responsibility.
An example will hopefully make things more concrete: let's
consider a zoo populated in a first phase only with herbivores. The
routine of feeding them with vegetal food may work satisfactorily
until the day when one introduces the first tiger. Until then, the
dynamic checking performed by the animals themselves had always
succeeded. In this example, the developer responsible for introducing
the tiger is actually constrained by the existing routine. The
assertions bound to the animal type do not guarantee the validity of
this routine. They are indeed never checked, since the checking is
only performed on the basis of the most derived, dynamic types.
Corrective action has to take place outside of the scope of the
change.