BOB ATKEY

Slides and notes for my OBT “Generalising Abstraction” talk

Tuesday 26th January 2016

Here are the slides I used for my keynote talk for the afternoon at this year’s Off the Beaten Track workshop in St. Petersburg, Florida, USA. Many thanks to Lindsey Kuper for inviting me to give a talk and for organising it all.

The talk wasn’t recorded, but here is a collection of notes to go with the things I talked about:

• The Abstract is ‘an Enemy’ is a paper by Alan F. Blackwell, Luke Church, and Thomas Green, written in response to Jeannette Wing’s highly influential Computational Thinking. Wing argues, amongst other things, that abstraction is a key feature of the set of techniques that computer scientists use when thinking about problems, and that people working in other disciplines could profitably make use of some of the abstraction tools developed by computer scientists. Blackwell et al. disagree with Wing’s emphasis on abstraction, noting that it can lead to system designs that de-emphasise and dehumanise users in favour of simple and tractable models designed for programmers. They also argue that abstraction can also lead to excessive literalism, conflation of the goals of a system with the goal of “the perfect abstraction”, and mathematical abstraction as a tool for theoreticians to hide behind when defending their theories. Admittedly, I put this slide up to get a cheap laugh from their abstract, but I do think the paper is worth reading in its own right.

• The “Pedestrian or Equestrian” sign is from Stanley Park in Vancouver. I went over the equestrian side. The combination of the pine forest visuals and the water dripping from the ceiling in the room where OBT was held made for quite the Vancouverean experience.

• Jean-Yves Girard’s Locus Solum is the paper that introduces Ludics, a logical formalism whose details persist in eluding my understanding. An interesting feature of the paper is the extensive glossary covering a large portion of logic, semantics, proof theory, and computer science in a unique way (Appendix A: A pure waste of paper).

• Barbara Liskov and Stephen Zilles’ Programming with Abstract Data Types was the first paper to really nail down the idea of an abstract data type as a structured thing described through a set of operations, instead of the more negative definition in terms of information hiding. This lead to the design of the language CLU, led by Liskov, and to a great amount of work in algebraic specification. The Power of Abstraction is a excellent and informative talk by Liskov covering the history of how she invented abstract data types.

• Types, Abstraction, and Parametric Polymorphism by John Reynolds is the founding paper of a semantic theory of abstraction, now called parametricity. Christopher Strachey’s original definition of parametricity was informally defined in terms of parametricity polymorphic functions being “uniformly defined” with respect to their type parameter. There are many ways to formalise this notion. We could strictly interpreting it as meaning there is a single implementation, ignoring the type parameter, as is done in PER models that interpret quantification over all types as intersection. Reynolds chooses to interpret parametricity as preservation of relations, generalising the invariance under homomorphism idea from algebra. This is formalised in the Abstraction Theorem which appears in this paper. As he notes, the Abstraction Theorem is closely related to the “fundamental”, or “basic”, lemma of Logical Relations, first used for the lambda-calculus by Gordon Plotkin for proving definability results. I believe the origin of logical relations goes back to Robin Gandy, who used them (or at least logical relations that are equivalence relations) to ensure extensionality in models of calculi with higher-order functions.

• John Harrison’s Without Loss of Generality is a genuinely practical paper for reducing the effort involved in proving geometric theorems in an interactive theorem prover. Harrison takes inspiration from the way that mathematicians reduce problems to simpler ones by exploiting symmetry. The idea being that “without loss of generality” one can consider a special case that soundly represents all of the instances of the general case. The paper presents an extension to the HOL Light theorem prover that pattern matches on goals containing geometric statements and reduces them to simpler goals using symmetry.

• The quote “A rose by any other name would smell as sweet” is from Romeo and Julliet by William Shakespeare. According to Wikipedia, this play about a catastrophic lack of invariance under renaming was written some time between 1591 and 1594.

• Andy Pitts’ work on Nominal Sets is collected in his book Nominal Sets: Names and Symmetry in Computer Science. The quote on the slide is taken from the introductory notes Nominal Techniques. The essence of nominal sets is that everything ought to be invariant under the swapping of names; it is only the relationships between names that matter.

