Daily ICFP

Several Tweagers all agreed to gather notes here about our ICFP (International Conference on Functional Programming) experiences.

Other posts in this series:

• ICFP - Day 0
• ICFP - Day 2
• ICFP - Day 3
• ICFP - Day 4
• ICFP - Day 5

Day 1 - Monday

These notes follow Noon, Arnaud, and Richard through their day at ICFP, roughly in order.

Richard — Calculating Dependently-Typed Compilers (Functional Pearl)

Started my day at 6:30am in order to attend the Q&A for Calculating Dependently-Typed Compilers (Functional Pearl), by Mitchell Pickard and Graham Hutton, of the University of Nottingham. (I watched the video itself last night.) This is a very cool paper about a technique for deriving a proved-correct compiler by construction. The main example in the talk was about compiling a simple expression language to a stack machine. The correctness condition is that exec (compile e) s = eval e : s, where e is the expression under consideration, s is a call stack, and : pushes a new item onto the call stack. Starting with this equation, we can consider different forms of e and then use the correctness requirement to derive what the stack language (the elements stored in s) needs to be, and how compile should work.

I really enjoyed the talk (though I haven’t yet gone back to the paper). It’s presented simply and convincingly. And I think the idea is really cool, showing the power of dependent types. (Both the source language and the target stack language are intrinsically typed, requiring the compilation to be dependently typed.) Do watch the talk: it’s accessible and educational.

The Q&A was a pleasant chat among like-minded folks; all seemed to generally support the line of research and appreciated the results. A nice nugget of knowledge that came out was the importance of the interactive features of Agda in order to create this solution. I asked whether an implementation in Haskell would be possible; Mitchell thought it probably would be. But I already know that the act of composing the solution in Haskell would be much more difficult than in Agda because Haskell is still catching up when it comes to editor integration. Yet another reason to support HLS!

Richard — Watched a few videos of talks I’m interested in. I don’t think I’ll list all such videos, lest anyone out there get offended by my choices. :) I really miss the in-person interactions of an in-person conference, but being able to watch videos at my leisure is really nice — especially when I can enable captions, run the videos at 1.25x or 1.5x, and rewind to rewatch the hard parts.

Richard — The Q&A sessions are technically available in either time band (the ICFP conference itself happens both 3am-10am in my time zone, US East, and also 3pm-10pm), but some authors are available only for one of the Q&A sessions. This is frustrating, because it means I miss some great stuff in the middle of my night. I wonder if it would be possible for the active Q&A session (some authors make it to both!) to be recorded and viewable later — perhaps just during the conference (in order to incentivize interaction and protect some degree of the privacy of the conversations).

Richard — The program at icfp21.sigplan.org allows users to select what events they are attending by starring them. Then, there is a way to make a subscribable calendar with those events (and it stays updated!). I’ve subscribed my usual Google calendar to this ICFP calendar, and it’s making time management so much easier! The only problem is that the main-time-band events share their state with the mirrored-time-band events, so things appear on my calendar twice. This is imperfect, but still really helpful.

Noon — Q&A: Algebras for Weighted Search

• Unfortunately missed most of the talk; but caught the Q&A.
• Looks like this was quite popular and people were very excited about it!
• As far as I understand it, people were excited to see weighted search formulated as a Monad.
• One interesting comment that Oisín mentioned in the talk was by swapping the order of … (something I can’t remember) you get a parser instead of a duplicate remover. This sounded very interesting to me, so I’d be curious to know what it means!
• Some comments about weighted optimisation!

Noon — Fun, Funky, Functional: The Pursuit of Better User Interfaces for Programming

• Learned about the combined field of PL =<< HCI
• Nice talk; I missed a lot of it, but I’ll go back and take a look!
• Love the idea of more structured editing and closing the gap between drawing by programming and other forms of drawing.

Richard — Watched the same keynote as Noon, above. It was delivered by Ravi Chugh. Very nicely done, introducing a wide array of different papers on the intersection of PL (programming languages) and HCI (human-computer interaction). The highlight of the talk was a tool made by Ravi and his students that supports advanced editing techniques:

• The language demonstrated describes a diagram, and the diagram appears to the right of the code. But you can edit the diagram by clicking and dragging, just like a drawing program, and demonstrated program updates the code. Very cool!

