Wadler's Blog

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.