Johnny Ball: A Betrayal of Science

Last night, I took my family to see a Christmas lecture by Johnny Ball, famous as a television presenter that popularized mathematics with shows in the 1970s and 80s such as Think of a Number.

The beginning of his talk was a beautiful introduction to square laws in the work of Galileo, Kepler, and Newton, with some lovely audience-participation demonstrations showing the value of experiment. Unfortunately, this was belied by the second half, a rant in denial of climate change that included statements such as 'The greens don't want modern society to work so they've decided to demonize carbon' and 'Carbon makes up only 1/3000 of the gases in the atmosphere. Can that have such a big effect? I don't think so'. No mention of the IPCC or the scientific consensus that contradicts his view.

The danger in this is that he may leave youngsters feeling that scientific disputes are similar to political disputes, with no understanding of how the scientific method can establish truth independent of popular opinion.

I gather his hosts, the University of Edinburgh and the Royal Society of Edinburgh, had no idea he was going to go off on this tangent. Going by the first half of his talk, he used to be capable of giving a truly wonderful introduction to science for young people. But now he should not be let near them; he has betrayed his trust.

[Update: This incident was reported in the TES
Johnny causes storm in lecture on climate change.]

Speculations on the Future of Science

From Kevin Kelly, former editor of Wired.

"Technology is, in its essence, new ways of thinking. The most powerful type of technology, sometimes called enabling technology, is a thought incarnate which enables new knowledge to find and develop news ways to know. This kind of recursive bootstrapping is how science evolves. As in every type of knowledge, it accrues layers of self-reference to its former state."

Droste

"The Droste effect is a Dutch term for a specific kind of recursive picture, one that in heraldry is termed mise en abyme."

Arithmetic for lists

Here are analogues of sum, product, and exponentiation for lists. Each takes two lists of values, of types a and b, and forms the list of all values of sum, product, and function (exponent) types.

type Sum a b = Either a b
type Prod a b = (a,b)
type Exp a b = [(b,a)] -- represents functions from b to a

(+++) :: [a] -> [b] -> [Sum a b]
xs +++ ys = map Left xs ++ map Right ys

(***) :: [a] -> [b] -> [Prod a b]
xs *** ys = [ (x,y) | x <- xs, y <- ys ]

(^^^) :: [a] -> [b] -> [Exp a b]
xs ^^^ [] = [ [] ]
xs ^^^ (y:ys) = [ (y,x):e | x <- xs, e <- xs^^^ys ]

The first two of these are already built-in to Haskell, in the form of append and list-comprehensions. The third is also quite useful, and I suggest it should be added to the standard List module. For example, if you want to form a truth table for the list of variables in names, your can do so using [True,False]^^^names to form all 2^n mappings of names to truth variables (where n is the length of names).

In case you doubt whether these actually correspond to sum, product, and exponentiation, here are Peano's definitions:

m+0 = m
m+(n+1) = (m+n)+1

m*0 = 0
m*(n+1) = (m*n)+m

m^0 = 1
m^(n+1) = (m^n)*m

And here are the above operations, rewritten to correspond to Peano's definitions:

(+++) :: [a] -> [b] -> [Sum a b]
[] +++ ys = map Right ys
(x:xs) +++ ys = Left x : (xs +++ ys)

(***) :: [a] -> [b] -> [Prod a b]
[] *** ys = []
(x:xs) *** ys = map f (ys +++ (xs *** ys))
  where
  f (Left y) = (x,y)
  f (Right p) = p

(^^^) :: [a] -> [b] -> [Exp a b]
xs ^^^ [] = [ [] ]
xs ^^^ (y:ys) = map g (xs *** (xs ^^^ ys))
  where
  g (x,e) = (y,x):e


Lambdacats

Thanks to Mitchell Wand.

Are our Civil Liberties being unduly eroded?

[From the newsletter of the Royal Society of Edinburgh.]

