Nonreferential this

This month's CACM contains articles by Jeffrey Ullman and Dave Patterson on how to advise PhD students. I particularly enjoyed the following aside from Ullman on a key writing skill:

While it sounds pedantic at first, you get a huge increase in clarity by chasing the "nonreferential this" from students' writing. Many students (and others) use "this" to refer to a whole concept rather than a noun. For example: "If you turn the sproggle left, it will jam, and the glorp will not be able to move. This is why we foo the bar." Now the writer of this prose fully understands about sproggles and glorps, so they know whether we foo the bar because glorps do not move, or because the sproggle jammed. It is important for students to put themselves in the place of their readers, who may be a little shaky on how sproggles and glorps work, and need a more carefully written paragraph. Today, it is not that hard to find a "this" that is nonreferential. Almost all begin sentences, so grepping for 'This' will find them.

Cafe Scientifique

I've been invited to give a talk for Cafe Scientifique, 8.30pm Mon 16 March at the Edinburgh Filmhouse. Title and abstract below. I've been asked to speak without using overheads or visuals, which should be an interesting challenge! The link above takes you to the Facebook page for the event.

Proofs are Programs: 19th Century Logic and 21st Century Computing

As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a principle for designing programming languages that will guide computers into the 21st century.

Similar material is covered in this article.

Conal Elliott on Type class morphisms

Just read Conal Elliott's draft paper Denotational design with type class morphisms. I thought the same point was made more succinctly and with more substance in his earlier paper Simply efficient functional reactivity. Many of us already know what is in the new paper, but it still makes a valuable point. However, I think it should be a Functional Pearl, and it might work twice as well if it were half as long.

Conal is right to put forward type class morphisms as a design principle. However, I think he oversells their utility. In Section 6, he states that the fact the laws of an applicative functor are satisfied for TMap come 'for free', but they are 'free' only because he assumes you have already verified the same laws for (->), which is isomorphic to TMap.

The principle of type class morphisms is closely related to a design principle elucidated by John Reynolds in his paper Using Category Theory to Design Implicit Conversions and Generic Operators: implicit conversions between types should be homomorphisms on generic operators (that is, on overloaded operations defined by both types).

What do you believe is true even though you cannot prove it?

The World Question Center asks a different question every year, and the title links to one of my favorites.

Clay Shirky: Gin, Television, and Social Surplus

Clay Shirky on what we can accomplish if we stop watching tv.

So how big is that surplus? So if you take Wikipedia as a kind of unit, all of Wikipedia, the whole project--every page, every edit, every talk page, every line of code, in every language that Wikipedia exists in--that represents something like the cumulation of 100 million hours of human thought. I worked this out with Martin Wattenberg at IBM; it's a back-of-the-envelope calculation, but it's the right order of magnitude, about 100 million hours of thought.

And television watching? Two hundred billion hours, in the U.S. alone, every year. Put another way, now that we have a unit, that's 2,000 Wikipedia projects a year spent watching television. Or put still another way, in the U.S., we spend 100 million hours every weekend, just watching the ads. This is a pretty big surplus.

Wordle

Wordle lets you generate word clouds from arbitrary sources. The picture shows a cloud built from this blog.

IMU on Citation Statistics

A report from the International Mathematical Union on the use and misuse of citation statistics. Highly relevant with the proposed move toward citations counts as a basis for the new Research Evaluation Framework (REF, the successor to the Research Assessment Exercise, or RAE).

• Relying on statistics is not more accurate when the statistics are improperly used. Indeed, statistics can mislead when they are misapplied or misunderstood. Much of modern bibliometrics seems to rely on experience and intuition about the interpretation and validity of citation statistics.
• While numbers appear to be "objective", their objectivity can be illusory. The meaning of a citation can be even more subjective than peer review. Because this subjectivity is less obvious for citations, those who use citation data are less likely to understand their limitations.
• The sole reliance on citation data provides at best an incomplete and often shallow understanding of research—an understanding that is valid only when reinforced by other judgments. Numbers are not inherently superior to sound judgments.

An off-by-one error heard round the world

At the inauguration of the 44th President of the United States, during the invocation Dr. Rick Warren stated 'Now, today, we rejoice not only in America’s peaceful transfer of power for the 44th time.' But of course, it was the 43rd.

JfJfP and SJJP

Today I became a signatory of Jews for Justice for Palestinians and Scottish Jews for a Just Peace. I should have done this years ago, but given the events of the past week I could not put it off any longer. If not now, when?

Well-typed programs can't be blamed

Philip Wadler and Robert Bruce Findler, ESOP 2009, LNCS to appear.

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.