# Abstraction and Invariance for Algebraically Indexed Types

## Publication Information

Robert Atkey, Patricia Johann, and Andrew Kennedy.

*Abstraction and Invariance for Algebraically Indexed Types*. In

*40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)*. 2013.

DOI:

10.1145/2500365.2500597## Abstract

Reynolds' relational parametricity provides a powerful way to reason
about programs in terms of invariance under changes of data
representation. A dazzling array of applications of Reynolds' theory
exists, exploiting invariance to yield ``free theorems'',
non-inhabitation results, and encodings of algebraic datatypes.
Outside computer science, invariance is a common theme running
through many areas of mathematics and physics. For example, the area of
a triangle is unaltered by rotation or flipping. If we scale a
triangle, then we scale its area, maintaining an invariant
relationship between the two. The transformations under which
properties are invariant are often organised into groups, with the
algebraic structure reflecting the composability and invertibility
of transformations.

In this paper, we investigate programming languages whose types are
indexed by algebraic structures such as groups of geometric
transformations. Other examples include types indexed by
principals--for information flow security--and types indexed by
distances--for analysis of analytic uniform continuity
properties. Following Reynolds, we prove a general Abstraction
Theorem that covers all these instances. Consequences of our
Abstraction Theorem include free theorems expressing invariance
properties of programs, type isomorphisms based on invariance
properties, and non-definability results indicating when certain
algebraically indexed types are uninhabited or only inhabited by
trivial programs. We have fully formalised our framework and most
examples in Coq.

## Additional Information

The Coq development (and source for the paper) is available on Github.