Wadler's Blog

From Glory, by Greg Egan, a story about one alien race trying to uncover the mathematics of another alien race, three million years old.

The theorem itself was expressed as a commuting hypercube, one of the Niah's favorite forms. You could think of a square with four different sets of mathematical objects associated with each of its corners, and a way of mapping one set into another associated with each edge of the square. If the maps commuted, then going across the top of the square, then down, had exactly the same effect as going down the left edge of
the square, then across: either way, you mapped each element from the top-left set into the same element of the bottom-right set. A similar kind of result might hold for sets and maps that could naturally be placed at the corners and edges of a cube, or a hypercube of any dimension. It was also possible for the square faces in these structures to stand for relationships that held between the maps between sets, and for cubes to describe relationships between those relationships, and so on.

That a theorem took this form didn't guarantee its importance; it was easy to cook up trivial examples of sets and maps that commuted. The Niah didn't carve trivia into their timeless ceramic, though, and this theorem was no exception. The seven-dimensional commuting hypercube established a dazzlingly elegant correspondence between seven distinct, major branches of Niah mathematics, intertwining their most important concepts into a unified whole. It was a result Joan had never seen before: no mathematician anywhere in the Amalgam, or in any ancestral culture she had studied, had reached the same insight.

I'm sure I'll want to cite this someday, possibly in class but perhaps in the pub. What I'll be citing it as an example of, I'm not yet sure. Thanks to Leonid Libkin for spotting this.

Last week I delivered a keynote at AOSD, on Well-typed programs can't be blamed. It was a marvelous opportunity to learn more about aspects, and more about Brussels.

The photo shows me with Gary Leavens atop the Musical Instruments Museum. You wander around wearing a headset, and when you stand next to an instrument you can hear it play. Someday soon, our whole world will be augmented in this way; but you won't need a specially supplied headset, you'll use your phone. One pleasure of my trip was to meet Wolfgang De Meuter and Tom Van Cutsem, whose Ambient Oriented Programming is aimed at just such applications.

People I enjoyed meeting include Dean Wampler, Eric Eide, Curt Clifton,
Emilia Katz, Maja D'Hondt, and Ellie D'Hondt. Ellie works in quantum computation, and told me (rather to my surprise) that monads have an application there. She had once read one of my papers on monads, but found it too difficult. This cheered me up, since I feel the same when I try to read about quantum computation.

Special thanks to Theo D'Hondt, Viviane Jonckers, and Isabelle Michiels for organizing the conference so well.

If you use Lisp and disdain Haskell, or vice versa, you'll want to read this brilliant Orwellian strip by Conrad Barski. Spotted by Ehud Lamm at Lambda the Ultimate. Thanks Conrad! Thanks Ehud!

School teacher and professional mathematician Paul Lockhart has written a brilliant denunciation of what is wrong with the teaching of mathematics in schools. Much of what he says applies equally well to other subjects, I expect. Certainly much of what passes for learning reading in schools takes something lively and beautiful and does its best to render it dull and lifeless, just like mathematics. And exposure to computing in secondary schools seems more likely to turn off and misdirect students then to prepare them to continue the subject in university.

I particularly enjoyed Lockhart's opening, an extended metaphor:

'A musician wakes from a terrible nightmare. In his dream he finds himself in a society where music education has been made mandatory. “We are helping our students become more competitive in an increasingly sound-filled world.” Educators, school systems, and the state are put in charge of this vital project. Studies are commissioned, committees are formed, and decisions are made—all without the advice or participation of a single working musician or composer.

'Since musicians are known to set down their ideas in the form of sheet music, these curious black dots and lines must constitute the “language of music.” It is imperative that students become fluent in this language if they are to attain any degree of musical competence; indeed, it would be ludicrous to expect a child to sing a song or play an instrument without having a thorough grounding in music notation and theory. Playing and listening to music, let alone composing an original piece, are considered very advanced topics and are generally put off until college, and more often graduate school.'

