TLDR: Follow me on Twitter if you want to see me share stuff.

For the last n months, I have been using IFTTT to mirror my Twitter account to my Facebook account. I am going to stop doing this because neither Facebook nor IFTTT support what I need to make this sensible.

I started using IFTTT because, while I maintain a Facebook account and connect with several people exclusively through Facebook, I primarily use Twitter. Twitter is easier to use for me, partly because posts are shorter and I manage my time carefully, and partly because bitlbee gives me an interface that matches my natural environment. Unfortunately, Facebook is not great at the same sorts of things that Twitter is.

Twitter automagically supports links and pictures that you tweet, linking and embedding them as appropriate depending on your client. Twitter supports a much more active stream of thoughts. Twitter makes it absurdly easily to share other peoples’ thoughts with attribution, i.e., retweets. Twitter has course-grained privacy, and the usual workflow for having private and non-private tweets is via multiple accounts, which Twitter clients support.

On the other hand, Facebook requires you to explicitly tell it what to do. If you post a link, but do not claim it is a link, Facebook will merely hyperlink the URL rather than embed the link. Facebook supports longer posts but fewer of them. Facebook seems to encourage sharing your own thoughts. Although it does support sharing, it is not nearly as simple, and is easy to remove to original attribution (presumable for privacy of the original author). Facebook supports fine-grained privacy of individual posts, but this too requires more interaction, i.e., explicitly telling Facebook what to do.

I setup IFTTT to simply mirror my tweets to Facebook, sharing them only with friends. However, I want some tweets to be public, and some to be friend-only. I want links and pictures to be automagically embedded. I want my tweets to appear without attribution, and retweets to appear with attribution. I only want some tweets to be mirrored.

While IFTTT has some support for some of this, for instance, using hashtags to denote which tweets should be thought of as links and the link embedded, it does not support everything that I want. Part of this is on Facebook for not being automagical, but I think this is probably a feature for Facebook since too much automagic is not appealing to many users. I, however, like automagic.

So, I am turning off IFTTT, and my Facebook posts will all but disappear. If you care about my random day-to-day thoughts, follow me on Twitter instead. All my Facebook messages go to bitlbee though, so I am still accessible through that.

A couple weeks ago, I wrote that I was beginning to hate conference talks. The next morning, I woke up with 50+ Twitter notifications caused by people debating that point. I have reconsidered my views.

In my earlier post, I point out that the typical advice I hear is “The talk should be an ad for the paper”. After several discussions, I think this is bad advice. Instead, Lindsey Kuper and Chris Martens encouraged me to ignore this advice and instead make my talk a performance.

At first, I was unsure what this meant. In fact, I am still not quite what this means. What does it mean to perform a paper? But I followed it anyway.

Essentially I tried to communicate, at a high-level, why I think this work is cool, and what parts of the work are most interesting. I tried to tell a story about what inspired this work, why I care about it, and what came out of it. I did not try to show many technical details; I showed only those necessary to tell the story of this work. I did not try to explain the particulars of all this work; I showed only those necessary to fit the work into the context of the story I wanted to tell.

I think the end result is actually an effective ad for the paper. However, by approaching the talk differently, I produced a much better talk (IMHO). And thankfully, I am not alone in that opinion. For example, I was very excited after my initial practice talk when Matthias called the talk “90% perfect”, in defiance of a NU PRL tradition of not dwelling on positive aspects and only giving constructive criticism after a practice talk.

A video of this talk is online here.

I am beginning to hate conference talks. I am in the midst of writing a conference talk for my recently accepted paper. Although I have only given one conference talk thus far, I have attended several conference and listened to many talks. These experiences have convinced me that conference talks are largely pointless.

I do not find conferences to be pointless. The papers are usually well written, if dense. The conferences themselves always lead to interesting conversations with clever people. I always return from a conference filled with creative energy. And, I admit, I like the excuse to travel to interesting locales.

However, the talks themselves are pointless. Most talks I have attended are terrible. Those that are not terrible I do not remember much of anyway, except that I should go read that paper. Of those talks, I would have made the same decision after reading the abstract for the paper. The talks add nothing because the talk slots are too short to communicate any technical material.

It is not entirely the fault of the speakers. For one, there is little incentive to give a good talk. If you give a good talk, then maybe you convince someone to read your paper, and maybe people remember who you are. This might be important if you are on the job market, but it does not matter for everyone else. Besides, most people will forget the talk in a month, good or bad.

Even if you are a perfectionist so incentive does not matter, it is not easy to craft a good talk. Conference papers are often complex and dense pieces of work. Frequently, the papers omit many details due to space, so completely understanding the work requires not only the paper but a technical appendix or code artifact published separately. Authors (usually (maybe only sometimes)) spend a great deal of time polishing these papers and supplementary materials to effectively communicate a complex and dense piece of work. The slot for the conference talk is 15—20 minutes, in which a speaker much fit a 12-page paper plus supplementary material?

“No! Obviously as a speaker you must not do that. The talk should be an advertisement for the paper. It should be an overview of the paper. It should communicate the key technical ideas and convince people to read the paper.”

What silly advice. I hate advertisements. Why should I sit through sessions and sessions of advertisements?