• This software also supports block-editing the code itself. That is, instead of thinking about characters and lines, you can think about programming constructs, like a particular variable binding or if-expression. Moving pieces around moves whole semantically-relevant pieces, not just a few characters. I’ve been wanting this for years.

• A further example included a program that produces an HTML version of a table. But you could edit the rendered table, and the HTML-generating code would update accordingly! You could even edit the DOM of the rendered HTML and the code would update. Amazing.

I can’t wait for the techniques demonstrated in this keynote become standard and widespread. We will all be better off when that happens.

Noon — Propositions-as-Types and Shared State

• Curious to know what this connection will be.
• Interested to learn the Linear logic <-> Session types connection.
• Got a little bit away from me technically as it went on; but surely quite interesting!

Noon — Calculating Dependently-Typed Compilers

• We want to formally verify a compiler;
• What if you specify the compiler and then derive an implementation? (Instead of programming it and then verifying you did it right.)
• This talk is about doing this!
• Cool explanation of using dependent types to define a language that doesn’t allow illegally-typed expressions.
• Very cool example of deriving the compile function! Felt a little bit magical?
• Really motivated me to read the paper!

Noon — Networking

• To end my day I had a really nice table-chat with a person from the community whose work I really love! They were so friendly and nice and it was a great conversation :) Left me feeling very good and energised for tomorrow!

Richard — I attended two PLTeas today. These are social sessions where each participant is randomly matched with several others to talk for 15 minutes. Over the course of the day, I participated in 4 such groupings. It’s all a little artificial, but random encounters are really the lifeblood of conferences: it’s these encounters that lead to future collaborations. (I have several papers that came about only because of random encounters at conferences.) A few highlights include chatting with my friend Joachim Breitner about pattern-matching syntax in Haskell (hope we didn’t bore the others!), telling a graduating undergrad to choose Penn for graduate school (I had a great experience there), and meeting someone (I didn’t ask for their permission to include their name here, so I won’t) working on code synthesis in the Haskell Language Server (HLS). This last project is about adding a feature to HLS (which powers editor integration across several editors via the Language Server Protocol) to figure out from context what code to insert next. If done right, this could be a game-changer for Haskell programmers. I’ve encouraged this young researcher to get in further touch so I can use whatever powers I have to support this important work.

(Fun fact: Joachim and I first met as roommates at ICFP’14. But this was after we co-authored a paper together! Joachim completed an internship at Microsoft with Simon Peyton Jones a little while after I did. Then, Simon, Joachim, Stephanie Weirich, and I wrote a paper. Joachim and I agreed to room together at the conference, and we thus first met in person when he arrived at our room. The majority of my papers have been written remotely with co-authors, even way before the pandemic.)

Arnaud — Contextual Modal Types for Algebraic Effects and Handlers

• This is about using the technology of contextual modal type theory to give type to algebraic effects and handlers.
• It differs from most treatment of effect type systems in that this lets the effects be represented by a comonad of sort, rather than a monad. Effectful arrows have type C a -> b for some C. I think this is sometimes referred as “capabilities”. This reminds me of Recovering purity with comonads and capabilities (though I don’t really understand this article yet). I’m really keen to understand this approach better.

Arnaud — Generalized Evidence Passing for Effect Handlers: Efficient Compilation of Effect Handlers to C

• This is about a compilation technique for algebraic effects and handlers.
• The talk was very enticing, but I didn’t really learn much from it. The compilation is performed in a series of passes, the first of which is conversion to multiple-prompt delimited continuation; which already seems to contain some magic. The result looks quite impressive, though. I’ll have to read the paper.

Richard — I played the Untitled PL Card Game with four other attendees. This social event has participants play an Apples-to-Apples-like game, but the cards are based on PL concepts. You can play online, too. This was fun, but I wish there was more opportunity to meet my fellow players.

Richard — I attended the Ask Me Anything on Climate Change with Benjamin Pierce. Well, it was supposed to be Benjamin, but he was called away with a family emergency (I very much hope everything is OK!), so Mike Hicks stepped in instead. Kudos to Mike for handling this surprise appearance so graciously. While climate change is not directly related to functional programming, it is an existential threat to the human race, so if we don’t work on climate change, too, functional programming will surely suffer. The topics were naturally quite interesting. We talked about the future of conferences, as there was talk of virtual conferences even before the pandemic. The sense I got from Mike is that we would like to get back to in-person conferences when possible, despite their impact on the climate, possibly mixed in with some virtual ones.