Wadler's Blog

Welcome to Scotland, Neil, Patricia, and Conor!

2008-06-30T13:39:00.003+01:00

A big welcome to Neil Ghani, Patricia Johann, and Conor McBride, who are establishing a new research group in Mathematically Structured Programming at the University of Strathclyde. And a big congratulations to Strathclyde, on attracting three top-notch researchers. Their arrival will strengthen the already strong programming languages community in Scotland, and they've already volunteered to host a meeting of SPLS.

Add FP to the ACM curriculum

2008-06-10T18:29:00.002+01:00

As a result of a recent Harvard workshop, there is a proposal to add FP to the ACM curriculum, and ACM members are encouraged to comment. Many excellent arguments appear on the comment page, here are two of my favorites.

Greg Morrisett:

I strongly endorse the recommendation to include functional programming in the curriculum. The most important benefit is a change in the mode of thought that can strongly influence design at all levels, from hardware to distributed systems. If they are to be successful, students must be able to pick up and learn new languages. Without deep experience in at least two very different environments, they will be unable to do so.

Robert Harper:

I endorse the proposed change to PL7/FunctionalProgramming to include more hours on the topic of functional programming and to correspondingly reduce commitment to vague or obsolete topics in the proposed curriculum. Functional programming has emerged as the central organizing principle in programming language design, and is increasingly important in industrial as well as academic settings. Once considered an esoteric niche topic, functional programming has emerged as a unifying conceptual framework that encompasses and enriches traditional concepts such as imperative and object-oriented programming. Many of the major innovations in language design over the last decade have emerged from the functional programming perspective, including reliance on managed storage ("garbage collection"); emphasis on static type disciplines in general and specific advances such as generics in particular; and the role of higher-order techniques, including functions and objects, for building reusable software component.

Current trends in the computer industry favor the functional perspective: (a) very large scale distributed computing models, such as Hadoop or map/reduce, depend essentially on the functional (state-free) model of computing; (b) small to medium-scale parallel computing, such as multicore processors or shared memory multiprocessors, strongly favors the functional model, which ensures determinacy of outcomes even in the presence of parallelism; (c) demand for mechanical verification of program properties to ensure software quality favors the functional model, which emphasizes the single most successful integration of formal methods into programming, rich static type systems.

It is entirely appropriate for ACM to place renewed emphasis on functional programming in the undergraduate curriculum. The present proposal, though overly modest, takes a step towards modernizing undergraduate education in programming languages. I urge that this change be adopted.

History of Lambda-calculus and Combinatory Logic

2008-06-05T10:50:00.002+01:00

This is the most definitive history of lambda calculus of which I am aware, a most useful resource. It includes two contradictory stories, both told by Church, of why Church picked the symbol 'lambda' (see p 7), but not the story that Church conceived the predecessor function after exposure to laughing gas at his dentist. (Does anyone know a source for that story?) My thanks to the authors for their efforts.

The Expression Lemma

2008-06-02T19:08:00.002+01:00

Ralf Laemmel and Ondrej Rypacek have a paper in MPC 2008 on the duality of functions and objects, which they formalize as folds over algebras and unfolds over coalgebras, as a step toward deeper understanding of The Expression Problem. I like their idea of dual models of functions and objects as algebras and coalgebras, has this appeared elsewhere?

Alien Category Theory

2008-04-25T15:54:00.004+01:00

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 uniﬁed 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.

Fun with correlation and citations

2008-04-16T11:31:00.003+01:00

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.

Fractal Food

2008-04-11T15:28:00.002+01:00

Who can resist
Sierpinski cookies and fractal pizza? Spotted via Boing Boing.

AOSD 2008, Brussels

2008-04-10T14:10:00.004+01:00

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.

Functional Programming is Beautiful

2008-04-07T17:47:00.003+01:00

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!

Lockhart's Lament

2008-03-20T09:48:00.004Z

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

On Extending Wand’s Type Reconstruction Algorithm to Handle Polymorphic Let

2008-03-06T10:45:00.003Z

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.

The cold truth about climate change

2008-02-29T10:49:00.006Z

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

Simply Easy

2008-02-28T11:57:00.002Z

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.

Data Types a la Carte

2008-02-28T11:55:00.003Z

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?

Great minds think alike

2008-02-26T17:29:00.004Z

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

2008-02-13T18:50:00.002Z

`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

2008-02-06T09:48:00.000Z

`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

2008-01-22T11:08:00.000Z

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

2008-01-22T10:54:00.000Z

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

2007-12-18T09:19:00.000Z

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

2007-12-17T09:44:00.000Z

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

2007-12-14T16:53:00.001Z

"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

2007-12-04T15:20:00.000Z

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

2007-12-03T13:21:00.000Z

Thanks to Mitchell Wand.

Are our Civil Liberties being unduly eroded?

2007-11-29T09:30:00.000Z

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