(crossposted from williamjbowman.com)

I am William J. Bowman, a sixth year Ph.D. student at Northeastern University. I am once more attending, contributing to, and volunteering at ICFP. But why do I do that?

As I prepare for ICFP 2017, I asked my self “why do I go to ICFP?”. I found the question harder to answer than I expected. Of course, as a scientist, when I come across a difficult question I know exactly what to do. So let us form a hypothesis for why I attend ICFP.

I could say that I go to see the talks. But actually I skip many talks, and I’ve written before that I hate most conference talks, although I also reconsidered that point. Besides, the talks are recorded by put online. This hypothesis implies I wouldn’t go to conferences, which I do.

Perhaps I go to talk to people. But actually I talk to few people out of the massive number of ICFP attendees. The few people I do talk to are either presenters, people who engage me after I present something, or people I already know and could talk to elsewhere. If my goal were to talk to these people, I could do so by emailing or calling people after watching their recorded talks, which I do not do.

Perhaps I go to see the interesting locales at which ICFP is held, and do sight-seeing. Of course, this would be a bad reason to attend ICFP, so let us hope this hypothesis proves to be false. If this hypothesis were true, I should spend most of ICFP sight-seeing. I should also not attend ICFP if there is no sight-seeing to be done. But mostly I spend it in crammed lecture halls starring at screens full of math and code. I go back to my hotel exhausted, and promptly fly home without seeing much of the locale at all. I have even attended ICFP when it was held in Boston, where I live, with no sight-seeing to be done. Phew.

The most plausible idea I’ve come to is the following.

Hypothesis: I go to ICFP because being at ICFP not only helps me keep up-to-date on the current research, but also gives me unexpected and unpredictable benefits to my research.

That is, while I could watch the talks online, by being at ICFP I sit through random talks that I would not know to look for or whose title and abstract don’t seem related to my research interests. While I could email presenters, by being at ICFP I end up in conversations with random people, presenters or not, that I could not find to contact if I tried. Furthermore, these random and unplannable experiences expose me to new ideas and perspectives that are beneficial to my research.

Analysis of data from ICFP 2016: Unifiers as Equivalences

Last ICFP I took extensive notes, so we can analyze these notes to seek unexpected experiences that turned out to be useful. If such experiences exist, they support my hypothesis. Spoiler alert: such experience exists. I will share one.

I sat through the talk Unifiers as Equivalences primarily because I wanted to see the talk after it, Elaborator Reflection: Extending Idris in Idris. The latter talk is directly related to my research interests; see Cur. However, I do not like coming in mid-session because it’s difficult to predict when to enter so as not to miss anything but also not interrupt anything. So I sat through the first talk too.

When I looked at the program schedule, Unifiers as Equivalences did not particularly interest me. To me, unification was useful in practice, but uninteresting. It seemed to be an ad-hoc method of making things easier, with no principle behind it to guide design decisions, nor any recourse to figure out why something I expect to happen didn’t or vice versa. The abstract mentioned something about Agda’s pattern matching, which also did not interest me, and neither did Agda.

As the talk went on I found both the problem and the solution interesting. The speaker started by introducing the problem: how do we make unification that can be verified; how do we make unification that is not purely syntactic, and that is agnostic to the core type theory? The solution, to make unifiers produce evidence in the form of equivalences, was interesting and seems widely applicable. Suddenly a unifier had a principle behind it: discover and produce equivalence constraints. I could now reason about unifiers.

This talk was unexpectedly interesting, but also turned out to be useful in my own research. I’m working on a type-preserving CPS translation of the Calculus of Constructions. At the end of the current draft, we consider how to extend the CPS translation to include dependent elimination of sums, because this is known to be impossible in general. We found we need additional equivalences constraints in order to type check the translated terms, but it was not obvious how to justify introducing these equivalences. However, these equivalences are essentially the same idea as proof-relevant unifiers: when we do dependent elimination, we discover a new equivalence constraint. Therefore we should be able to build on Unifiers as Equivalences to justify introducing the equivalences we require. Of course, this is speculation future work, but having seen this unexpected talk gave me a promising research avenue to explore.

Prediction and Planned Experiment: ICFP 2017

The next step is to make a prediction based on the hypothesis. I will post a follow up with an analysis of my observations after ICFP 2017.

I predict that I will sit through at least one talk that is unexpectedly interesting and useful to my research. Further, I predict I will have at least one unexpected interaction with a fellow researcher in which I learn something new or learn a new perspective on something I know. This interaction will not be with the authors or presenters of any of the talks I expect to find interesting. Below I briefly list of the talks I expect to find interesting and those I expect to sit through.

• Sunday, mostly sitting through HOPE 2017
  1. Higher-order Programming is an Effect
  2. A monadic solution to the Cartwright-Felleisen-Wadler conjecture
  3. Cogent⇑: giving systems engineers a stepping stone
  4. Only Control Effects and Dependent Types
  5. Logical Relations for Algebraic Effects
  6. Recalling a Witness
• Monday, mostly sitting through ICFP 2017
  1. Compositional Creativity
  2. Super 8 Languages for Making Movies
  3. A unified Approach to Solving Seven Programming Problems
  4. Relating System F and λ2: A Case Study in Coq, Abella and Beluga
  5. Abstracting Definitional Interpreters
  6. Effect-Driven QuickChecking of Compilers
• Tuesday, mostly sitting through ICFP 2017
  1. Verified Low-Level Programming Embedded in F*
  2. Verifying Efficient Function Calls in CakeML
  3. Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
  4. Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
  5. Compiling to Categories
• Wednesday, mostly sitting through ICFP 2017
  1. A Specification for Dependent Types in Haskell
  2. Parametric Quantifiers for Dependent Type Theory
  3. Normalization by Evaluation for Sized Dependent Types
  4. A Metaprogramming Framework for Formal Verification
  5. Inferring Scope through Syntactic Sugar
• Thursday, alternating between ML and Haskell 2017
  1. State machines all the way down
  2. First-class subtypes
  3. VOCAL – a verified OCAml Library
  4. Using Coq to Write Fast and Correct Haskell
• Friday, rotating. Nothing stands out.
• Saturday, mostly sitting in FARM 2017
  1. Interfacing OCaml and Rust: picking the right tool for the job
  2. Modelling the Way Mathematics Is Actually Done
  3. Demo — Octopus: A High-Level Fast 3D Animation Language