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

Day 2 - Tuesday

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

Richard — Watched the video for Symbolic and Automatic Differentiation of Languages, by Conal Elliott. Conal’s papers and talks are always very insightful — because they are always very simple. Conal has a remarkable knack for taking problems that seem complex and reducing them to their essence — often, a simple compositional language. This work fits very much in this vein, describing how we can derive parsers for a language straight from its definition. The talk is gentle and mind-blowing all at the same time.

Noon — Higher-Order Probabilistic Adversarial Computations

• Wondering if this is related to Adversarial Machine Learning.
• I think maybe; but it seems to be focused on categorising types of adversaries via type theory?
• It got quite technical for me quite quickly, but it’s at least interesting to see a totally different take on this concept!

Noon — How to Evaluate Blame for Gradual Types

• Interested in this because I was curious about Gradual Types.
• “The Rational Programmer” - Seems cute/interesting; but also maybe a bit fraught because I think comparing the idea to the usage in economics is a mistake, as I believe it’s widely considered to be one of the biggest mistakes in economics to assume rational agents!

Noon — Symbolic and Automatic Differentiation of Languages

• Always relaxing to listen to Conal talk.
• I learned that the derivatives Conal talks about initially are these: Brzozowski derivative
• He then relates this to differential calculus!
• He then describes automatic and symbolic differentiation in this setting, and using this, builds language derivatives.
• The conclusion is that these two things have the same structure with different interpretations. Very cool.

Richard — I attended both Q&A sessions for my own paper, An Existential Crisis Resolved: Type Inference for First-Class Existential Types. The first session went for 30 minutes, and the second session went for an hour. This is a wonderful aspect of the online format: we have as much time as we want to discuss a paper. There was considerable interest in an implementation. A few other tidbits:

• The approach to existential types in the paper requires including expressions in types. In order to compute type equality, then, we must define what expressions are equal to one another. A simple starting point for an expression equivalence relation is to use syntactic equality. Thus, 1 + 1 would equal 1 + 1, but it wouldn’t equal 2. We can get cleverer over time. However, there is immediately a problem: GHC might optimize an expression. For example, it might change let x = 5 in 10 to be just 10 (x was unused). But these expressions are not considered equal in types, so the optimization has the possibility of destroying the well-typedness of an expression. The solution is likely that we will have to have Core coercions (a coercion is essentially a little expression that says that two certain types are equal) that witness the correctness of optimization passes.

• Rust has a feature called impl traits (I think) that are essentially existentials. They seem strictly less powerful than what we’ve proposed in this paper, but I need to learn more about what Rust does.

Noon — How to design co-programs

• Where do programs come from? Programs come from data structure.
• Mostly we talk about input data structure; but should also talk about output data structure!
• If you use this idea, you get a different algorithm for the sorting example.
• Overall I like the idea; I feel like there’s probably more fruit to be gained from it.

Noon — PLTea

• Chat 1 - Very nice chat hearing about bidirectional programs.
• Chat 2 - Had a nice chat about CLaSH and formal verification.

Noon — SIGPLAN CARES

• Very nice chat about feeling included/excluded at a conference.
• Was very well moderated by Simon Peyton-Jones; left me feeling very hopeful.

Noon — Leibniz equality is isomorphic to Martin-Löf identity

• Looked interesting; didn’t follow it all.
• My main conclusion: I need to learn more Agda.

Noon — PLTea #2

• Less good; conversations were a bit dominated by one or two people.

Noon — Building PL-Powered Systems for Humans

• Describing interesting UIs and programming synthesis in evaluating MOOC programming tasks.
• Nice discussion around how to let the users control the search space.
• Interesting paper to look into: Assuage.
• Interesting keynote idea to interview another researcher during your talk!
• Mostly enjoyed the interview, but sometimes got a bit lost when there wasn’t any text/graphics to ground the conversation.

Arnaud — There have been several discussions on quantitative evaluation of programming-language tools. The first was in How to Evaluate Blame for Gradual Types. It isn’t obvious from the title, but this paper is about building a model of the programming activity in order to be able to quantify the effect of error messages in the debugging process. The second such discussion was during the keynote (see previous paragraph) where the difficulty of quantifying effects in programming language was raised and Elena Glassman said that she favoured qualitative evaluation. This is a very important discussion, programming languages is a field where tools and technologies are rarely evaluated for their real-world relevance rather than their theoretical elegance. I contend that we don’t know how to evaluate programming languages yet, so it’s always exciting to see people make steps in this direction.

Noon — Dinner

• Got a nice intro to the ‘Granule’ programming language from Dominic Orchard and Jack Hughes.
• Learned that there is such a thing as types indexed by continuous variables!

Richard — Enjoyed the trivia night, quickly becoming a SIGPLAN conference tradition, hosted by José Calderón and Paulette Koronkevich. We formed a team rather randomly at one of the conference tables and then proceeded to win. It turns out that recognizing a small detail of a Hieronymus Bosch painting can come in handy!

(Richard attended less of ICFP than usual today, due to the need to execute travel plans that had been delayed by Hurricane/Tropical Storm Henri over the weekend. More action tomorrow and future days!)