A good abstraction or two can be invaluable for programming, enabling reasoning, performance, and maintainability. We build abstractions by erecting barriers to the flow of information between implementations and their clients.

John Reynolds’ theory of relational parametricity seeks to explain abstraction in terms of invariance under change. Reynolds’ original theory explains abstract types by modelling change of representation types by mathematical relations. In essence, we have successfully maintained a barrier to information flow if the program is invariant under all changes of representation that act identically given the information they are permitted to have.

In this talk, I’ll present some ways of generalising Reynolds’ theory to novel applications by considering alternative notions of change. Change in space and time yields applications to geometry and classical mechanics. Considering changes as distances affords quantitative accounting of information flow. Indexed and dependent types allow programmers more precision in describing changes and so more precision is defining abstractions.