I had a great time at PEPM and POPL in Denver! My plan was to write about it on getting home, but missed my connection at LAX (apparently, when lightning hits a plane its a big deal) so spent 20 hours in the terminal waiting for the next one, and am only now recovering.
My talk at PEPM was well received. No-one objected "But that contradicts the Church-Turing Thesis!" Instead, everyone was listening, trying to integrate this new worldview. What more could I ask for?
In the hallway track, I was a demon, waiting to be summonsed. I would chat, ask about their work, but whenever someone said " And what are you working on?" I would show them the frontispiece of my book, that displays the self-evaluator, and then they were hooked, most going straight to our splash page. My favourite reaction was "Each of those dots must be an abstraction, right; what are they?" "No," I proudly replied "they're just the nodes of a tree; there are only 509 of them". It was very satisfying.
At a deeper level, I enjoyed technical discussions about combinators, logic and compiler construction. Someone asked me about a paper I wrote twenty years ago! I had to look it up online, reminding me of the old professor who spluttered at the young me "I've forgotten more than you'll ever know!"
Three discussions suggested possible future directions for tree calculus. First, I got to shake hands with Johannes Bader for the first time, after Zooming for over a year. We wondered "What can we do face-to-face that we can't do online?" "I don't know" I said "but at least I can see your profile!" I had been thinking about how to internalise the type system, so that typed terms of tree calculus are embedded in the untyped calculus. He suggested that we look at gradual typing, where type inference and checking that cannot be handled statically is delayed until runtime.
Second, Vikraman Choudury gave an interesting talk on co-lambda-abstractions, which, like lambda-mu-calculus, provide support for classical logic and control operators. When I asked if he had a combinatorial account of the co-lambdas, he replied "Not yet, but I want one." It seems that many of the side conditions on the reduction rules can be expressed using intensional combinators. For example, that some expressions are values can be captured by an operator V that is not expressble as a combination of S, K and I. The downside is that this willl not fit into his larger framework, using category theory.
Third, were some new ideas triggered by discussion with Johannes. Since
programs now have normal forms, all of the parametric polymorphism of
System F can be captured by tree types. That is, for trivial reasons,
all program have principal types! The challenge,
then is to decide when programs have function types, so that type
inference amounts to the following problem. Given a program of type
My patter was well-honed by the end of the week. When our plane was diverted from LAX to Ontario, California, the accountant next to me asked "so what are you working on?" Next thing I know, not only had he downloaded the book, but also the software developer in the row ahead, and some dude in the row behind!