Great minds think alike

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!

Lambda Calculus in a Can

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

Web Trend Map 2008

`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

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.

Representation Pain

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.

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.