This Mock Trial, chaired by Dr Magnus Linklater FRSE, was staged at the Society on Monday 19 November, before a capacity audience, who acted as jurors. The protagonists were Baroness (Helena) Kennedy, QC, who led three witnesses, Shami Chakrabarti, Director of Liberty, Henry Porter, Novelist and Journalist and Roy Martin QC, Former Dean, Faculty of Advocates, arguing for the proposition; and Lord (Charlie) Falconer, PC QC, arguing to the contrary, leading Lord Elder, House of Lords, Alistair Bonnington, Solicitor to the BBC in Scotland and Lord McCluskey, former Solicitor General for Scotland. The event was supported by the Faculty of Advocates, Messrs Balfour & Manson and Messrs Simpson & Marwick, solicitors, and the Clark Foundation, to all of whom the Society is immensely grateful. This interesting and entertaining debate can now be viewed on the Society’s web page.

[The audience, in the role of jury, voted before and after the trial. The initial vote was 94 in favor, 33 against, 20 undecided; the final vote was 95 in favor, 45 against, 7 undecided.]

Hubble captures dance of the galaxies

A stunning photo, courtesy of the Guardian.

The Law of Leaky Abstractions

From Joel Spolsky's blog. Obvious, but no less important for that, and I've never seen a name attached to this important phenomenon before.

F# productized

Don Syme's F# will have commercial support from Microsoft, as part of Visual Studio. Well done, Don!

PC PC: Physical or Virtual?

[A post in honour of Blog Action Day.]

As program chair of POPL 2008, I followed tradition and organized a program committee meeting in Edinburgh last September, attended by 22 members. They worked very hard, and went to great lengths to attend (literally---members came from Japan, New Zealand, and India), and the result was a program I'm looking forward to seeing next January.

But after I sent out the invitations, I read George Monbiot's Heat, and began to wonder if I had made the right choice. If the world got serious about stopping climate change, what would be an equitable figure for Britain's carbon emissions? Monbiot reckons we would need to reduce our carbon footprint to 10% of current levels by 2030. Remarkably, he sketches out a plan whereby this can actually be achieved for house heating, energy sources, ground transport, and so on. With one exception: the only way he could find to reduce the carbon footprint of air travel is to travel less. Way less.

I'm not one of those campaigners who believes that the way to save the world is to bike to work. (I do bike to work, I just don't believe it will save the world.) The solution to our problems will be political, not personal. I'm not willing to stop flying abroad for vacation while the Government's official policy is to expand airport capacity.

But the carbon footprint of a program committee is not negligible. (For POPL, we have a 20+ PC, as compared to 200+ attendees.) And conferences are not personal, they are run by collections of people who can express a political point of view.

Without the climate issue, there are strong arguments both in favor of and against physical PC meetings. For me, the climate issue tips it: I think it is time for conferences like POPL to begin to experiment, to see whether virtual pc meetings might be comparable in effectiveness to physical. It's out of my hands now, but the program chair of the next POPL is considering just that.

Peter Graham, Wandering Shadows

I only recently discovered the Scottish National Gallery, wandering in after visiting the Warhol show at the neighboring Scottish Academy. I was blown away by two pictures. One is listed above.

The other was John Knox, View from Ben Lomond. (Thanks to Anonymous for the correct link!)

Blog Action Day

A simple idea: ask every blogger to post on the same topic on one day, a powerful illustration of how the web can enable democracy. On Monday 15 October 2007, the topic is the environment. Watch this space!

Google, IBM expand program to teach 'Internet-scale' computing

Sounds like a great idea, I'd love to get Edinburgh on the list of participating institutions.

Why you can't cite Wikipedia in my class

A reasoned argument about some of the limitations of Wikipedia. Spotted by my colleague Mahesh Marina.

O'Reilly History of Programming Languages Poster

What it says on the tin. Haskell is the green line near the bottom, just above SML and Caml, and just below Scheme.

Galois

Another play from the festival. They began with a brilliant pocket history of the French revolution (including mime and puppets). They made a valiant run at the mathematics involved, writing quadratic, cubic, quartic, and quintic equations on the blackboard. But not even a straightedge and compass. If King Louis can get a puppet, can't field theory get one too?

The play puts forward the theory that Galois sacrificed himself to foment revolution, ignoring his own reference to a duel over a woman in his last letter. But it did inspire me to reread the history.

The scene where Cauchy dismisses Galois's work as incomprehensible reminded me of too many reviews I had written. But one of my students took the story to heart, saying that it drove home how it is not enough to have an idea, it is just as vital to communicate it!