• The reflexive graph model for System F is originally due to Edmund Robinson and Giuseppe Rosolini, who showed that it is possible to take existing denotational models of System F (i.e., typed lambda-calculus with “for all” types) and complete them to a relationally parametric ones by considering reflexive graphs whose sets of nodes and edges are denotations of types in the original model. I used this approach to give a relationally parametric model of System Fomega (i.e., System F plus type-level functions) in Relational Parametricity for Higher Kinds. A similar approach had been used by Ryu Hasegawa in Relational limits in general polymorphism. Neil Ghani, Patricia Johann, and myself used the reflexive graph approach to give a relationally parametric model of dependent types in A Relationally Parametric Model of Dependent Type Theory. The model I presented in the talk is essentially the same as the one in that paper, except that the reflexive graphs are presented in “indexed-style”, rather than “display-style”.

• Dimension Types seem quite popular at the moment, with libraries popping up for many different languages that encode dimension types. However, most of these systems concentrate on the computer says “no” aspect. They are only interested in the type system preventing things, and womble on about Mars rockets going missing and so forth, like using a different programming language would have fixed that. Andrew Kennedy’s Relational Parametricity and Units of Measure is much more insightful because it shows how unit-correctness actually yields interesting results: including scale invariance results, type isomorphisms, and indefinability results. This was really the point of my talk: abstraction yields properties.

• Philip Wadler dubbed some of the consequences of type abstraction that arise from Reynolds’ work “Theorems for Free!”, because the theorem is derived from the type instead of inspection of the program, which will often be more complex. This has led to many paper titles that end with “... for free!” when they use parametricity to prove something.

• Distance-indexed types, where two objects are related if they are within a certain distance, are originally from Distance makes the Types Grow Stronger by Jason Reed and Benjamin C. Pierce. The intended application there was to differential privacy, where programs (interpreted as queries on a database), are constrained to have limited dependence on small changes to the input. Roughly speaking, limiting the precise dependence of the output on the exact values input ensures that the privacy of the people whose information is in the database is protected. The Reed-Pierce paper presents a linear type system that treats information leakage as a resource that needs to be conserved. The model I presented in the talk doesn’t mention linearity anywhere at all. However, it can be encoded in the reflexive graph model by treating the Reed-Pierce resource-limited types as types indexed by Dist, and building up the other connectives using the same techniques as the Day-construction models of Bunched Implications.

• Geometric-group indexed types first appeared in Abstraction and Invariance for Algebraically-indexed Types by myself, Patricia Johann, and Andrew Kennedy. They are a generalisation of the unit-indexed types from Andrew’s previous work, but allow for a richer set of transformations that the program can be invariant under. We looked at two other forms of “algebraically-indexed types”: one for information flow, and one for distance indexing. The indefinability results from Andrew’s work carry over to this more general setting too.

• The classical mechanics types, terms, and examples are taken from my paper From Parametricity to Conservation Laws, via Noether’s Theorem. Emmy Noether’s Theorem is a result in the Calculus of Variations that shows that it is possible to derive conserved properties of the stationary solutions of variational problems from continuous symmetries of their actions, and in some cases to go back again. This theorem is very important in physics. Many physical theories, not just in classical mechanics, are described in terms of stationary solutions of variational problems. Noether’s theorem gives a way to deduce properties of solutions without having to explicitly solve the system. In computer science terms, roughly speaking, Noether’s Theorem shows how to derive time-global invariants over runs of a system from time-local invariants of the single-step behaviour of the system (though in Noether’s case, there are no “single-steps” because everything is continuous). My paper showed that it was possible to derive the local symmetries as consequences of free theorems, which can then be plugged into Noether’s theorem. Note that I didn’t show that parametricity implies Noether’s theorem, though the idea doesn’t necessarily seem too outlandish, if one could give a suitable account of continuous change. Noether’s original paper Invariant Variation Problems is available in translation. I found the book Applications of Lie Groups to Differential Equations by Peter Olver extremely helpful in understanding the basic theorem, and its generalisations, which were also proved by Noether. The book Emmy Noether’s Wonderful Theorem gives a readable account of the background and how the theorem is applied in physics applications.