Years ago, I asked Mitch Wand whether it was possible to extend his lovely constraint-based inference algorithm to handle polymorphic let. Now Sunil Kothari and James Caldwell have done just that. (François Pottier has also done nice work along these lines, which these authors don't cite.)

Postscript: Didier Rémy writes to let me know that the material in François Pottier's notes that I cite above also appears in a definitive textbook form: François Pottier and Didier Rémy. The Essence of ML Type Inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, Chapter 10, pages 389-489, MIT Press, 2005. Didier confirms that this work subsumes the work of Kothari and Caldwell.

Last December, I wrote about Johnny Ball. I was outraged that he ended a lecture that was supposed to educate children about science with a rant denying climate change. That post has eighteen comments to date, more than any other blog entry.

I wrote: "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."

Most of those commenting took umbrage with my claim that there is a scientific consensus that man-made climate change is occuring, and they counter-claimed that the IPCC is politically biased. The article linked to above, by Joseph Romm on Salon, sets out the case very well. He points out that the word 'consensus' is indeed inappropriate in the scientific context, and that the IPCC is indeed biased: political influences have caused it to water down its conclusions enormously.

My favorite lines from the article: "One reason science works is that a lot of scientists devote their whole lives to overturning whatever is the current hypothesis -- if it can be overturned. That's how you become famous and remembered by history, like Copernicus, Galileo, Newton, Darwin and Einstein.

"In fact, science doesn't work by consensus of opinion. Science is in many respects the exact opposite of decision by consensus. General opinion at one point might have been that the sun goes around the Earth, or that time was an absolute quantity, but scientific theory supported by observations overturned that flawed worldview."

Thanks to Maurice Naftalin for pointing me at the article. (And now I await a new cascade of critical comments.)

Andres Loeh, Conor McBride, and Wouter Swierstra. Simply Easy! An implementation of a dependently typed lambda calculus. Draft.

A tutorial introduction to dependent types aimed specifically at Haskell programmers. Lovely! I hope this appears somewhere soon.

Wouter Swierstra. Data Type a la Carte. Functional Pearl, accepted to Journal of functional programming.

Presents the best solution to the Expression Problem that I've seen in Haskell (well, Haskell with -fglasgow-exts).

There is one unfortunate feature. The instances of the injection function for subtypes are assymmetric:

data (f :+: g) e = Inl (f e) | Inr (g e)

class (Functor sub, Functor sup) => (:<:) sub sup where
inj :: sub a -> sup a

instance Functor f => (:<:) f f where
inj = id

instance (Functor f, Functor g) => (:<:) f (f :+: g) where
inj = Inl

instance (Functor f, Functor g, Functor h, (:<:) f h) => (:<:) f (g :+: h) where
inj = Inr . inj


It would be better to replace the left instance by one symmetric with the right:

instance (Functor f, Functor g, Functor h, (:<:) f g) => (:<:) f (g :+: h) where
inj = Inl . inj

But Haskell, alas, cannot support this (even with -fglasgow-exts). Is there a symmetric solution in Haskell?

One of my favourite examples of the confluence of theory and practice is this pair of papers on exception handling.

Nick Benton and Andrew Kennedy, Exceptional Syntax, Journal of Functional Programming, 11(4):395--410, July 2001.

Richard Carlsson, Björn Gustavsson, Patrik Nyblom Erlang's Exception Handling Revisited, Erlang Workshop, Snowbird, Utah, September 2004.

Both present exactly the same variant on traditional exception handling, but the first paper is driven by proof-theoretic concerns, while the second is entirely pragmatic. (Alas, the symmetry is marred by the fact that Benton and Kennedy also address pragmatics, though one can hardly fault them for that.)

Both papers exhibit deep insight of different kinds, and both are a pleasure to read. A brilliant example of Curry-Howard in action!

`You can get soup in a can. You can get bread in a can. Now the long wait is over! You can finally get Lambda Calculus in a can...Project LambdaCan takes [the Lambda Calculus] and implements it on a microcontroller better suited to the most mundane of tasks, like running a vending machine or microwave oven. And it sticks the microcontroller in a can that you can connect to your PC using a USB cable.'

Spotted on Lambda the Ultimate.

`This time we’ve taken almost 300 of the most influential and successful websites and pinned them down to the greater Tokyo-area train map.'

It reminds me of Simon Patterson's The Great Bear.

POPL in San Francisco was brilliant. My thanks to everyone who made it happen, particularly the authors and speakers. This year we tried an experiment, with three talks in an hour session (rather than three talks in an hour and a half, or four talks in two hours). I was delighted that all of the speakers worked hard to give a proper twenty minute talk, rather than cramming a thirty minute talk into twenty by speaking fast. Conor McBride deserves special mention for a superb performance of his pearl, 'Clowns to the left of me, jokers to the right'. The comments I received on twenty minute talks and on pearls were positive, and I hope both will become POPL traditions.

One of the joys of the trip was sitting in the sun at Union Square, working on the blame calculus with Jacob Matthews, Amal Ahmed, and Robby Findler. Another was going on a Segway tour of Fisherman's Wharf with Robby. The photos show us on our Segways and in front of the Palace of Fine Arts.

Some representations are easier to use than others. Ease of use also seems to depend on purpose and inclination. S-expressions are excellent for many purposes, but the associative law is far easier to read in an infix notation. Compare

(= (+ x (+ y z)) (+ (+ x y) z))

and

x + (y + z) = (x + y) + z.

My taste puts S-expressions far above XML, but given the relative popularity of the two, I presume for some it is the exact opposite.

Ezra Cooper and I observed the importance of the pain of representation in connection with mapping function calls into path names. If every function takes a fixed number of arguments, one can map a call directly into a path name. For example,

f(g(a,b), h(c))

becomes

f/g/a/b/h/c

although the second is less clear to read. We could map open and close brackets into the path

f/open/g/open/a/b/close/h/open/c/close/close

but this so painful as to be worse than useless.

There must be a psychological theory that can underpin such choices. A quick web search failed to turn up anything apposite, suggestions for the correct terms to search on would be welcome.

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.]

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."

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

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


Thanks to Mitchell Wand.

[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.]

A stunning photo, courtesy of the Guardian.

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.

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

[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.

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!)

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!

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

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

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

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!

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.

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

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.

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.

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.

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.)

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!

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.

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".

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

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).