26th January

Slides and notes for my OBT “Generalising Abstraction” talk

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:

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:

Coloured Index cards with the questions below written on them

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.