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

Day 0 - Sunday

These notes follow Noon and Richard’s ICFP day, roughly in order.

Noon

• This is my first day ever at ICFP! I’m just trying to get the hang of the platform, the topics, what background knowledge I’m expected to have, and how things are presented.

Noon — Higher-order Programming with Effects and Handlers by Jonathan Immanuel Brachthäuser

• First talk I was able to make it to (I slept in…)
• Was still waking up when I started watching it, so missed a few of the motivations and key concepts.
• Based on Effekt (not Effekt).
• Seemed to hinge on function as “second-class” citizens, but I didn’t quite capture what this meant or what was important about it.
• There was a comment that “currying is the enemy of effectful systems”, but I didn’t understand this and unfortunately my internet disconnected precisely at the moment this question was being answered!

Noon — Computational and Contextual Program Differences by Francesco Gavazzo

• I hadn’t intended to attend this talk, but got convinced by accidentally watching the start!
• Was excited about how to think about program differences and it’s relationships to my old love, AI.
• To start with they show you can think about differences as a single number.
• Then, the argument is that maybe it’s nice to have “higher-order” differences, to compare, say, richer programs.
• In the end, this framework can be used to compute a (numeric?) difference between two programs, along with (I think?) a notion of derivatives.
• They show how this composes nicely and give some examples. One that I somewhat followed was the distribution monad (i.e. comparing programs that use probability distributions)
• There was an argument this is useful for effectful programs (but I didn’t totally follow this).
• Overall it seemed quite interesting!
• I was left wondering how it would relate back to program optimisation, and more generally more examples of where it would be useful; i.e. could you use it for program synthesis? I.e. here are two programs that are quite different; let me make an automatic change to get them to be closer together!

Noon — Speed Networking

• Chatted to a few nice people;
• Commiserated with one person over not understanding some parts of earlier talks;
• Forgot I manually muted my microphone and lamented that there was no way to see this on the platform.

Noon — Functional Machine Calculus by Willem Heijltjes

• Quite enjoyed the presentation.
• Didn’t quite comprehend the motivation, but I enjoyed the talk!

Richard

• Attended TyDe talk on Chameleon, a project by Shuai Fu and his advisors Tim Dwyer and Peter Stuckey at Monash University in Melbourne to provide a better user experience for type errors in Haskell. The key is that it doesn’t just make fancier type errors! It uses aspects of a graphical user interface to provide a selection of different type errors. After all, if you say not 'x', the not might be wrong, and the 'x' might be wrong: Chameleon lets you choose which to focus on and provides appropriate type errors. The authors want to expand to more kinds of errors and more IDEs. Sounds like a very cool project!

Richard

