Why is a monad like a writing desk?

A presentation by Carin Meier at Clojure/West.  Only time I've been accused of writing poetry.  Spotted by Mitch Wand.

Programming Language Tag Clouds

 

Bernard Lambeau created the Programming Language Tag Cloud, reminiscent of Wordle.  It is based on texts submitted by the public; contribute today!  Above, languages currently covered, below Haskell, C, Clojure.  Random juxtaposition endows Haskell with a 'wonderful experimental semantics' and a 'sophisticated ecosystem of monads'.

Good luck

From fail.nl.

Kohei Honda, 1959—2012

Kohei Honda died of a stroke on Monday 3 December 2012.  It was sudden, and many of us still have not taken it in.  My recent paper is a direct descendant of Kohei's work on session types, and I had been fortunate to have the opportunity to work with him on a grant proposal in the last few months.  I spent some time liaising with the W3C on XML and Sun on Java, so I can appreciate the far greater effort involved in Kohei's work liasing with the W3C on WS-CDL, with Cognizant, Red Hat, and VMWare on Scribble and Savara, and with the OOI, all on applications of session types.  Few academics both make deep technical contributions and successfully communicate these to practitioners.  I am sure the theoretical computing community will continue to build on his work, and I hope more computer scientists will emulate his efforts to liaise with practitioners, which should serve as a role model for us all.

Tech Mesh 2012

Tech Mesh was my second developer conference this year, the first being QCon.  While QCon had a track devoted to functional programming, Tech Mesh was devoted to 'alternative programming', meaning FP, in its entirety, with keynotes on Haskell, Clojure, and Erlang, and other talks covering Scala and F#.  A highlight for me was meeting Rich Hickey.  I am impressed that in five years he has taken Clojure to the same place it has taken Haskell twenty years to reach.  Another highlight was seeing Joe Armstrong, Robert Virding, and Mike Williams deliver a joint keynote.  Slides for the Haskell keynote (Peyton Jones, Hughes, and Wadler) are here, and for my other talk are here.

Another pleasure was meeting Clojure developer Bodil Stokke, who was wearing a shirt reading `A monad is just a monoid in the category of endofunctors. What's the problem?'  I'm grateful to Pelotom for an answer on StackOverflow with a definitive explanation of this statement and its spurious connection to myself. 

Avnery: The correct name for this war is "Operation Short Memory"

From Gush Shalom:

The name chosen for the new war in Gaza is "operation Cloud Pillar". A far more appropriate name would have been "Operation Short Memory" Said former Knesset member Uri Avnery, Gush Shalom activist. "Prime Minister Netanyahu is counting on the public's short memory. Netanyahu counts upon people forgetting that dozens and even hundreds of "liquidations" had been carried out and they did not solve any problem - always there was somebody replacing those who were killed, and more than once the new one was more capable and more radical. Netanyahu counts on people not remembering that four years ago Israel went to war in Gaza, killing 1300 civilians in three weeks – which otherwise did not make any significant change in the situation. Netanyahu counts on people failing to remember that just yesterday morning the media reported on people in the communities of the South heaving a sigh of relief at the complete cessation of missiles from Gaza.

"Binyamin Netanyahu and Ehud Barak have taken the decision - for the second time in a row the State of Israel will conduct general elections under the shadow of war in the Gaza Strip. The cease-fire which already started to stabilize had been broken and shattered to pieces. The inhabitants of te communities of southern Israel, who just started to breathe freely, are sent right back to air raid alarms and the running to shelters.

At the price of great suffering on both sides of the border, the government's aim had been accomplished: the social issues, which threatened to assume prominence in these elections, have been pushed aside and removed from the agenda of the elections campaign. Forgotten, too, is the brave attempt of Mahmud Abbas to address the Israeli public opinion. In the coming weeks, the headlines will be filled with constant war and death, destruction and bloodshed. When it ends at last, it will be revealed that no goal has been achieved and that the problems remain the same, or perhaps got worse."

Hurricane Sandy's Fibonacci Golden Spiral

By JIMWICh, via Boing Boing.

Animated Factorisation Diagrams

From Brent Yorgey's Factorisation Diagrams comes Stephen von Worley's (Data Pointed) beautiful and hypnotic Animated Factorisation Diagrams.  Via Conor McBride (@pigworker).  Virgin wanted me to confirm I was over 18 before it would display the animation on my phone.  Number porn?

Petition: Secure the EU Research and Innovation Budget

You may wish to sign this petition to heads of the EU to preserve the research budget.  It complements the open letter of 42 European Nobel Laureates and 5 Fields Medallists recently published in the major European newspapers.

The next summit of the EU heads of states on 22-23 November 2012 will be a decisive step in determining the EU research budget for the next seven years. The conditions are not favorable: the financial crisis has put severe constraints on the national budgets and several countries, in particular the "net-payers", are demanding cuts on the total EU budget. Research and innovation will compete with other policy priorities.

Share and Enjoy: Nina Paley's Mimi and Eunice

I've just discovered Nina Paley's wonderful comic Mimi and Eunice. She encourages folk to copy it, so share and enjoy!

Philip Giraldi: Why I Dislike Israel

Philip Giraldi's Why I Dislike Israel tells it like it is:

The Israeli government is a rogue regime by most international standards, engaging as it does in torture, arbitrary imprisonment, and continued occupation of territories seized by its military. Worse still, it has successfully manipulated my country, the United States, and has done terrible damage both to our political system and to the American people, a crime that I just cannot forgive, condone, or explain away.

CH = PH

Two representations for lambda calculus terms are the Church representation, due to Thierry Coquand (left) and Gerard Huet (middle), let's call it CH, and PHOAS, due to Adam Chlipala (right), let's call it PH.  Here is a Haskell program giving both encodings, and showing they are interconvertible.  (The CH representation is called `finally tagless' by Carette, Kiselyov, and Shan, which is not the most perspicuous name; Atkey, Lindley, and Yallop point out the idea goes back to Coquand and Huet; PH was introduced by Chlipala.)

