Why did I go to ICFP 2017

In August, I was reflecting on why I even go to conferences. I set forth an experiment to judge my own hypothesis about why I go to ICFP. ICFP 2017 met both criteria: I sat through a talk that was not on my list of expected interesting talks, and I had one unexpected interaction and learned something new (and got a new research idea out of it).

To refresh your memory, my hypothesis was:

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.

I analyzed my past notes and made the following prediction to test my hypotheiss.

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.

I have been analyzing my notes from ICFP 2017 and conclude that both predictions came true.

An unexpected talk and a new view of Haskell

I was sitting in the Haskell Symposium on Friday, a day I marked as having nothing that looked particularly interesting. It was an afternoon session and I was a bit sleepy. The first talk of the session was Elaboration on Functional Dependency, and it jolted me awake.

I wasn’t interested in the particular problem this worked solved. As far as I can tell from my notes, it developed a elaboration and inference algorithm for some neat feature of Haskell’s type system. Sounds like fine work.

What interested me about this talk was a deeper insight about Haskell’s design that had not occurred to me before. For the first time, I realized that Haskell is implemented essentially as a series of type-preserving compilers. The source language is Haskell, plus a bunch of language extensions that are bolted on by pragmas. Each of these extensions, and most of Haskell itself, it essentially (although not implemented this way) a bunch of macros that compile down to Core, which is little more than System F. I should have known all this, but it had never clicked before.

What’s more, these type-preserving compilers appear to be related to my own work. In this talk, it appeared that their elaboration uses use strong existential pairs to implement functional dependency in the core language. The translation struck me as similar to work on module systems for ML, which some of my recent work on type-preserving closure conversion for CIC is based. I haven’t figured out how this functional dependency paper is related to my own work, but it is on my todo list to find out.

Had I not been at ICFP, I would have never looked at this talk. I like Haskell in theory, but I don’t follow it very closely. The title “Elaboration on Functional Dependency” is meaningless to me, and the abstract describes details of Haskell’s implementation that I don’t care about. And yet, I saw the talk, and I got a lot out of it.

An unexpected chat and a CPS translation

I ran into Neel Krishnaswami during one of the breaks, and he started scribbling an alternative to the target language of the type-preserving CPS translation I recently developed with Nick Rioux, Youyou Cong, and Amal Ahmed. One annoying fact of the work is that the target language is a non-standard calculus with two additional type rules required to recover type-preservation. Neel’s idea was an attempt to avoid these two additional rules. We discussed the idea, and I rejected it. I had investigated a similar idea before, and found I couldn’t make a CPS translation work. Still, I took the scrap of paper Neel had scribbled on and left it in my bag.

That note has been sitting on my desk for the past 2 months. I keep coming back to it. If I could make it work, it would be such an improvement—a much more elegant target language.

Last week, as I was getting ready to go to dinner, I glanced at it again. I had been talking about the CPS work all week, and had a similar conversation with someone—these two additional typing rules are a bit inelegant and it would be nice to avoid them. This time, I’d found a new way to express exactly why the translation wouldn’t work. As I was leaving for dinner, I glanced at the bit of paper and started replying my new argument in my head. But found a new direction: what if I just tweak the translation like so?

Now, at the bottom of that scrap of paper, I have a new CPS type translation. I have no idea if it will work, but I haven’t found a counterexample yet.

If I had not been at ICFP, I wouldn’t have had this random conversation with Neel, and wouldn’t have had this scrap of paper sitting on my desk glaring at me for 2 months. Now, I have an interesting new translation to study.