Abstraction and invariance for algebraically indexed types

Robert Atkey, Patricia Johann, Andrew Kennedy

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

4 Citations (Scopus)

Abstract

Reynolds’ relational parametricity provides a powerful way to rea- son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the- ory 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 trian- gle, then we scale its area, maintaining an invariant relationship be- tween the two. The transformations under which properties are in- variant 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 ge- ometric 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 Theo- rem include free theorems expressing invariance properties of pro- grams, 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.
LanguageEnglish
Title of host publicationProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Subtitle of host publicationPOPL '13
EditorsRoberto Giacobazzi, Radhia Cousot
Pages87-100
Number of pages14
DOIs
Publication statusPublished - Jan 2013
EventProceedings of the 40th ACM SIGACT-SIGPLAN Symposium, POPL 2013. - Rome, United Kingdom
Duration: 23 Sep 201325 Sep 2013

Conference

ConferenceProceedings of the 40th ACM SIGACT-SIGPLAN Symposium, POPL 2013.
CountryUnited Kingdom
CityRome
Period23/09/1325/09/13

Fingerprint

abstraction
programming language
information flow
computer science
physics
continuity
Group
mathematics

Keywords

  • abstraction
  • invariance
  • algebraically indexed types

Cite this

Atkey, R., Johann, P., & Kennedy, A. (2013). Abstraction and invariance for algebraically indexed types. In R. Giacobazzi, & R. Cousot (Eds.), Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : POPL '13 (pp. 87-100) https://doi.org/10.1145/2429069.2429082
Atkey, Robert ; Johann, Patricia ; Kennedy, Andrew. / Abstraction and invariance for algebraically indexed types. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : POPL '13. editor / Roberto Giacobazzi ; Radhia Cousot. 2013. pp. 87-100
@inproceedings{1d8a492abd534cc9a8fc4fe8322866ce,
title = "Abstraction and invariance for algebraically indexed types",
abstract = "Reynolds’ relational parametricity provides a powerful way to rea- son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the- ory 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 trian- gle, then we scale its area, maintaining an invariant relationship be- tween the two. The transformations under which properties are in- variant 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 ge- ometric 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 Theo- rem include free theorems expressing invariance properties of pro- grams, 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.",
keywords = "abstraction , invariance, algebraically indexed types",
author = "Robert Atkey and Patricia Johann and Andrew Kennedy",
year = "2013",
month = "1",
doi = "10.1145/2429069.2429082",
language = "English",
isbn = "978-1-4503-1832-7",
pages = "87--100",
editor = "Roberto Giacobazzi and Radhia Cousot",
booktitle = "Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages",

}

Atkey, R, Johann, P & Kennedy, A 2013, Abstraction and invariance for algebraically indexed types. in R Giacobazzi & R Cousot (eds), Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : POPL '13. pp. 87-100, Proceedings of the 40th ACM SIGACT-SIGPLAN Symposium, POPL 2013., Rome, United Kingdom, 23/09/13. https://doi.org/10.1145/2429069.2429082

Abstraction and invariance for algebraically indexed types. / Atkey, Robert; Johann, Patricia; Kennedy, Andrew.

Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : POPL '13. ed. / Roberto Giacobazzi; Radhia Cousot. 2013. p. 87-100.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Abstraction and invariance for algebraically indexed types

AU - Atkey, Robert

AU - Johann, Patricia

AU - Kennedy, Andrew

PY - 2013/1

Y1 - 2013/1

N2 - Reynolds’ relational parametricity provides a powerful way to rea- son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the- ory 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 trian- gle, then we scale its area, maintaining an invariant relationship be- tween the two. The transformations under which properties are in- variant 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 ge- ometric 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 Theo- rem include free theorems expressing invariance properties of pro- grams, 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.

AB - Reynolds’ relational parametricity provides a powerful way to rea- son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the- ory 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 trian- gle, then we scale its area, maintaining an invariant relationship be- tween the two. The transformations under which properties are in- variant 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 ge- ometric 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 Theo- rem include free theorems expressing invariance properties of pro- grams, 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.

KW - abstraction

KW - invariance

KW - algebraically indexed types

UR - http://www.scopus.com/inward/record.url?scp=84874155816&partnerID=8YFLogxK

UR - https://personal.cis.strath.ac.uk/robert.atkey/algebraic-indexed.html

UR - https://personal.cis.strath.ac.uk/robert.atkey/algebraic-indexed.pdf

U2 - 10.1145/2429069.2429082

DO - 10.1145/2429069.2429082

M3 - Conference contribution book

SN - 978-1-4503-1832-7

SP - 87

EP - 100

BT - Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

A2 - Giacobazzi, Roberto

A2 - Cousot, Radhia

ER -

Atkey R, Johann P, Kennedy A. Abstraction and invariance for algebraically indexed types. In Giacobazzi R, Cousot R, editors, Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : POPL '13. 2013. p. 87-100 https://doi.org/10.1145/2429069.2429082