Unlocking Scotland's Potential

A new report from the NUS.

Findings

• At current rates it would take 40 years to reach fair and representative access in Scotland.
• Across Scotland, for every one student from the most deprived background recruited to university, there are 2.5 students from the least deprived background. However, at our institutions with the worst records on widening access (Edinburgh, Aberdeen and St Andrews), the ratio reaches 1 to 16.4 of most deprived to least deprived. At St Andrews the ratio reaches 1:28.
• It is by no means the rule that deprivation levels dictate participation rates, with many constituencies with high levels of deprivation with good records in terms of sending pupils to HE and vice versa.

This Land is Mine, by Nina Paley

Nina Paley, creator of Sita Sings the Blues and Copying is not Theft, has a new project.  You may want a scorecard.  Share and enjoy!

Dennis Ritchie memorial symposium

A note from Brian Kernighan on the symposium held in memory of Dennis Ritchie last month. I had the great honour to have Dennis and then Brian as my boss when I worked at Bell Labs. I particularly enjoyed Brian's talk on Dennis, below, where he focussed on Dennis as a writer.

It's unfortunate, but time marches on.  There was a gathering in honor of Dennis Ritchie's contributions at Bell Labs on Sept 7. It drew a large crowd, mostly Bell Labs alumni and present employees.  Several of us gave short talks, which eventually wound up on YouTube.

    Susanne Arney Intro:  http://youtu.be/5phgZAYzjx8
    David Patterson:  http://youtu.be/Bx8PL5sMD6o
    Brian Kernighan:  http://youtu.be/uxtKwJZbYr0
    Doug McIlroy:  http://youtu.be/Y-TrkYL0VtI
    Steve Fortune and the other Bell Labs researchers:
      http://youtu.be/1d4HrfFvIws
    Al Aho:  http://youtu.be/GfoSbffSIQ4
    Eric Schmidt:  http://youtu.be/3-gTXWhx1y8
    Lynn Ritchie:  http://youtu.be/7Zt50RpYs70
    John Ritchie:  http://youtu.be/E4h6WynJzjI
    Bill Ritchie: http://youtu.be/_BwVlHOpX10
    Artwork:  http://youtu.be/IjRPHdCWUQQ

Al did an especially good job, and the Ritchie segments reveal how talented the family is, along with some facets of Dennis's life that none of us ever knew.

Three remarkable films

This week I saw three films at the Take One Action film festival.  Studies that are deeply personal and political, all three are relevant, riveting, and remarkable, 

This is Not a Film:Jafar Panahi, an Iranian filmmaker, is under house arrest and under court order not to act or direct.  So without acting or directing, he documents his life, claiming that the result is not a film to comply with his court order. This film, the result, was smuggled into Cannes in a cake.

1/2 Revolution: the story of the Tahrir Square in Cairo and the ouster of Mubarak, from the point of view of five friends of mixed Arabic and European heritage.

5 Broken Cameras: Emad Burnat buys a camera to video his newborn fourth son, then feels compelled to document the struggle of his village Bil'in, to oppose the barrier erected by the Israeli's that cuts them off from the land they use for the livelihood.  His camera is destroyed by a bullet from an Israeli soldier's gun, so he buys another, and the story continues through protests, arrests, deaths, and five broken cameras. Emad himself attended the screening, and after the events of the film I was moved to see him present, now with a head of greying hair, still devoted to non-violence. The audience welcomed him with something I rarely see among stoic Scots, a standing ovation.

Clay Shirky: How the Internet will (one day) transform government

Clay Shirky explains how Github enables better arguments, with a detour into Scottish school lunches.

Brian Goetz on the future of Java

Brian Goetz, author of Java Concurrency in Practice, is leading Project Lambda, Oracle's effort to add lambda expressions to Java.   Below is an excerpt from comments he posted last year on the design.

