As I am killing time in the hotel waiting for my 6am flight back to the intellectually fertile lands of New Jersey, I figured it might be a good idea to reflect on this past week I spent at the International Conference on Functional Programming in St. Louis, Missouri. I should say that I’m inspired by William’s posts, and it might be a good idea to take notes about the talks I attend so that I can come back if I need to. I’ve been told that I should work on my title-finding skills, and given that I’m becoming more of a metaprogramming buff every day, I think this one is somewhat appropriate.
I gave talk in a conference setting for the first time at the Type-Driven Development workshop, about the paper David and I wrote on our work on extending Idris’s editor actions. It went fine, I think! I made the audience laugh a couple times, once with a reference to a joke Joachim Breitner made the day before about the differences between Coq and Haskell. (the joke is that you swap : and ::) My practice talk had taken 17 minutes (it was supposed to be 20), and I added a bunch of stuff afterwards (more background and examples) but when I finished the actual talk I still had 10 minutes, which means I finished in 15, probably. (I started 2 min early) So we had a long question and answer session afterwards, in which I received some challenging questions, about future directions my work can take. They involved better error message reporting, ways to get around writing any Emacs Lisp at all. Cyrus Omar asked about the possibility of editor action suggestions at a given state, which sounds like a new direction that can and should be explored in any proof assistant, not to mention that it would strongly relate to his vision on his Hazel project.
The next time I should practice more. I remember using the word “obvious” a couple times, which I hate when I hear at other talks. I should not have done that, I’ll try to fix that in the future. I should time myself better, and most importantly, slow down. I was told after my practice talk that I talk too fast and sometimes my syllables get lost because of this. It’s funny that I get this because I do this far more often in Turkish than English. I always thought my diction (not accent) was better in English.
I got a lot of positive reactions afterwards. Jesper Cockx told me that they were going to talk about adding it to Agda at the implementors meeting they’ll have in 3 weeks. When I said that I hadn’t finished the pull request to Idris yet he joked that Agda might have it before Idris, which would be embarrassing. One of my heroes told me at lunch “I remember seeing your talk and enjoying it, but I don’t remember when, where and what it was about”, which I can’t decide is nice or not. I choose to take it the good way. At PLMW, Stephanie Weirich had a list of topics in dependent types that are open questions or areas worth exploring. And then she had a list of papers at ICFP that were about them, in which my paper was included, which was flattering.
Here were the talks and papers that I found especially interesting:
- Equivalences for Free: Univalent Parametricity for Effective Transport: I don’t quite understand this one yet. The talk convinced me that the problem they’re solving is important, but I have to read this more carefully to understand.
- Mtac2: typed tactics for backward reasoning in Coq: This is really impressive, but I’m not fully convinced that tactics with more restrictive tactics are always a better thing. I’ll give this a careful read soon.
- Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (long version of an ML workshop paper): I’m always interested in tactic languages, especially if they’re unified with the metalanguage. They’re considering working on user interfaces as well so I may even be able to collaborate.
- Generic deriving of generic traversals: Deriving efficient lenses using GHC’s generics. I have a generics-based paper idea that I pitched to some people, so I’ll read this one to learn how to tune a Haskell-specific paper to the ICFP audience.
- Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam: Stylistically very interesting functional pearl, featuring two rembetiko musicians! Also the first author worked on tactic languages even before Mtac, so I got to talk to him about where he thinks that area of research is heading, even if I might not be able to pursue that anymore.
- Generic zero-cost reuse for dependent types: I had perused this one a month or so ago, not quite applicable to Agda but certainly interesting.
Not to mention that I also got a ton more papers on my reading list, including Adam Chlipala’s PHOAS paper, which got the most influential paper award. I thought I knew what PHOAS was, from what I learned at the DeepSpec summer school and also a StackOverflow answer, but I should read the source of these concepts to have a more full understanding.
And today, I went to RacketCon, at which I was very impressed by David’s talk about todo-list, Laurent Orseau’s talk about quickscript (with examples), and Pavel Panchecka’s talk about verifiying web pages using Z3 (the project is called Cassius). I pitched a similar idea to some people when I was trying to find a PhD advisor, and I remember not getting particularly positive reactions. My idea was to design a type system to check if a web page is responsive, then one would write the pages in a DSL. Cassius’s approach seems like a better solution for sure, but I’m sure no one had directed me to their work. Maybe I should work on how I communicate not-fully-fleshed-out ideas to other people. When I pitched my generics-based paper idea, I got similar reactions, except for the one person who knew enough about the topic, and some other person who gave me enough time to explain the topic extensively.
This has been a rather frank blog post, but let’s see if this is a good idea or not. I should take these notes for myself anyway, I’m not sure if making them publicly available is a good idea. (Also, I can’t believe I skipped mentioning winning a The Little Typer at a raffle and getting it signed by both David and Dan Friedman!)
Let’s finish this post with a quote from Joachim Breitner’s brilliant talk: “Data type invariant is a euphemism for insufficiently powerful type system.”