“No! Obviously as an audience member you must not do that. Just go read the abstracts and find the talks you want to attend. Skip the rest to have conversations with colleagues and authors.”

Okay, so the audience is going to read the abstract to convince them to see a talk that convinces them to read the paper of which they just read the to convince them to see the talk that convinces them to read the paper? This is circular reasoning that wastes the time of both the speaker and the audience.

As a speaker and writer, I have already spent a lot of time and effort on the paper. I have crafted the abstract and introduction to communicate the key technical ideas and give an overview of the paper as precisely and concisely as possible. Shortly thereafter, I have carefully written the rest of the paper to effectively communicate the technical contributions in as much detail yet as concisely as page limits allow. Besides, I had to write them anyway to effectively communicate my research. Why should I reproduce these efforts in a short talk that must communicate less due to the nature of the talk and the audience?

As an audience member, if I want an overview of the paper, the abstract and introduction section provide this. The author already spent a great deal of time writing these sections, which communicate more thoughts in less time than the talk will. If I want more details, these sections are conveniently located with the rest of the paper. Besides, I need to read the abstract anyway to figure out which talks to attend and which papers to read. Why should I then sit through a talk that advertises a paper that I have already decided whether or not to read?

“Well the talks give an excuse and talking points around which we can organize a conference.”

Well why can’t we find a better excuse or better talking points? Why not give longer highly-technical talks that supplement the paper, or questions-and-answer style talks for those who have read the paper and want more? Or why not make the papers more open ended so talks can be more speculative?

I do not know what should go in place of the current conference talks, but the current system seems utterly pointless and results in completely wasted effort.

A while back I wrote a post about paranoia in which I was considering allowing Google or Apple to manage things like my calendar and contacts. Since then, I have reequipped my paranoia hat. This week I setup my own WebDAV, CalDAV, and CardDAV servers and secured them behind an nginx proxy which provides SSL encryption and HTTP authentication.

My monthly cellphone bill averages less than $10 per month. I have a smartphone. I have data, texting, and voice, and I use them. Let me tell you how I achieve such a low bill.

Disclaimer: I will get a credit if you sign-up through my referral link, but so will you.

I need to write more.

In order to practice writing clearly and concisely,

to organize my thoughts,

to let small thoughts grow,

to store my thoughts in a less imperfect storage medium,

I need to write more.

And so begins a weekly¹ Rambling.

¹ hopefully.

Today I read Ur: Statically-Typed Metaprogramming with Type-level Record Computation. This paper presents the Ur language, a functional programming language based on an extension of System Fω. The novel idea is to use type-level functions as a form of type-safe meta-programming. The paper claims this novel idea enables safe heterogeneous and homogeneous meta-programming in Ur.

The interesting insight is that type-level computation may be valuable outside of dependently typed languages. The paper quickly and easily makes this case. The type-level computations reduce type annotations by enabling the programmer to compute types rather than manually write them everywhere. This could be a useful form of meta-programming in any typed language.

The claims about heterogeneous and homogeneous meta-programming seem overstated. Ignoring the novel ability to compute type annotations, type-safe heterogeneous programming could be as easily accomplished in any other type-safe language. I could just as easily (or more easily) write a program in Coq, ML, Haskell, or Typed Racket that generates HTML and SQL queries as I could in Ur. As for homogeneous meta-programming, restricting the meta-programs to record computations at the type-level seems to severely restricts the ability to generate code at compile-time and abstract over syntax, features which are provided by general-purpose meta-programming systems such as Racket’s macros or Template Haskell.

Yogurt is stupid expensive compared to the milk from which it is made, particularly if you want Greek-style yogurt.

So I decided to do it myself.

This summer I was in Paris for two months. Every day I got a fresh baguette for under €1. When I got back, I couldn’t eat store bought bread. It was terrible. And it cost $3. There’s no bakeries nearby, and the grocery store baguettes are crap and even more expensive.

So I decided to do it myself.

In my recent work, I found it useful to pair a term and its context in order to more easily reason about weakening the context. At the prompting of a colleague, I’ve been reading about Beluga, [1] [2], and their support for programming with explicit contexts. The idea seems neat, but I’m not quite sure I understand the motivations or implications.

So it seems Beluga has support for describing what a context contains (schemas), describing in which context a type/term is valid, and referring to the variables in a context by name without explicitly worrying about alpha-renaming. This technique supports reasoning about binders with HOAS in more settings, such as in the presence of open data and dependent types. Since HOAS simplifies reasoning about binders by taking advantage of the underlying language’s implementation of substitutions, this can greatly simplify formalized meta-theory in the presence of advanced features which previously required formalizing binders using more complicated techniques like De Bruijn indices. By including weakening, meta-variables, and parameter variables, Beluga enables meta-theory proofs involving binders to be much more natural, i.e., closer to pen-and-paper proofs.

Obviously this is great for formalized meta-theory. While I have seen how HOAS can simplify life for the meta-theorist, and seen how it fails, I don’t fully understand the strengths and weakness of this work, or how it compares to techniques such as the locally nameless. I’m also not sure if there is more to this work than a better way to handle formalization of binding (which is a fine, useful accomplishment by itself).

If anyone can elaborate on or correct my understanding, please do.