• Attended Edsko de Vries’s talk on quadratic behavior within GHC (video), with two primary examples: records with lots of fields and type-level lists. Records with lots of fields generate quadratic amounts of code because each record-selector must do a case-match on the record constructor, which binds a variable for each field. So each selector has size proportional to n (the # of fields), and there are n selectors. Quadratic behavior. Urgh. Type-level lists (example: in heterogeneous lists) have a different problem: they repeat the types in the tail at every cons constructor. Quadratic behavior. Urgh. Edsko has a library that helps eliminate the bad behavior by putting a type-safe interface over internal untyped operations.

  There was some nice discussion after the talk about how to avoid the type-level list problem. Two possibilities: there is a paper Scrap Your Type Applications to fix this — at the cost of considerable complication in Core. Or, we could use let to bind types and thus create sharing (eliminating the quadratic behavior). This let idea seems quite promising to me. I have posted a ticket to the GHC bug tracker to track this idea.

  To avoid the quadratic behavior around records is, in some ways, easier. We just have to modify Core’s case expression not to require a listing of all fields bound by a constructor. This is a change to Core, though, and so we must tread carefully, as Haskell’s type safety rests on the type safety of Core.

Noon — Integrating Agda with SMT Solvers by Wen Kokke

• Based on refinement types for neural networks.
• Wanted to use SMT solvers.
• Real numbers vs. Floating point.
• Very fun quiz about what laws floating-point numbers might follow.
• Very nice discussion about integrating SMT solvers and languages such as Agda.
• Got me excited to keep trying to learn Agda!

Richard

• HIW Keynote by Marten Agren (video) about Standard Chartered’s compiler for Mu, a reinterpretation of Haskell. Standard Chartered has over 5 million lines of Mu code, a strong statement of the usefulness of pure, functional, strongly typed programming. They use Mu, not Haskell, for better interop with C++ and Excel. Interestingly, recursion is disabled by default.

Noon — Speed Networking (again)

• Gave up after being unable to find a match (despite there being several people in the networking; I think it’s a quirk of the platform.)

Richard

• I gave my own talk on generalization in GHC. Should be viewable on YouTube.

Richard

• Sam Derbyshire (my intern at Tweag) gave a talk on the type-checker plugin (video) work he has been doing during the summer.

Noon — FHPNC Table

• I joined the table and heard discussions about intermediate representations and MLIR; learned that apparently some people are thinking of walking UP the MLIR stack to do different kinds of compiling (rather than the normal direction: down).

Richard

• Matthías Páll Gissurarson gave a very well-produced talk on a type-checker plugin that makes Haskell into a dynamically typed language(!) (video). I’m not sure exactly where this will get used, but it’s interesting to see how easy this is to do, and opens up new directions in gradual types research.

Richard

• Simon PJ’s and Ben Gamari’s “State of GHC” talk (video) was a hit, as always. There is lots and lots and lots of innovation in Haskell and GHC in the last year — and the community is getting broader, with more contributors.

Noon — Missed some sessions because of a bug on the ICFP 2021 page.

Noon — Testing Haskell with Mocks (video) by Chris Smith

• Introduces the HMock library.
• Naively googling this library yields some relaxing imagery.
• Surprised by the complexity of building this library.

Richard

• Chris Smith’s talk on HMock — a library supporting testing class interfaces by mocking up their behavior — was interesting. He described a little language of expectations that was compositional and can be used to describe the expected results of tests. I love how Haskellers do this all the time: express their APIs in terms of little languages; these languages are frequently compositional and provide the elemental building blocks for arbitrarily complex solutions.

Richard

• Tweag intern Jeff Young gave a talk (video) summarizing the current state of play of his work on IntMaps and the Uniques in GHC. These IntMaps are used through GHC to track environments, and we have a hunch that cleverer representations of either the mapping structure or of Uniques themselves will improve compile times.

Richard

• Faustin Date presented work on GSOL (video), a tool to check for the confluence of Haskell rewrite rules using second-order logic. He found several potential sources of non-confluence in the rewrite rules in Control.Arrow, but also observed that the rules don’t fire in practice. I chatted with him afterwards about the possibility of applying his idea to type family equations. GHC requires that type family equations are confluent but does so by somewhat brutally limiting their expressiveness. If we had a tool like GSOL, we could perhaps prove the confluence of type family equations in a different way and allow much more liberal rules in these equations. (Indeed, some of this might make Sam’s work on plugins much less needed!)

Noon — Introduction to Mechanized Metatheory by Brigitte Pientka

• Enjoyed this presentation about what is required when proving things about type systems.

Noon — Emotional Machines by Aaron Turon

• I had intended to go to PLTea but I ended up skipping that to watch this talk.
• I really enjoyed this talk; a bit surprisingly (when I read the description I wasn’t certain I’d like it.)
• I really resonated with a lot of the topics that were brought up; and it gave me a lot to think about.

Noon

• That’s where I ended the day. Overall it was quite a lot of talks. I’m glad I ended where I did, on something a bit relaxing. As usual, in a conference like this, I would vote for more breaks :D (and, if at all possible, given the online nature of this conference, if conference snacks could be delivered to all attendee’s houses; I was missing free chocolate muffins and other tidbits to help me focus for so long!)

Richard

• To end the day, I had volunteered to serve as a mentor to PLMW (Programming Language Mentoring Workshop) attendees. I sat with a few other old hands with several newcomers to the field, discussing the shape of the PL field and brainstorming about directions and research ideas. I’ve done this before at PLMW, and it’s always rejuvenating to hear new ideas and to help young researchers take their early steps.