Wadler's Blog

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.

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 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 (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?

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?

Two things that struck my eye on the interweb.

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!