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
- 14 Generic Programming
- 15 Inductive and Coinductive 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
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
14 - Generic Programming
from Part VI - Infinite Data Types
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
- 14 Generic Programming
- 15 Inductive and Coinductive 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
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
Summary
Many programs are instances of a pattern in a particular situation. Sometimes types determine the pattern by a technique called (type) generic programming. For example, in Chapter 9, recursion over the natural numbers is introduced in an ad hoc way. As we shall see, the pattern of recursion on values of an inductive type is expressed as a generic program.
To get a flavor of the concept, consider a function f of type ρ → ρ', which transforms values of type ρ into values of type ρ'. For example, f might be the doubling function on natural numbers.We wish to extend f to a transformation from type [ρ/t]τ to type [ρ'/t]τ by applying f to various spots in the input, where a value of type ρ occurs to obtain a value of type ρ', leaving the rest of the data structure alone. For example, τ might be bool × t, in which case f could be extended to a function of type bool × ρ → bool × ρ' that sends the pairs ⟨a, b⟩ to the pair ⟨a, f (b⟩.
The foregoing example glosses over an ambiguity arising from the many-one nature of substitution. A type can have the form [ρ/t]τ in many different ways, according to how many occurrences of t there are within τ. Given f as above, it is not clear how to extend it to a function from [ρ'/t]τ to [ρ/t]τ. To resolve the ambiguity, we must be given a template that marks the occurrences of t in τ at which f is applied. Such a template is known as a type operator, t.τ, which is an abstractor binding a type variable t within a type τ. Given such an abstractor, we may unambiguously extend f to instances of τ given by substitution for t in τ.
The power of generic programming depends on the type operators that are allowed. The simplest case is that of a polynomial type operator, one constructed from sum and product of types, including their nullary forms. These are extended to positive type operators, which also allow certain forms of function types.
- Type
- Chapter
- Information
- Practical Foundations for Programming Languages , pp. 119 - 124Publisher: Cambridge University PressPrint publication year: 2016