Book contents
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- 42 Modularity and Linking
- 43 Singleton Kinds and Subkinding
- 44 Type Abstractions and Type Classes
- 45 Hierarchy and Parameterization
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
42 - Modularity and Linking
from Part XVII - Modularity
Published online by Cambridge University Press: 05 March 2016
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- 42 Modularity and Linking
- 43 Singleton Kinds and Subkinding
- 44 Type Abstractions and Type Classes
- 45 Hierarchy and Parameterization
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
Summary
Modularity is the most important technique for controlling the complexity of programs. Programs are decomposed into separate components with precisely specified, and tightly controlled, interactions. The pathways for interaction among components determine dependencies that constrain the process by which the components are integrated, or linked, to form a complete system. Different systems may use the same components, and a single system may use multiple instances of a single component. Sharing of components amortizes the cost of their development across systems and helps limit errors by limiting coding effort.
Modularity is not limited to programming languages. In mathematics, the proof of a theorem is decomposed into a collection of definitions and lemmas. References among the lemmas determine a dependency relation that constrains their integration to form a complete proof of the main theorem. Of course, one person's theorem is another person's lemma; there is no intrinsic limit on the depth and complexity of the hierarchies of results in mathematics. Mathematical structures are themselves composed of separable parts, for example, a ring comprises a group and a monoid structure on the same underlying set. Modularity arises from the structural properties of the hypothetical and general judgments. Dependencies among components are expressed by free variables whose typing assumptions state the presumed properties of the component. Linking amounts to substitution to discharge the hypothesis.
Simple Units and Linking
Decomposing a program into units amounts to exploiting the transitivity of the hypothetical judgment (see Chapter 3). The decomposition may be described as an interaction between two parties, the client and the implementor, mediated by an agreed-upon contract, an interface. The client assumes that the implementor upholds the contract, and the implementor guarantees that the contract will be upheld. The assumption made by the client amounts to a declaration of its dependence on the implementor discharged by linking the two parties accordng to their agreed-upon contract.
The interface that mediates the interaction between a client and an implementor is a type. Linking is the implementation of the composite structural rules of substitution The type τintf is the interface type. It defines the operations provided by the implementor eimpl and relied upon by the client eclient.
- Type
- Chapter
- Information
- Practical Foundations for Programming Languages , pp. 395 - 398Publisher: Cambridge University PressPrint publication year: 2016