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 1
• ICFP - Day 2
• ICFP - Day 4
• ICFP - Day 5

Day 3 - Wednesday

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

Noon — On Continuation-Passing Transformations and Expected Cost Analysis

• Discussion of the difficulty of costing probabilistic algorithms (i.e. you don’t know what it will do.)
• Turns out using continuations makes it a bit easier to reason about (I didn’t quite follow the trick that makes it true),
• But, it gives a way to think compute average-cost analysis, which seems pretty useful!

Noon — Automatic Amortized Resource Analysis with the Quantum Physicist’s Method

• Quantum physics? I’m interested.
• “This talk doesn’t involve any quantum physics at all”. Oh well.
• Idea is to think in terms of an “energy bank” and how much your program will need over time.
• Can use this to think about time, and space.
• Analogy to Alice and Bob having some fixed money and some fixed task (buying candy).
• Their idea is to take a (kind-of) super-position of all kinds of ways of splitting up resources (money).
• This helps with some technical detail of the standard amortized resource approaches (I didn’t quite get why.)
• Really enjoyable.
• Definitely curious to take a look at this paper!

Arnaud — GhostCell: Separating Permissions from Data in Rust

This talk addresses an important problem in the Rust programming language: how does one write a structure with pointer sharing in Rust (typically: a doubly-linked list). Until now, it was either using unsafe features (danger!) or using a Cell type (slow and icky). In this talk a new safe and efficient approach is proposed. Which would be remarkable already. But the authors also proved their approach safe in Coq, as part of the RustBelt project. Impressive.

Noon — Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course

• In learning about proofs and correctness, how to get to the good stuff faster?
• Answer: By using features of the host/meta language.
• I’m personally unconvinced (not that I’m an expert); it seems worse to me to have implicit implementation details that students don’t quite understand.
• But I do understand the desire to speed up getting to the good parts!
• And maybe this is a good technique when not teaching? Just for your own experimenting? Probably.

Richard — Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl), by Adam Chlipala

This was a nice talk about a technique Adam uses in his course on formal verification of programming languages using the Coq proof assistant. His goal is to take undergraduates, in a single semester, from no experience with Coq to being able to do non-trivial proofs on programming languages with e.g. effects or concurrency. The talk describes the use of mixed embeddings in his formalization of effectful languages: use a deep embedding of the command language but a shallow embedding of expressions. That is, the command structure (e.g. write to memory, goto, etc.) is expressed using a datatype, but expressions (that evaluate to some value) are just written in Coq’s native syntax. This allows for e.g. proofs about commands without needing to worry at all about expressions (and variable binding!).

I had previously viewed shallow embeddings as a bit of a parlor trick: if you’re describing a programming language that has behavior very similar to the one you’re writing in, you can skip some of the description. But the whole trick depends on a close correspondence between the object language (that is, the one you’re implementing) and the host language (that is, the one you’re writing in). Yet this presentation made me realize that shallow embeddings are considerably cheaper than deep ones — in the cases when the trick works. Cheap and cheerful is sometimes indeed better than fully general — especially if it allows undergrads to access advanced material so quickly.

Richard — Catala: A Programming Language for the Law, by Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko

I was so excited when I saw this paper in the program, as I always wondered how we could take legal statutes and formalize them. This paper attempts this for the tax code, where the rules are very algorithmic. (Formalizing, e.g., slander laws seems harder.) The authors worked with lawyers to design a language, Catala, that is a fully expressive functional language while using a syntax easily readable by lawyers (i.e. domain experts). In the act of translating tax statutes into Catala, lawyers frequently discovered new ambiguities in the law. In the Q&A session, we even imagined writing QuickCheck properties over laws. (Example: you would probably want a monotonic tax system, where an increase in gross income never yields a decrease in take-home income. Indeed, Jonathan explained that non-monotonic tax law is actually unconstitutional in France — yet he believes the existing tax law is non-monotonic anyway.)

This talk filled me with optimism at the receptiveness of lawyers to this new technology. The research group is actively seeking new groups to collaborate with.

Noon — Catala: A Programming Language for the Law

• One of the few (only?) talk about a paper that I had actually read before the conference!
• I’ve been fascinated with tax calculations since reading the various Piketty books.
• Motivation: Converting law into code is hard and sometimes subjective.
• IRS income tax program implemented in assembly from the 60s!
• Idea: Mix law and code together (as both are necessary for determining correctness.)
• Interesting fact: The language was at least partly co-designed by lawyers who helped pick the keywords,
• Quite liked this idea and the talk!

Noon — PLTea

• Some interesting conversations.

Noon — Programming Contest Report

• An astonishing amount of work goes into this.
• Richard: Yes, it does! I’m amazed every year by the generosity of the organizers of this contest in planning and executing it.

Richard — Program Chair Report

Many conferences include a report from the program chair, including information about the number of submissions, the selection process, and how many papers got accepted. Interestingly, the pandemic has had only a small effect on the number of submissions to ICFP, despite anecdotal evidence I’ve heard that submissions are down in other scientific fields. (Plausible theories: less time for focused thought during school shutdowns; less ability to focus due to anxiety in the news; less research time for faculty who teach due to the need to redesign courses to work well in a remote format.) Maybe this means that interest in ICFP is actually going up, cancelling out the negative effect of the pandemic. Huge thanks to Ron Garcia for chairing the program committee and to Sukyoung Ryu for chairing the conference!

Noon — Industrial Reception

• Had a really enjoyable chat with the various visitors to the Tweag table. Thanks everyone for stopping by!

Richard — I second that comment about the Industrial Reception. We had a very nice crew of people interested both in Tweag and in research ideas. Among more Tweag-centric discussions, I had a small but fascinating conversation about which is more fundamental: math or computer science. I’ve felt for a few years that computer science is just applied mathematics, but the way in which dependent types can describe fundamental mathematical concepts makes me wonder sometimes whether I’ve gotten the relationship backwards. As a case in point, I wondered aloud with a visitor to the Tweag table (I did not ask permission for posting their name) about how to re-express the fundamental definitions about differential calculus on manifolds using dependent types. This sounds very, very fun, but I worry it will be too distracting from “real” work (like continuing to improve GHC)! We’ll see whether I can fit this in.

Richard — How to design co-programs, by Jeremy Gibbons

This presentation gives a wonderfully elegant, simple approach to taking the first steps toward writing functions. There are no advanced concepts (don’t trip over the word “corecursion”!) and the video shows how typed functional programming is such an aide to reasoning about how to write programs.

Richard — Leibniz equality is isomorphic to Martin-Löf identity, parametrically, by Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler (presented by Phil)

This paper presents a proof that Leibniz equality and Martin-Löf equality are isomorphic. The talk gives very nice introductions to both of these concepts, so I am going to skip that here. As the talk concedes, the isomorphism between these two notions of equality is not necessarily all that useful, but it’s nice to know how the proof can be done, and it’s interesting that the proof requires an assumption of parametricity. The paper (and presentation!) are both literate Agda, meaning that rendering the LaTeX or slides also type-checks the technical content, giving greater assurance of the result.

This talk is a nice peek into the power of dependent types to write formal proofs!

Richard — If other attendees at ICFP are reading this, please spend more time in the lounge! A few times I cruised through the lounge looking for new folks to meet and left disappointed. Somehow, last year’s ICFP did not suffer from this problem: I had many great out-of-band conversations. Maybe the novelty of online conferences has worn off? I’ve still had a number of fine conversations this year, but it definitely feels a step down from last year.