Neil Ghani
(University of Strathclyde)
An Algebraic Approach to Parametricity

The world is more uniform than we might imagine. For example it is riven with symmetries whose mathematical formalisation has proved to be of fundamental importance. These uniformities exist not just in Physics and Mathematics, but also in Logic and Computer Science. For example, polymorphic functions such as the function rev : List A -> List A (which reverses every element of a list containing elements of type A) does not inspect the type A. Indeed, rev ignores the type A and rather performs an algorithm which does not vary as A varies. The algorithm for reversing a list of integers is exactly the same as that for reversing a list of strings! This phenomenon has come to be known in programming languages research as parametricity and is one of the most sophisticated tools possessed by programming language researchers.

I'd go further. I believe parametricity has much deeper significance than its incarnation within programming languages research might suggest. In order to deploy parametricity outside programming languages we need to develop a more abstract understanding of parametricity and in this talk I will sketch some ways in which I have been doing this. My fundamental conclusion is this: while our understanding of the world is usually inherently categorical (being built from the language of categories, functors and natural transformations) parametricity involves a fibrational understanding of the world based upon fibrations, fibred functors and fibred natural transformations. The aim of my talk will be to get the ideas behind this position across and thus I will not assume familiarity with either parametricity or category theory.