If the Matrix ran on Windows

Brilliant and hilarious amateur production.

If programming languages were X

Lambda the Ultimate has a collection of analogies of the form 'If programming languages were X' for X varying over religions, cars, and so on. My favorite is girlfriends.

Unsafe

Via Iain Parris.

A person ran
$ grep -w -o '\(unsafe[A-Z][a-zA-Z]*\)' haskell.log | sort -u.
A handful of highlights from the list:
unsafeAtAnySpeedIO
unsafeShutUpAndActLikeACompiler
unsafeAttemptMiracles
unsafeBuyBackLoans
unsafeCallCthulhu
unsafeCollideHadrons
unsafeEatBabiesAndMaybePerformIO
unsafeExecuteArbitraryMachineCode
unsafePerformTheMightyFistOfTheDesertGodWithNoVowelsInHisName


Type Safe Pattern Combinators, by Morten Rhiger

An ingenious set of combinators for expressing pattern matching in a type-safe way. No ADTs required. Opens up the possibility of programming languages where we can declare new binding forms just as we declare new functions. Revolutionary, but may have been hard to publish before Programming Pearls were created---it shows why they are a good idea.

RAE 2008

Every few years, the UK Government conducts the Research Assessment Exercise, to determine the quality of research of every department in every university. The results for the most recent exercise are out, and by any measure Informatics at the University of Edinburgh did very well.

The Price of Forgoing Basic Research

An article by Bill Buxton in Business Week, making the case that too much emphasis on applications is counterproductive. My favorite line:

To be blunt, I believe that when academic research starts demonstrating industry relevance is when funding should be cut off, not augmented.

Informatics Christmas Meal

Facebook tells me the photo at left was shown at the Informatics Chrismas Meal. Caption: '"Some believed we lacked the programming language to describe your perfect world." says Agent Smith. Well, they should've used Lamda Calculus!'

Informatics 1 - Fancy Dress and Competition

Every year I enjoy teaching Haskell to Informatics 1, but this year was spectacular. The students decided to attend the last day of lectures in fancy dress, and brought cupcakes decorated with lambdas. This year's programming competition was also exceptional. Every year there are one or two stunning entries, but this year we felt we had to award prizes to no less than seven!

Scooping the Loop Snooper

A proof in verse of the undecidability of the halting problem, in the style of Dr Seuss, by my colleage Geoffrey Pullum.

No general procedure for bug checks succeeds.
Now, I won’t just assert that, I’ll show where it leads:
I will prove that although you might work till you drop,
you cannot tell if computation will stop.

Proofweb

Looks interesting, but I was unable to figure out how to get it to complete even a simple proof.

A bizarre function over streams

Alex Simpson showed me this bizarre function. Given a total predicate p over streams, the function (exists p) returns true if there is some stream for which the predicate returns true. This works because if the predicate is total, then there must be some bound on the initial segment of the stream that it examines.

The auxiliary function (epsilon p) returns a stream for which p holds, if one exists, and an arbitrary stream otherwise. The auxiliary function (prefix b p) is like (epsilon p), but only considers streams beginning with b.

exists :: ([Bool] -> Bool) -> Bool
epsilon :: ([Bool] -> Bool) -> [Bool]
prefix :: Bool -> ([Bool] -> Bool) -> [Bool]

exists p = p (epsilon p)
epsilon p = prefix (p (prefix True p)) p
prefix b p = b : epsilon (\x -> p (b : x))

Here are some test predicates and a testing function.

pos i x = not (x !! i)
run i x = and (map not (take i x))
alt i x = take i x == take i (cycle [False,True])
fal i x = not (take i x == take i x)

test f i = (exists (f i), take (i+1) (epsilon (f i)))

And here are some test runs.

*Main> test pos 5
(True,[True,True,True,True,True,False,True,True])
*Main> test run 5
(True,[False,False,False,False,False,True,True,True])
*Main> test alt 5
(True,[False,True,False,True,False,True,True,True])
*Main> test fal 5
(False,[False,False,False,False,False,False,False,False])


Atypical Typing

Mark Jason Dominus' talk at OOPSLA 2008. This covers similar ground to my OOPSLA talk, but in many ways Dominus makes a better job of it than I did. And it sounds better coming from someone outside the Haskell community.

From computers to ubiquitous computing, by 2020

I haven't had the time to read this yet, but it seems worth a look. Includes articles by Andy Hopper, Jeanette Wing, Thomas Henziger, Ronald Rivest, and Robin Milner, among others.

DabbleDB and Widgenie

Two cool ways to play with data: DabbleDB and Widgenie.

Brokers with Hands on their Faces Blog

A sign of the times. Spotted by Cory Doctorow at Boing Boing.

Learn You a Haskell

A rather nicely illustrated Haskell tutorial. Thanks to Jeremy for the tip.

Method and Apparatus for Automatic Notification and Response Based on Communication Flow Expressions

I've always envied those that list patents on their cv. Now I can too!

