Daily ICFP
Several Tweagers all agreed to gather notes here about our ICFP (International Conference on Functional Programming) experiences.
Other posts in this series:
Day 4 - Thursday
These notes follow Noon and Richard through their day at ICFP, roughly in order. (The talks are not publicly posted at the time of publication of this post, but we expect they will be over the coming weeks.)
Noon — Second to last day of ICFP. I’m becoming sad that it’s going to be over! But that said, I’m really looking forward to today! I feel a bit relaxed as well, because from my timezone (UK) I get a bit of a break in the morning (as I’m starting my day at the Haskell track.)
Chesskell: A Two-Player Game at the Type Level, by Toby Bailey and Michael Gale
Noon
- What if you were taught chess slowly by a compiler?
- Chesskell uses a little bit (a lot) more memory than the Witcher 3.
- Overall a very fun talk about pushing the limits of type-level programming in GHC.
Richard
This was such a fun talk. Chesskell is an implementation of chess such that any illegal move is a type error. You play by typing in a Haskell buffer to append moves to the game.
To be clear: this is not an implementation of a chess game. It’s really only a fun experiment to see how far Haskell’s type system can go. In this sense, this project is a little dangerous: I wouldn’t want, say, a Java programmer to come across Chesskell and think this is how one would implement chess in Haskell! With that out of the way, though, this is indeed really fun. It’s amazing this can be done at all.
The talk focused mostly on limitations in GHC around its evaluation of type families, which is unpredictably slow. We at GHC know this and are working on it (led by Adam Gundry of Well-Typed), but this talk really pointed out all our flaws. It also describes an EDSL (embedded domain-specific language) that struggles with the new simplified subsumption in GHC 9. (See the proposal for a description.) It’s the first example I’ve come across of a program that is anti-simplified-subsumption in a way that cannot be easily repaired.
Express: applications of dynamically typed Haskell expressions, by Rudy Matela
Noon
- Talking about this library
- Very cool library.
- Really cool capability to generate conjectures (equations that are true from testing) from expressions; i.e. learn things such as
xs ++ [] = xs, and other interesting ideas. - Uses this to generalise property-based testing counter-examples.
- Also does function synthesis!
- Overall I loved this talk and the idea and I think the library will only get much more awesome over time!
Richard
I really liked this talk, too. It starts with a simple idea — Haskell’s
Dynamic — and extends it with the ability to track function application and
store abstract variables (that is, an x that is not bound to a value, like
we would see in an algebraic equation). The talk then explores all manner of
applications of this simple idea. The whole approach (simple idea leading to
multifarious applications) is so Haskelly.
Haskell⁻¹: Automatic Function Inversion in Haskell, by Finn Teegen, Kai-Oliver Prott and Niels Bunkenburg.
Noon
- When inverting, how to deal with functions that are not injective? (i.e. no unique inverse)
- Idea: Just allow multiple inverses!
- With the plugin, any function in standard Haskell can be inverted.
- Want a “functional logic” version of Haskell, similar to Prolog.
- Went into a bit more detail about the function inversion process.
- Overall pretty interesting, and gives me more motivation that one day I’d love to investigate how GHC plugins work and what is possible with them!
Richard
This nice talk shows another superpower of GHC: allowing plugins that can manipulate Haskell source — this one, computing inverses of functions.
Why functional programming with linear types matters, by Tweag CEO Mathieu Boespflug
Noon
- My favourite quote: “The Spleen of Reality”
Richard
This talk explores why Tweag is interested in linear types, focusing on two key benefits: extra safety (the example given was that we don’t want our functional program to accidentally duplicate one pizza into two) and extra performance (linear types can be used to ensure resource disposal, and so provides a potential alternative to garbage collection and the costly latency GC can introduce).
The talk also includes an excellent introduction to linear types for anyone who does not know about them.
Design Patterns for Parser Combinators (Functional Pearl), by Jamie Willis and Nicolas Wu
Noon
- Love the code-review talk format!
- https://github.com/j-mie6/design-patterns-for-parser-combinators/issues/3
- https://github.com/j-mie6/design-patterns-for-parser-combinators/pull/6/files
- Can’t be described; you have to watch the talk. Exceptional.
Richard
Amazing talk. Do watch. And, when you do, keep in mind that everything you’re seeing is actually live.
This is one of a series of amazing talks by Nick Wu. I will endeavor to watch the talk of any paper of his into perpetuity.
Oh, and there was content: a very nice description of useful design patterns for parser combinators. Nothing earth-shattering here, but it’s really great to have all this material in one place. When I reach for parser combinators next (or am mentoring someone who is), I will point them to this paper.
Noon — Graded Monads and Type-Level Programming for Dependence Analysis, by Finnbar Keating and Michael Gale
- Imagine working with a robot.
- Want types to reflect what we do: such as reading from the screen, writing to the screen, etc.
- Graded monads can help us do this.
Noon — Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk), by Allister Beharry
- Popped into this talk because I was curious about the topic.
- It’s based in F#; not a language I’ve used a lot recently.
- Main idea is to have a language that allows for computer-algebra and general-purpose programming.
- Integrates with other tools (say, Z3).
- I really like the idea in general, and it was nice to watch this and step outside my usual comfort zone a bit.
Richard — In the afternoon PLTea, an interesting conversation led to a new insight: GHC has for some time thought about doing finer-grained analysis for recompilation avoidance. That is, if I change one function, then I have to recompile only modules that depend on that function. But I don’t think the current analysis is always quite that clever. And so, being cleverer would avoid spurious recompilation. The new insight is that this kind of cleverness would be very helpful to IDEs trying to provide live code feedback: in order for an IDE to know where (say) a type error is, it has to run the code through GHC. If we can compile just a tiny part of the file at a time (part of what would power the fine-grained recompilation-avoiding dependency analysis), then this live feedback would come much faster. So it’s nice to see multiple benefits from one feature! Now we just have to design and implement the feature…
About the authors
If you enjoyed this article, you might be interested in joining the Tweag team.
