July 31, 2010

Big Lambda




Illustration and first page of the story "Missing Out" by Leila Aboulela, in Granta no. 111. The protagonist is a young Sudanese postgrad math student in London.

March 7, 2010

What ARE anamorphisms

So I got sucked into editing the wikipedia page for anamorphisms, which was a mess: it didn't define the concept itself, except to say that it's a generalization of unfolds, and allude to category theory; it had duplicated code, but treated the duplicates as different, and was generally jargon-heavy and not very helpful.

But while fixing it, I got stuck on a puzzle: what exactly is an anamorphism?

Is an anamorphism a higher-order unfold operator? Or is it any function which is defined by partially applying such an operator? Or a function that is defined using a certain syntactic pattern, corresponding to an unfold operator? Or any function at all that could be so defined?

In the almighty "Programming with Bananas, Lenses, Envelopes and Barbed Wire," they seem to use "anamorphism" to refer to a function defined by a certain syntactic pattern. It's a question of interpretation, but they don't seem to define it as a higher-order function, exactly: the text posits some pre-existing operators and then the code sample, which takes just one argument (the "seed" value to unfold from), uses those posited operators.

It seems natural to me to use "anamorphism" to refer to the (unique) unfold operator for a given ADT, and likewise for "catamorphism" and fold. We still have the plural "anamorphisms," since we have many types with such operators. And, I'm not sure to what extent a function is intrinsically "an anamorphism" in Meijer, et al.'s sense. Of course, it is intrinsic whether a function can or cannot be defined that way; but when we start using the whole bag of bananas, lens, envelopes and barbed wire, I think we get multiple ways to define many functions, so it's less intrinsic.

I'd like to hear what others think: What are anamorphisms? Please comment!

March 1, 2010

Simply adding lambda won't make your rewrites diverge

I've been working on trying to extend a result from my thesis, having to do with strong normalization of a certain higher-order rewrite system, but its proof is very complicated, so I've been working on simplifying it.

Along the way I found a paper by Mitsuhiro Okada from 1989 which proves strong normalization for the combination of STLC with any first-order term-rewriting system. But this paper is hard to read because it has strange notations and concepts and says things like, "If a part s[*/x1, ..., */xn, */y] of t belongs to the cap then the part s[*/x1, ..., */xn, */y] also belongs to the cap." Say what?

I knew I could prove the same result using the Tait-Girard method (the same basic approach Okada takes) in a more straightforward way—at least to me. So I did, and here it is for future reference: "Simply adding lambda won't make your rewrites diverge."

February 27, 2010

Krugman

Economist Paul Krugman, as portrayed in this week's New Yorker profile, reminds me a lot of a computer scientist. MacFarquhar explains one of Krugman's economic ideas, namely that locations specialize economically—cars in Detroit and chips in Silicon Valley—and reports this interesting reaction to it:

'I explained this basic idea to a non-economist friend, who replied in some dismay, "Isn't that pretty obvious?" And of course it is.' Yet, because it had not been well modelled, the idea had been disregarded by economists for years.
(MacFarquhar, "The Deflationist." The New Yorker, March 1, 2010.)

Much of what we academics do (in computer science and, apparently, in economics) is to take an intuitive idea and make it precise—modelling it, if you will. Those who simply think intuitively may have already absorbed the idea and treat it as old hat—but the model, by making it more precise, illuminates it further and more securely and can lead to new inspirations.

MacFarquhar adds another interesting idea here:

His friend Craig Murphy, a political scientist at Wellesley, had a collection of antique maps of Africa. ... Sixteenth-century maps of Africa were misleading in all kinds of ways, but they contained quite a bit of information about the continent's interior—the River Niger, Timbuktu. Two centuries later, mapmaking had become much more accurat, but the interior of Africa had become a black. As standards for what counted as a mappable fact rose, knowledge that didn't meet those standards—secondhand travellers' reports, guess hazarded without compasses or sextants—was discarded and lost. Eventually, the higher standards paid off—by the nineteenth century the maps were filled in again—but for a while the sharpening of technique caused loss as well as gain.

I'm intrigued by this idea that higher standards of precision can cause us to 'forget' disciplinary knowledge, material that no longer meets the standards. Of course, the higher standards are all about eliminating 'knowledge' that isn't actually correct. But some of it, perhaps, is correct, and anyway there's an outer shape to the knowledge that is useful: after all, there was still a River Niger even if the mapmakers didn't know exactly where it flowed.

This might happen in computer science, too. I think of Don Knuth's penchant for reading antique sources describing algorithms from pre-modern times.

There might be inspiration in the older, less-precise knowledge of one's field: it might be a source of ideas to be modelled.

February 16, 2010

What I'm doing now

So what I do lately is I work for a company in Cambridge, MA that has a big XQuery engine for searching "semi-structured" databases. That is, we use language technology to allow people to write nifty searches.

I had some other interesting job offers, but I took this one because (a) it was in the Boston area, which is where I wanted to be at the time and (b) I wanted to get behind one central product and contribute some programming-language knowledge to it. I was surprised to discover a company that would let me do both.

As part of what how we're improving the product just now, we're building a parallelizing compiler for relational algebra—roughly the sort of stuff that titilates me as a langauge engineer, and tangentially (at least) related to some of my thesis work.

Since it's a company trying to compete against others, I probably won't be blogging much about what I'm doing at work, but I still hope to keep this blog active and post researchy notes here.

January 7, 2010

Time-saving proposal to improve the reviewing process

Proposal: As an academic reviewer, you should always vote to publish a paper, without reading it, even if it is a tedious waste of time.

The time-saving benefit of this strategy is subtle to grasp but significant. You see, only the reviewers of a paper "must" read it, while everyone else will discard it if it's boring. By voting to publish, you waste no one else's time—but the time you save is your own. If every reviewer did this, the time saved would allow us all to do far more research!