Joanne J. Ordille, Thomas A. Petsche, and Philip L. Wadler. Method
and Apparatus for Automatic Notification and Response Based on
Communication Flow Expressions. US Patent no.: 7,436,947 B2. Date of
Patent: October 14, 2008.

Garbage Collection and the Dust Heap of History

[A post in honour of Blog Action Day.]

Last month, at the workshop Commercial Uses of Functional Programming (CUFP), one of the speakers described the use of Haskell for garbage collection. Not for reclaiming unused computer memory, but for programming an embedded processor in the hydraulic engine of a garbage truck. As he pointed out, every five-year old thinks working with garbage trucks is cool. I think its cool too. Twenty years ago, when we created Haskell, I would not have found it credible if you told me that in twenty years time it would be running in a garbage truck.

Indeed, twenty years ago, most practitioners in my field were avoiding garbage collection altogether—and now I am referring to reclamation of computer memory. They would tell you it was too slow and too inefficient, because they were used to C and C++. Then Java came along, and now garbage collected languages are the accepted norm.

Now let's shift time and subject. Three years ago, when I still felt new to my new home, the city of Edinburgh hosted the Make Poverty History march. It was wonderful to see folk converge from all over to push the cause to the G8 leaders, meeting nearby in Gleneagles. But the thing I enjoyed most was the audacity of the theme. Make Poverty History. Not, Let's Reduce Poverty. But, Let's Eliminate Poverty Completely. No person lacking water, food, shelter, education.

Of course, it seems impossible. And as time goes by, and the G8 leaders fall further behind the Millenium Goals they set themselves, it seems less likely still. But, as I hope the technical stories above show, sometimes what seems impossible one day seems common wisdom the next.

No better example exists than recent events. Today's Daily Telegraph notes that the UK, US, and Europe are spending two trillion pounds (£2,000,000,000,000) to bail out the banks. Socializing banks was unthinkable a year ago. Now everyone is doing it.

And for less than two trillion pounds we could put poverty on the ash heap of history.

Many Eyes

A web site devoted to tools for visualization. Some neat stuff here! To the left, a visualization of the words spoken by John McCain in his acceptance speech at the Republican Convention.

Provenance semi-rings

One joy of my recent visit to Penn (see below) was a chance to look at recent work by Val Tannen and others on a generalized model of provenance. Reading these papers was the perfect way to brighten up my trip home. Truly elegant.

Todd J. Green, Grigoris Karvounarakis, Val Tannen. Provenance semirings. PODS 2007, Beijing, China.

J. Nathan Foster, Todd J. Green, Val Tannen. Annotated XML: queries and provenance. PODS 2008, Vancover, Canada.

Combining Events And Threads For Scalable Network Services

Last week, I enjoyed a visit to Penn for Nate Foster's PhD proposal. They have a great language group, and I had many enjoyable discussions. Many thanks to Nate Foster, Steve Zdanceowic, Benjamin Pierce, and everyone else for hosting my visit.

I also got to read some great papers I might otherwise have missed. Here's one, another in my next post.

Peng Li and Steve Zdancewic. Combining Events And Threads For Scalable Network Services. In Proc. 2007 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), pages 189-199, 2007.

Mandelbrot Maps

My MSc student, Iain Parris, has put together a brilliant web-based app for viewing Mandelbrot and Julia curves in real time. It lets you move about a point on the Mandelbrot set, and displays the corresponding Julia curve in real-time. There are other apps that perform similarly, but this is the only one I've seen that provides real-time response. Try it out!

Caml Trading

Caml trading – experiences with functional programming on Wall Street
by Yaron Minsky and Stephen Weeks
Journal of Functional Programming, Volume 18, Issue 04, July 2008, pp 553-564

Functional programmers are always keen to gather evidence that it is actually of use in the 'real world'. Jane Street Capital, by adopting O'Caml as the language in which they write the programs that earn them so much money, has provided one of the clearest demonstations. Yaron Minsky delivered a brilliant invited talk to this effect at POPL 2008, and I'm delighted to see that he and Steven Weeks have now published a companion article for JFP.

An error in a financial program of this kind can wipe out a firm's profits for the year in a few seconds, so reliability is a concern. The partners of Jane Street review the code themselves, and this turned out to be one of the major factors influencing the adoption of Caml.

I thought their comments on OO programming were of interest.

When we first tried switching over from VB to C#, one of the most disturbing features of the language for the partners who read the code was inheritance. They found it difficult to figure out which implementation of a given method was being invoked from a given call point, and therefore, difficult to reason about the code. It is worth mentioning that OCaml actually does support inheritance as part of its object system. That said, objects are an obscure part of the language, and inheritance even more so. At Jane Street, we almost never use objects and never use inheritance. We use standard functional programming techniques and code reviewers find that style more comprehensible. In particular, they can reason by following static properties of the code (module boundaries and functor
applications) rather than dynamic properties (what class an object is).

I've had similar thoughts about the perils of inheritance, but this is one of the few places I've seen them documented.

Welcome to Scotland, Neil, Patricia, and Conor!

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

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

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

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

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.

Fun with correlation and citations

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

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

AOSD 2008, Brussels

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

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

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

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

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

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

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

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.