• The non-example of Higher Order Abstract Syntax is from my paper Syntax for Free: Representing Syntax with Binding using Parametricity, which proved that the (denotation of the) type forall a. ((a → a) → a) → (a → a → a) → a is isomorphic to the set of closed lambda-terms. This result appears to require Kripke-indexed relations, which are not included in the simple reflexive graph model I used in the talk. After my talk, Ambrus Kaposi mentioned some ideas to me of how to incorporate Kripke-indexed relations, which I need to follow up.

• The final section of the talk reported on unpublished work in progress on internalising relational parametricity into the type theory. Using the reflexive graph model at a meta-theoretical level is all very well, but it would be extremely useful to be able to prove invariance results internally, just as one can prove equalities between programs internally in dependent type theories. The approach I presented here is based on the observation that “relatedness” is sort of like a weakened version of equality in Martin-Löf type theory (MLTT). (For simplicity I only considered MLTT with equality reflection.) The resulting system is something like Ambrus Kaposi and Thorsten Altenkirch’s Cubical Type Theory, but differs in how it considers equality within in the universe U of small types. Jean-Phillipe Bernardy, Thierry Coquand, and Guilhem Moulin have published a syntax and model for internalised parametricity. Their system has unary, but higher-dimensional, relations, and does not (as far as I understand) have an explicit relationship with equality.

After the talk there were a few questions, which were written down on 5x3 index cards and read out by the session chair. This style of questions is an innovation by Lindsey for OBT to try to encourage people who wouldn’t normally ask questions to ask, and to share time more equally between questions. My impression was that possibly more questions were asked than I would have normally expected. Also, I got to keep the cards with the questions on:

The questions, and my answers, are listed below. These answers are with the benefit of hindsight and a long plane journey to ruminate on “what I should have said”, so they aren’t exactly what I said at the time.

1. How is that related to homotopy type theory/univalence? This is an especially natural question given the formal similarities between the higher-dimensional models for both. I used to think that relationally parametric type theory would be a “baby” version of univalent type theory, where the composable, reversible paths between objects are replaced by a weaker notion of relatedness. However, I now think that relational parametricity and homotopy type theory are orthogonal. Relational Parametricity is agnostic with respect to the notion of equality it uses, and so it is possible to speak about relationally parametric (extensional type theory | type theory with equality reflection | intensional type theory | observational type theory | univalent type theory). However, thinking a bit more, it might be possible that Homotopy Type Theory might be a sub-system of relationally parametric type theory, where relatedness just so happens to be slightly richer.

2. What ever came out of John Harrison’s “WLOG” work? Any useful tools for automatic theorem proving? I don’t know about tools for automatic theorem proving, though I think that it would be interesting (I vaguely remember that constraint solving systems often involve the use of symmetry to cut down the search space; the name Karen Petrie springs to mind). Harrison’s original work is now part of the HOL light theorem prover, in the Multivariate library.

3. Have you looked at Lorentz invariance? This is in reference to how all the examples I showed of mechanics systems were invariant under Galliean invariance, which doesn’t account for the effects of special relativity. Lorentz invariance does account for special relativity. I haven’t looked at Lorentz invariance explicitly, but I think that it can be handled by the system I presented.

4. Where can I get your slides and/or papers you used as examples? This page.

5. How about Calculus? At the time I interpreted this question as being about the special type constructor C^\infty I used to internalise smooth functions for the purposes of classical mechanics models, and I muttered something about Synthetic Differential Geometry. Looking back, I think it probable that the questioner was actually asking about the relationship between the “theory of change” model I talked about here, and differential calculus as a theory of continuous change. I think that this is a really interesting question, which might have a lot to say about incremental computation, bidirectional computation and reversible computation. The paper A theory of changes for higher-order languages — incrementalizing λ-calculi by static differentiation gives an account of a static “differentiation” process for lambda-calculus terms for the purposes of doing incremental computation. Gabriel Scherer noted a similarity between that work and relational parametricity, which I wrote a blog post about.