Ravenhill for Breakfast

One of the joys of living in Edinburgh is the annual festival. My favorite play this year was Ravenhill for Breakfast at the Traverse Theatre. This was part of a series of seventeen short plays written for the festival, I saw number fourteen, which is linked to above.

Haskell Coffin

On the walls at Jane Street, I spotted this work by an artist I had not heard of before, Haskell Coffin.

Jane Street

I visited Jane Street Capital 15--17 August to see the reports from their OCaml Summer Project. Olin Shivers was there too. An excellent time was had by all. I enjoyed speaking in a room filled by clever people interested in FP not in order to write an academic paper, but because they have a large pile of money that they want to make larger.

Four vacancies

Julian Bradfield, head of LFCS, writes:

We have just advertised the first four of what will, it is hoped,
ultimately be ten posts funded via SICSA (a.k.a. "pooling").

Three of the four are areas in which LFCS has an interest, so please
communicate the existence of these posts to anyone or any community
you know where good candidates may be found.

The announced topics are:

• Software Engineering
  
• Modelling/Concurrency
  
• Security
  
• Large Scale and Robust Natural Language Processing
  

and each post may be at Lecturer or Reader level, depending on the
applications.

The official ad is at the link above.

Note that there is a single vacancy reference, so applicants should
make clear the post(s) they wish to apply for.

Functional languages on NearlyFreeSpeech.net

Haskell, Lisp, OCaml, and Scheme (as well as C, C++, Fortran, Java, Lua, Perl, Python, Ruby, and Tcl) are the languages supported by NearlyFreeSpeech.net, a web hosting company. I enjoyed reading their FAQ.

Real-World Haskell

A forthcoming O'Reilly book on Haskell, by Bryan O’Sullivan, Don Stewart and John Goerzen. Interestingly, O’Reilly has agreed to publish chapters online, under a Creative Commons License. (Great that they managed to achieve this, O'Reilly was reluctant to consider something similar when Maurice and I proposed it for our book.)

Festschrift for John C. Reynolds’s 70th birthday

Edited by Olivier Danvy, Peter O’Hearn and Philip Wadler. The community says Thank You to John Reynolds for a lifetime of inspiring ideas. Happy birthday, John!

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!

When IT Becomes a Profession

An intriguing article, suggesting that the current Computing Science must evolve into a much broader discipline. Touches on a number of points, including principles vs. practices, ways in which computing must 'cross the chasm' (in the sense of Geoffrey Moore's book), why computing must focus on its customers, invention vs. innovation, and CS vs. IT. Thanks to Uday Reddy for recommending it.

First Java, then Ajax, and now ... Flash?

Bruce Eckel argues that Flash is the new, new thing. He's particularly keen on Flex, which compiles Actionscript, a superset of ECMAscript, to run on Flash. I agree with him when he says "applications of any complexity using HTML, CSS and JavaScript are difficult and expensive to develop", and also agree that a big motivator for using Javascript or Flash is that there are far fewer installation problems than Java. Perhaps we should consider setting up Links to generate either Javascript or Flash. Thanks to Greg Morrisett for pointing me at the article.

O'Caml Summer Project at Jane St. Capital

Jane St. Capital, a financial firm, made a stir when they started to advertise for O'Caml programmers. Now they are running a summer project, loosely modelled on Google's Summer of Code, to spur development of O'Caml libraries and tools.

Decorators for Python metaprogramming

A cute idea to support code that manipulates code. A tip of the hat to Lambda the Ultimate for the pointer.

Definitional Interpreters for Higher-Order Programming Languages

I just became aware that this seminal paper by John Reynolds was republished by HOSC in 1998, making it available online. (Thanks, Olivier and Carolyn!) If you've never read it and you are interested in programming languages then I suggest you read it immediately. It introduced the term metacircular interpreter and the concept of defunctionalization, as well as being one of the first clear explanations of continuation passing style. The paper is accompanied by a new forward written by John, Definitional Interpreters Revisited.

The Essence of Functional Programming: the code

Oleg Paraschenko has typed in all the examples from The Essence of Functional Programming, and made them available online. There is also a review of the paper in Russian. Thanks, Oleg!