Reith Lectures 2007

Taking his lead from John Kennedy's precept 'Peace is a Process', in the 2007 Reith Lectures, Jeffrey Sachs, Director of the Earth Institute at Columbia University, lays out a system of initiatives that government, institutions, and citizens can follow to achieve peace, limit climate change, and reduce economic inequality. In the last lecture, he claims a special place for scientists to organize to solve the world's ills, and cites Wikipedia and Linux as a model---a sort of Open Source government. Heady stuff; it's not often one encounters this scope of vision. The lectures are delivered from London, Beijing, New York, and (for the finale) Edinburgh, home of Adam Smith and the Enlightenment.

Oh no! Alligators!

One of my great joys on visiting Berkeley was to meet Bret Victor, of Magic Ink fame. I mentioned to him that I had been working with a student on a visual lambda calculus, in part because I wanted a way to explain lambda calculus to my eight-year old daughter and son. He responded with a game involving alligators and their eggs, such a clever morphing of lambda calculus that it wasn't until I reached the end that I realized exactly what was going on.

So far, I've had a chance to show it to my daughter, who managed to successfully solve the problem at the end. She guessed a definition of 'not', and then applied 'not' to 'true' and checked that the result is 'false'. But she was most interested in drawing pictures of alligators! I expect it would be more fun to use if there was software that implemented the game.

Bret also pointed to David Keenan's graphical lambda calculus, based on Raymond Smullyan's "To Mock a Mockingbird".

LambdaVM

A backend for GHC that compiles to the JVM, by Brian Alliet. Thanks to Adam Megacz for the pointer.

Visit Stanford, Google, Intel Berkeley

Many thanks to my hosts who invited me to speak at Stanford, Google, and Intel Berkeley. A link to the video of my Google talk is above, Intel Berkeley tells me they will also post a video.

I met quite a few interesting folk on my visit, including Dominic Hughes, Adam Chlipala, Adam Megacz, and Bret Victor (of Magic Ink fame).

Google Tech Talk: Parametric Polymorphism

A talk by Phil Gossett given in Google's Advanced Programming Language series. Cites my work on type classes and the Girard-Reynolds isomorphism; I was pleased to see he began by discussing Frege and Russell, and finished by describing Lennart Augustsson's Djinn. Nice talk, and has me looking forward to speaking at Google (which I'm scheduled to do this Friday); my talk will cover some similar material. (I tried to find Gossett's e-mail and failed, maybe this will help me get in touch.)

I spotted a couple of technical errors in the talk. (1) He suggested that the Girard-Reynolds Isomorphism guarantees that every term that has a given polymorphic type is isomorphic; in fact, distinct proofs of a theorem correspond to distinct terms of a type. (2) In answer to a question, he said that parametricity does not extend to type classes; in fact, my paper Theorems for Free includes a sketch of how parametricity does extend to type classes (see Section 3.4).

Magic Ink: Information Software and the Graphical Interface

A screed by Bret Victor. The only document I've read that compares with Edward Tufte (author of four famous books on information design). Shows how beautiful a web page can be. My favourite parts were

• Demonstration: Showing the data. Redesigning Amazon as an information graphic.
• Demonstration: Arranging the data. Redesigning Yahoo! Movies as an information graphic.

I would skip to those to start. Spotted via Lambda the Ultimate.

Particle-wave duality

A fragment of an animated video explaining particle-wave duality. Nicely done, though the explanation of how a particle behaves when observed verges on anthropomorphic. Of course, I like the character in the superhero suit. On YouTube, spotted via Slashdot Review.

Three ways to improve your writing

Read these three texts. Each is short, but the benefits will last a long time. Heeding their advice will improve your life. It will improve mine too, if I ever read what you write.

• Minicourse on Technical Writing by Donald Knuth. When an undergraduate I had the great fortune to take Knuth's course on algorithms, which included a couple of lectures on technical writing. If my writing is readable, that owes much to Knuth. Later, Knuth ran a semester-long seminar on the subject, which you'll find at the end of this link. The first three sections are the minicourse, and worth their weight in gold.
  
  I endorse all he says, save that in Section 1, Point 24, I think even the 'good' examples are bad. Better to find a vigorous verb for the vital first sentence, rather than dull 'is' or 'are'.


• Politics and the English Language by George Orwell. The predecessor of Haskell was named Orwell, and the user manual began with this quotation from the essay:
  

  A man may take to drink because he feels himself to be a failure, and then fail all the more completely because he drinks. It is rather the same thing that is happening to the English language. It becomes ugly and inaccurate because our thoughts are foolish, but the slovenliness of our language makes it easier for us to have foolish thoughts.

  Orwell explains why you cannot think clearly unless you express yourself clearly, and gives rules of thumb to help ensure the latter.


• The Elements of Style by William Strunk Jr and E. B. White. The book is 105 pages and costs under five pounds. It could be the best five pounds you ever spent.
  
  If you're too cheap to buy the book, Bartelby has an online version of the first edition, Strunk before White.

Read, enjoy, and write better!

A modern eye on ML type inference

François Pottier, A modern eye on ML type inference: old techniques and recent developments. Lecture notes for the APPSEM Summer School, September 2005, Frauenchiemsee, Germany. The above link takes you to the slides of the talk; there is also an associated paper.

Many interesting ideas, including a constraint-based view of Hindley-Milner typing that includes 'let' generalization (something that I've sought ever since reading Mitchell Wand's lovely paper on the subject). Thanks to Wand for the recommendation.

Lisp in XKCD

From XKCD, a webcomic of romance, sarcasm, math, and language, by Randall Munroe. Thanks to Mitchell Wand for passing this on!