Oracle's position is that Java must evolve -- carefully, of course -- in order to remain competitive. This is, of course, a difficult balancing act. It is my belief that the best direction for evolving Java is to encourage a more functional style of programming. The role of Lambda is primarily to support the development and consumption of more functional-like libraries; I've offered examples such as filter-map-reduce to illustrate this direction. There is plenty of evidence in the ecosystem to support the hypothesis that, if given the tools to do so easily, object-oriented programmers are ready to embrace functional techniques (such as immutability) and work them into an object-oriented view of the world, and will write better, less error-prone code as a result. Simply put, we believe the best thing we can do for Java developers is to give them a gentle push towards a more functional style of programming. We're not going to turn Java into Haskell, nor even into Scala. But the direction is clear.

Thanks to Maurice Naftalin for pointing me to these comments, in response to some questions I raised regarding his FAQ.

Lambda for Java: the FAQ

Java 8 will, at long last, contain lambda expressions. Maurice Naftalin, my co-author on Java Generics and Collections, has started a Lambda FAQ.  Have a look, your comments may feed into the 2nd edition of JGaC.

ICFP 2012

Thanks to the organisers of ICFP 2012, and to Malcolm Wallace and his assistants for videoing and posting talks rapidly. For me, the emergent theme was the rise of DSLs.  Kunle Olukotun's keynote (video above) argued that DSLs are reaching maturity as a technology for programming parallel and heterogeneous hardware (although less was said on the equally important question of distributed systems).  Lee Pike et al's Experience report: a do-it-yourself high-assurance compiler presented a case study of a real-life DSL used for monitoring safety on aircraft, and a series of techniques to implement DSL's at low cost while increasing confidence that the implementation is correct, and another whole session was devoted to techniques for implementing DSELs (1 2 3).  Olivira and Cook's Functional programming with structured graphs applies PHOAS to representing cyclic structures.  Nothing to do with DSL's, below is a link to the video of my talk, Propositions as Sessions.

CUFP tutorials announced: Haskell (by Jeremy Gibbons and Simon Marlow), F# (by Tomas Petricek), Scala, and more!

Faith, Evolution, and Programming Languages

I just received the following,

Hi Philip,

Your presentation Faith, Evolution, and Programming Languages, published on Aug 9, 2012 and recorded at QCon London 2012 has generated 10,198 page views so far. Congratulations!  Roxan Bacila, Community Contributions Facilitator. 

Star Ratings

Handy information for the Edinburgh Festivals, from XKCD.  I give 4 1/2 stars to Coalition, and four stars to Tubular Bells for Two, Blues!, and The Bongo Club.

Is it Anti-Semitic to call it Apartheid?

Jonathan Ben-Artzi, a mathematician at Cambridge University, refusenik, and nephew of Israeli Prime Minister Benjamin Netanyahu, argues in an interview in favour of classifying Israeli attitudes towards Palestinians as apartheid.

You studied at Brown University. I’m sure you’re familiar with our political discourse here in the United States. Comparing Israeli policies toward the Palestinians with apartheid in South Africa inevitably invites charges of anti-Semitism and extremism.

It has always seemed like a correct analogy to me, in that Israel is facing demographic pressures, and has set up a quasi state with no real sovereignty. They’re pretending that that quasi state is in fact independent. In apartheid South Africa these were called Bantustans.

[Update: My thanks to Ohad Kammar for pointing out I misread the above: the second paragraph is not Ben-Artzi's answer, but part of the interviewer's question, which makes the view expressed of considerably less interest. My apologies for the error.]

How to write good

Useful rules from Frank L. Visco and William Safire.  Spotted via a post from Perdita Stevens.

The truth wears off

The truth wears off, Jonah Lehrer, The New Yorker, 13 December 2010.  Recommended by Amer Diwan in his keynote at PLDI 2012.  It's hard to establish an effect by rigorous experiment.  This article describes cases, mostly medical, where a demonstrated effect becomes harder to replicate as time passes.

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!

What Must be Said

Gunter Grass continues to face accusations of antisemitism for his poem `What Must Be Said', which predicts that very reaction.

But why do I forbid myself
to name that other land in which
for years—although kept secret—
a usable nuclear capability has grown
beyond all control, because
no scrutiny is allowed.

The universal silence around this fact,
under which my own silence lay,
I feel now as a heavy lie,
a strong constraint, which to dismiss
courts forceful punishment:
the verdict of “Antisemitism” is well known.
...
Why is it only now I say,
in old age, with my last drop of ink,
that Israel’s nuclear power endangers
an already fragile world peace?

Commercial Uses of Functional Programming 2011

Kudos to Anil Madhavapeddy (U. Cambridge), Yaron Minsky (Jane Street Capital), and Marius Eriksen (Twitter) for producing an excellent summary of CUFP 2011 and publishing it in JFP (22(1):1--8).  CUFP is valuable, and this readable and compact summary increases its value.  I hope it becomes a JFP tradition.

Why Programmers Should Use the Haskell Language Now

A post at e-Week, based on Andy Adams-Moran's presentation at Microsoft's Lang.NEXT. Thanks to Vladimir Gapayev for the pointer.