Clay Shirky on Creativity
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.Philip Wadler (2007), The Girard-Reynolds isomorphism (second edition), Theoretical Computer Science 375(1-3):201-226.
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).
Nick Hanauer’s TED Talk on Income Inequality
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
OCaml for the Masses by Yaron Minsky, from the Nov 2011 CACM. Is material on FP for developers the new trend?
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!