2012/01 : ezyang's blog

2012/01

POPL January 28, 2012

Last night, I returned from my very first POPL, very exhausted, and very satisfied. It was great putting faces to names, chatting with potential PhD supervisors (both from the US and in the UK), and reveling in the atmosphere.

Highlights from my files:

Tony Hoare, on being awarded the ACM SIGPLAN Programming Languages Achievement Award, even though he has received so many other awards, “…it makes me feel a little guilty. I didn’t ask for it!”
Hoare: “I like mistakes; if I find it’s my fault, I can rectify it. If it’s someone else’s fault, there’s not much you can do.”
Hoare: “Simplicity is not an engineering goal.”
Tony had just described how he retracted an accepted paper because the reasoning on it was intricate, and he didn’t think it presented program proving in a good light. The interviewer complimented him for his principles, saying that if he had a paper accepted which he didn’t think was up to snuff, he probably wouldn’t have the courage to retract it. It was “so brave.” To which Tony replies, “Well, I wish you could!” [laughter] “Unfortunately, the pressure to publish has increased. We feel obliged to publish every year, and the quality of the average paper is not improved.”
One recurring theme: Tony Hoare mentioned that proofs and tests were not rivals, really they were just the same thing… just different. In the “Run your Research” talk, these theme came up again, where this time the emphasis was executable papers (the “run” in “Run your Research”).
“Don’t just support local reasoning, demand it!” (Brute force proofs not allowed!)
On JavaScript: “null is sort of object-y, while undefined is sort of primitive-y.”
The next set come from the invited speaker from the computer networks community. “During 9/11, on average, the Internet was more stable. The reason for this was the NetOps went home.” (on the causes of network outages in practice.)
“Cisco routers have twenty million lines of code: there’s actually an Ada interpreter in there, as well as a Lisp interpreter.”
“It used to be acceptable to go down for 100ms… now we have video games.”
Speaker: “I am the walrus.” (Goo goo g’ joob.)
“I believe we do not reuse theorems. We reuse proof methods, but not the actual theorems. When we write papers, we create very shallow models, and we don’t build on previous work. It’s OK. It’s the design. It doesn’t matter too much. The SML standard was distributed with a bug report, with 100+ mistakes in the original definition. Doesn’t detract from its impact.”
“Put on the algebraic goggles.”
“The Navy couldn’t install it [a system for detecting when classified words were being transmitted on insecure channels], because doing so would be admitting there was a mistake.”
“Move to something really modern, like Scheme!” (It’s like investing one trillion, and moving from the thirteenth century to the fourteenth.)
Strother Moore (co-creator of ACL2): “After retirement, I’ll work more on ACL2, and then I’ll die.”
“What’s the best way to make sure your C program is conforming?” “Write deterministic code.” [laughter]

Modelling IO: MonadIO and beyond January 24, 2012

The MonadIO problem is, at the surface, a simple one: we would like to take some function signature that contains IO, and replace all instances of IO with some other IO-backed monad m. The MonadIO typeclass itself allows us to transform a value of form IO a to m a (and, by composition, any function with an IO a as the result). This interface is uncontroversial and quite flexible; it’s been in the bootstrap libraries ever since it was created in 2001 (originally in base, though it migrated to transformers later). However, it was soon discovered that when there were many functions with forms like IO a -> IO a, which we wanted to convert into m a -> m a; MonadIO had no provision for handling arguments in the negative position of functions. This was particularly troublesome in the case of exception handling, where these higher-order functions were primitive. Thus, the community began searching for a new type class which captured more of IO.

monad-control is tricky January 23, 2012

Editor’s note. I’ve toned down some of the rhetoric in this post. The original title was “monad-control is unsound”.

MonadBaseControl and MonadTransControl, from the monad-control package, specify an appealing way to automatically lift functions in IO that take “callbacks” to arbitrary monad stacks based on IO. Their appeal comes from the fact that they seem to offer a more general mechanism than the alternative: picking some functions, lifting them, and then manually reimplementing generic versions of all the functions built on top of them.

Mystery Hunt and the Scientific Endeavour January 16, 2012

It can be hard to understand the appeal of spending three days, without sleep, solving what some have called “the hardest recreational puzzles in the world,”; but over this weekend, hundreds of people converged on the MIT campus to do just that, as part of MIT Mystery Hunt. To celebrate the finding of the coin, I’d like to share this little essay that I found in my files, which compares Mystery Hunt and the scientific endeavour. (If you are not familiar with Mystery Hunt, I recommend listening to the linked This American Life program.)

Problem Set: The Codensity Transformation January 7, 2012

Have you ever wondered how the codensity transformation, a surprisingly general trick for speeding up the execution of certain types of monads, worked, but never could understand the paper or Edward Kmett’s blog posts on the subject?

Look no further: below is a problem set for learning how this transformation works.

The idea behind these exercises is to get you comfortable with the types involved in the codensity transformation, achieved by using the types to guide yourself to the only possible implementation. We warm up with the classic concrete instance for leafy trees, and then generalize over all free monads (don’t worry if you don’t know what that is: we’ll define it and give some warmup exercises).

Why iteratees are hard to understand January 4, 2012

There are two primary reasons why the low-level implementations of iteratees, enumerators and enumeratees tend to be hard to understand: purely functional implementation and inversion of control. The strangeness of these features is further exacerbated by the fact that users are encouraged to think of iteratees as sinks, enumerators as sources, and enumeratees as transformers. This intuition works well for clients of iteratee libraries but confuses people interested in digging into the internals.