Lambda Calculus, Then and Now, by Dana Scott

Last May, I was honoured to be invited to speak at Princeton's Turing Centennial Celebration.  My talk was scheduled between Dana Scott and Leslie Valiant.  Dana's talk was not an easy act to follow.  The talk summarises the history of lambda calculus from 1930 to the present, a resource for future scholars.  I'm pleased that a version is now available.  Dana asked me to indicate he would be pleased to receive any suggestions or criticisms.

In Praise of Impractical Programming

Neil Harris, In Praise of Impractical Programming.

Although it’s become a cultural mainstay now, I still remember when I first saw that thick book — the one with the wizard on the cover — about a school for magic where wonders are easily conjured by those who know the proper spells. Of course, I’m talking about the Structure and Interpretation of Computer Programs. There was that other book with the spells, but the “Wizard Book” sincerely claimed to teach magic.

For the past few years, I’ve been working as a software developer in the newsroom, where perceptions of my kind have changed from novelty to a necessity. Recognizing this, some journalism schools now even require programming courses to teach students practical skills with databases or web frameworks. It’s thrilling to contemplate a generation of web-hacking journalists — but I wish we could somehow squeeze a little magic into their course load.

 Spotted by Conal Elliott (@conal), via twitter.

Tsuru Capital, Haskellers @ Gonpachi

Clearing my desk, I spotted a souvenir of an event I had meant to blog at the time. Tsuru Capital is a financial firm specialising it automated trading.

At the moment our focus is mainly on option market-making strategies in active listed markets. Our edge is in superior strategies and efficient low latency execution. We use the Haskell programming language almost exclusively since we believe it gives the best combination of high-level cleanliness, execution safety and high performance.

Similar to Jane Street, but newer and smaller, with OCaml replaced by Haskell. Tsuru kindly sponsored a reception for the Haskell community during ICFP, on Wednesday 21 September 2011. Judging by the quantity and quality of sushi on offer, they are doing well in their early days. The reception was held at Gonpachi, which I'm told is the inspiration for the restaurant scene in Kill Bill.

Clay Shirky on Creativity

Clay Shirky speaks on creativity. My favorite remark:

When I think about groups and institutions grappling with creativity, particularly institutions, one of the odd things about institutions, and the bigger they are the more they have a problem with this, is that they often reverse the second law of thermodynamics: it becomes easier to start doing something than to stop doing something. A big part of it is knowing when to stop doing stuff that used to work but that's not working anymore. ... Getting in the habit of understanding what's stopped working and stopping doing that is huge input to any creative organisation. Because in many cases it is not filling the helium balloon but cutting off the sandbag that gets you aloft.

My university often comes up with new things for staff to do, what a boon if they also started to think of things for staff to stop doing.

Proofs for Free: Parametricity for dependent types

In a series of papers, published 2001-2007, I explained Reynold's Abstraction Theorem as a mapping from System F to a suitable logic, and Girard's Representation Theorem as a mapping from the logic back into System F, with the two mappings forming an embedding-projection pair.  Recently, Bernardy, Janson, and Paterson have described a lovely generalisation of this idea to an arbitary Pure Type System (PTS).  An illuminating part of their construction is that given one PTS, they can construct another suitable for use as the logic of the first.  The journal version of their work arrived in my postbox this morning.  Neat stuff!

Jean-Philippe Bernardy, Patrik Janson, and Ross Paterson, Proofs for Free: Parametricity for dependent types, Journal of Functional Programming 22(2):107-152, March 2012.

Studies of parametricity for System F and its variants abound in the literature, starting with the seminal paper by Reynolds (1983), where the polymorphic semantics of System F types is captured in a suitable model.
We use here a more syntactic approach, where the expressions of the programming language are (syntactically) translated to formulas describing the program. This style was pioneered by Mairson (1991) and used by a number of authors, including Abadi et al. (1993), Plotkin & Abadi (1993), and Wadler (2007). In particular,Wadler (2007) gives an insightful presentation of the abstraction theorem, as the inverse of Girard’s (1972) Representation theorem: Reynolds (1983) gives an embedding from System F to second-order logic, while Girard (1972) gives the corresponding projection. Our version of the abstraction theorem differs in the following aspects from that of Wadler (2007) (and to our knowledge all others):
1. Instead of targeting a logic, we target its propositions-as-types interpretation, expressed in a PTS.
2. We abstract from the details of the systems, generalising to a class of PTSs.
3. We add that the translation function used to interpret types as relations can also be used to interpret terms as witnesses of those relations.
The question of how Girard’s projection generalises to arbitrary PTSs naturally arises, and is addressed by Bernardy & Lasson (2011).

Philip Wadler (2007), The Girard-Reynolds isomorphism (second edition),   Theoretical Computer Science 375(1-3):201-226.

Nick Hanauer’s TED Talk on Income Inequality

Nick Hanauer has accused TED of censorship for failing to post his talk arguing that low taxes on the 1% do not foster job creation.  Censorship is a bit harsh---failing to give someone billing is not censorship---but it may well be correct to say that TED failed to post it for fear of offending its affluent attendees.  After the fuss, TED released the video on YouTube, but not on their home page, and not up to their usual production standards.  I think it deserves a broader audience, so I post it here.   A short five minutes of sense.  Background on the argument at Salon and full text of the presentation at The Atlantic.  Thanks to Maurice Naftalin for bringing this to my attention.

Ethical Identity Validation

Ethical Identity Validation (subtitle: A proposed weapon against both Terrorism and Tyranny) proposes apps in phones as an alternative to identity cards.  Written by a fellow named Harry Stottle, who may be a pseudonym and at times appear borderline crackpot.  But the basic plan for an identity escrow service seems eminently reasonable.  Anyone know who Harry Stottle is?  Or where to find sensible discussions of alternatives to id cards?

OCaml for the Masses

Here's one I meant to blog earlier: OCaml for the Masses by Yaron Minsky, from the Nov 2011 CACM.  Is material on FP for developers the new trend?

Surfin'

Two things that struck my eye on the interweb.

Research and the Economy

Alex Simpson's inaugural raised the question of to what extent fundamental research impacts the economy.  (And to what extent we should use that to justify fundamental research.)  My own belief is that fundamental research has a hugely positive economic impact in the long term, but I cannot produce stacks of evidence to justify that view.  After the talk, Sean Matthews mentioned the theory that Germany's economic dominance can be traced back to its investment in research universities in the 19th century, though again he could not cite chapter and verse.  I'd be grateful if readers know of sources that back (or refute) these claims.  Comments, please!