Towards Independence

As an experiment, I have created a separate blog for political posts: Towards Independence.

Labels: ,



Bright Club

Tuesday 25 November at The Stand Comedy Club, I will be part of the line up at Bright Club, speaking on the subject of 'Turingery'. Bright Club is stand-up by academics---we are trained professionals; don't try this at home! Doors open 7:30pm, show starts 8:30pm. The Stand is at 5 York Place, Edinburgh, EH1 3EB. Tickets £5 at the door or online.

Labels: , ,



CITIZENFOUR showing in Edinburgh

CITIZENFOUR, Laura Poitras's documentary on Edward Snowden, sold out for its two showings in Edinburgh. The movie is rated five-stars by the Guardian ("Gripping"), and four-stars by the Independent ("Extraordinary"), the Financial Times ("True-life spy thriller"), the Observer ("Utterly engrossing"), and the Telegraph ("Everybody needs to see it").

Kickstarter-like, OurScreen will arrange to show a film if enough people sign up to see it. I've scheduled a showing:

Cameo Edinburgh, 12 noon, Tuesday 2 December 2015
cost: £6.80 Book tickets from OurScreen.

If 34 people sign up by Sunday 23 November, then the showing will go ahead.

Labels: , ,



Save our Universities

An open letter to my MSPs. Support and suggestions for how to carry
this forward as a campaign are solicited.

Dear Gavin Brown, Sarah Boyack, Alison Johnstone, Kezia Dugdale,
Cameron Buchanan and Neil Findlay,

I write to ask your help to preserve a secure future for Scottish

Academics for all UK universities, including those in Scotland, have
faced falling wages and falling pensions over many years.  "The real
wages of academics have fallen by 13% since 2008, one of the largest
sustained wage cuts any profession has suffered since the Second World
War." So wrote Will Hutton in the Guardian, October 2013 [1].

In 2011, Universities UK imposed vastly reduced pensions on new
hires. Old hires who pay into the pension fund for forty years receive
a pension of one-half their final salary; new hires who do the same
receive a pension of one-half their average salary. Basing pensions on
average rather than final salary may be sensible, but to do so with no
adjustment in multiplier suggests employers are using this as an
excuse to slip in a large cut; it means new hires receive about 2/3
the benefits received by old hires. All staff also suffered other cuts
to pensions: additional caps and less good adjustment for inflation.
At the time, it was predicted that within a few years old hires would
be moved to the inferior scheme for new hires, and that is what has
now come to pass. [2]

Universities UK argue that the reductions are necessary to avoid a
deficit, but their claim has been widely criticised. Notably, a group
of prominent statisticians point out Universities UK inflated the
deficit by assuming a buoyant economy when predicting future salaries
but assuming a recession when predicting investment returns. [3]

A strong university system is one of the jewels in the crown of the
UK, and particularly for Scotland.  That excellence is a huge driver
of innovation and growth. If Scotland reduces its investment in
universities, it won't be long before we feel that loss throughout the
economy. [4,5]

Scotland has a University system second to none, and to keep it strong
we need pay and pensions that attract and retain the best minds
throughout the world.  We must have a system that is fair to both: old
hires must retain attractive conditions; new hires must have the bad
deal imposed on them in 2011 rolled back. Speaking as an old hire, I'd
settle for a small cut in pension if it meant bringing new hires onto
the same level: we must keep the system strong for the future.

The UCU has gone on strike over the issue (suspension of assessment,
which it hopes will minimise disruption for students). But UCU is
unlikely to succeed without political support.

I write to ask you, as my representative in the Scottish parliament,
will you direct the Scottish Funding Council to make fair treatment
for academics in Scottish Universities, both new hires and old, a top

Thank you for your consideration. Yours,

-- Philip Wadler
Professor of Theoretical Computer Science
School of Informatics
University of Edinburgh

[1] http://www.theguardian.com/commentisfree/2013/oct/13/england-leave-funding-universities-students
[2] http://www.theguardian.com/education/2010/nov/23/oxbridge-pensions-academics-protest-united
[3] http://www.theguardian.com/higher-education-network/blog/2014/oct/29/marking-boycott-why-are-academics-protesting-about-pensions
[4] http://www.universities-scotland.ac.uk/index.php?mact=News,cntnt01,detail,0&cntnt01articleid=156&cntnt01returnid=23
[5] Royal Society of Edinburgh, Enlightening the Constitutional Debate, Science and Higher Education, p177--198,

Labels: , , ,




SNAPL will take place 3-6 May 2015 at Asilomar.
SNAPL provides a biennial venue to focus on big-picture questions, long-running research programs, and experience reports in programming languages. The ideal SNAPL paper takes one of two forms:
  • A promising idea that would benefit from discussion and feedback.
  • A paper about an ongoing research project that might not be accepted at a traditional conference.
Examples include papers that
  • lay out a research roadmap
  • summarize experiences
  • present negative results
  • discuss design alternatives
SNAPL is interested in all aspects of programming languages. The PC is broad and open-minded and receptive to interesting ideas that will provoke thought and discussion.
Interesting papers would combine the specific with the general. Submissions are limited to five pages (excluding bibliography), and must be formatted using ACM SIG style. The final papers can be up to 10 pages in length. Accepted papers will be published on an open-access site, probably arXiv CoRR.
To encourage authors to submit only their best work, each person can be an author or co-author of a single paper only. SNAPL will prefer experienced presenters and each submission must indicate on the submission site which co-author will present the paper at the conference.
SNAPL also accepts one-page abstracts. Abstracts will be reviewed lightly and all submitted abstracts will be published on the SNAPL 2015 web page. Authors of selected abstracts will be invited to give a 5-minute presentation at the gong show at the conference.
SNAPL is unaffiliated with any organization. It is a conference for the PL community organized by the PL community.

Important Dates

Submission: January 6, 2015
Decisions announced: February 20, 2015
Final versions due: March 20, 2015
Conference: May 3-6, 2015

Labels: ,



Errata, please

This is a space where you can leave comments describing errata in any of my published papers. Please include bibliographic details of the paper, and a link to where the paper appears on my web page if you can. Thank you to Dave Della Costa for volunteering the first entry and inspiring the creation of this post, and to all who utilise this space to record and correct my errors for posterity.

Labels: , ,



Composable Queries in F# 3.0

James Cheney speaks to the F#unctional Londoners meet-up about our F# library that implements A Practical Theory of Language-Integrated Query.

Labels: , ,



The military and the referendum.

Many readers will have heard about Lord Dannat in the Telegraph arguing a vote for independence will dishonour Scotland's war dead.

Perhaps not as many will have heard that Jimmy Sinclair (the oldest surviving Desert Rat, aged 102), Colin May (Lieutenant Commander, Faslane), and sixteen others have written a letter slamming Dannat; at least, I didn't hear until this morning. "How dare he take their sacrifice in vain and try to turn it to political advantage?"

Both sides are reported by the BBC, though the headline mentions only one. (More #bbcbias?)

Labels: , ,


The case for Europe

Readers of this list will know that I don't always see eye-to-eye with Alex Salmond. Nonetheless, I think he put the case for Europe well this morning on the Today Program.
In a BBC interview just the other night, a spanish minister being
interviewed by Kirsty Wark despite being invited three or four times
refused to say that Spain would attempt to veto Scottish
membership. And the reason for that of course is that the Spanish
government have already said that in the circumstance of a consented
democratic referendum, as they put it, Spain would have nothing to say
about it.

We can go through legal opinion and expert opinion as much as we like.
I think the answer is in four figures: 1, 20, 25, and 60.

1% is the percentage of Scotland's population compared to the European Union.

20% is the percentage of the fish stocks of the entire European Union.

25% is the percentage of the renewable energy of the entire European Union offshore.

And 60% is the oil reserves that Scotland has.

Anyone who believes that a country [with these resources] is not
going to be welcome in the wider Europe doesn't understand the process
by which Europe accepts democratic results and that Scotland has a
huge amount of attractiveness to the rest of the European continent.

You can hear the original here, the relevant segment starts at around 8:00.

Labels: , ,



The British Biased Corporation

Scandalous! Nick Robinson asks Alex Salmond a question, and Salmond takes seven minutes to answer in detail.

On the evening news, Nick Robinson summarises Salmond's answer in a few seconds as 'He didn't answer'.

(Above spotted via Arc of Prosperity.)

And today, this.
I used to be a supporter of the BBC, but it's getting harder and harder to justify.

Labels: , ,


Dinna fash yersel — Scotland will dae juist fine!

One relentless lie behind 'No' is that Scotland is too wee to make it on its own, counterexamples such as Denmark, Sweden, Singapore, and Hong Kong being conveniently ignored. May this post from Thomas Widmann, a Dane residing in Scotland, help to dispel the disinformation. 
Pick a random person from somewhere on this planet. Ask them to name an alcoholic drink from Scotland, and it’s very likely they’ll reply “Whisky”. Ask them to name one from Denmark, and they’ll probably be tongue-tied. (They could answer “Gammel Dansk” or “Akvavit”, but they’re just not nearly as famous as whisky.)

Now repeat the exercise, but ask about a food item. Again, it’s likely they’ll have heard of haggis but that they’ll be struggling to name anything from Denmark.

Now try a musical instrument. Bagpipes and … sorry, cannot think of a Danish one.

A sport? Scotland has golf, of course. Denmark can perhaps claim ownership of handball, but it’s not associated with Denmark in the way that golf makes everybody think of Scotland.

A piece of clothing? Everybody knows the kilt, but I’d be very surprised if anybody can name one from Denmark.

A monster? Everybody knows what’s lurking in Loch Ness, but is there anything scary in Denmark?

The only category where Denmark perhaps wins is toys, where Lego surely is more famous than anything from Scotland (but many people don’t know Lego is from Denmark).

Denmark is also well-known for butter and bacon, of course, but these aren’t Danish in origin or strongly associated with Denmark in people’s minds.

Several famous writers and philosophers were Danish (e.g., Hans Christian Andersen and Søren Kierkegaard), but Scotland can arguably list more names of the same calibre, and the Scottish ones wrote in English, which makes them much more accessible to the outside world.

Scottish universities are also ranked better than the Danish ones in recent World rankings.

Finally, Scotland has lots of oil and wind, water and waves. Denmark has some, but not nearly as much, and most other countries have less than Denmark.

Because of all of this, I don’t worry about the details when it comes to Scottish independence. If Denmark can be one of the richest countries on the planet, of course Scotland can be one too.

Yes, there might be a few tough years while the rUK are in a huff and before everything has been sorted out. And of course there will be occasional crises in the future, like in any other country.

However, unless you subscribe to the school that Denmark and other small countries like Norway and Switzerland are complete failures because they don’t have nuclear weapons and a permanent seat on the UN’s Security Council, there’s simply no reason to assume Scotland won’t do exceptionally well as an independent country in the longer term.

So I’m not worried. Of course there are many details to sort out, but at the end of the day everything will be fine. Scotland will be a hugely successful independent country. Dinna fash yersel!

Labels: , ,


Krugman vs. Stiglitz, now with added Stiglitz

My last post quoted Joe Stiglitz, indirectly, to refute Paul Krugman's fear mongering. Now the man himself has spoken in the Sunday Herald.
As Scotland contemplates independence, some, such as Paul Krugman, have questioned the "economics".

Would Scotland, going it alone, risk a decline in standards of living or a fall in GDP? There are, to be sure, risks in any course of action: should Scotland stay in the UK, and the UK leave the EU, the downside risks are, by almost any account, significantly greater. If Scotland stays in the UK, and the UK continues in its policies which have resulted in growing inequality, even if GDP were slightly larger, the standards of living of most Scots could fall.

Cutbacks in UK public support to education and health could force Scotland to face a set of unpalatable choices - even with Scotland having considerable discretion over what it spends its money on.

But there is, in fact, little basis for any of the forms of fear-mongering that have been advanced. Krugman, for instance, suggests that there are significant economies of scale: a small economy is likely, he seems to suggest, not to do well. But an independent Scotland will still be part of Europe, and the great success of the EU is the creation of a large economic zone.

Besides, small political entities, like Sweden, Singapore, and Hong Kong have prospered, while much larger entities have not. By an order of magnitude, far more important is pursuit of the right policies.

Another example of a non-issue is the currency. There are many currency arrangements that would work. Scotland could continue using sterling - with or without England's consent.

Because the economies of England and Scotland are so similar, a common currency is likely to work far better than the euro - even without shared fiscal policy. But many small countries have managed to have a currency of their own - floating, pegged, or "managed."

Labels: , ,



Krugman vs Stiglitz

Some of my colleagues have commented on Paul Krugman's financial diatribe, Scots, what the heck. My colleague Nigel Goddard penned a response.
While I have a lot of respect for Paul Krugman, his blanket warning against currency unions is misplaced, at least according to Joe Stiglitz, another Nobel prize winning economist (two economists; three opinions). Stiglitz said (at the book festival) that all three proposed models (currency union, use of currency without union, separate currency) can work depending on the characteristics of the economies and, most particularly, the quality of the institutions running the currency (or currencies). For a union to work the economies must be similar in various important ways (level of investment, competitive advantage, etc). rUK and Scotland are similar at present so it can easily work. Over the longer term it may be that Scotland breaks out of the low-investment, low-skill rUK model and goes for a more northern European high-investment, high-skill model (let's hope!). In that case a currency union would over time come under strain and eventually break up (i.e., into separate currencies). But in that case I know which economy I'd rather be in.
In the current situation, if the UK's central bank takes a decision contrary to Scotland's interest there is nothing we can do about it. An independent Scotland using UK currency could, if need be, move to its own currency. Krugman's piece says not a word on this option.

RBS, Lloyds, and TSB cannot afford to keep their headquarters in Scotland without the backing of the larger UK, though they may well keep much of their operations here. This is touted by Darling as a reason to vote No, but for me it's a reason to vote Yes. Banks too big to fail are an appalling idea; getting rid of them is an enormous benefit of an independent Scotland. I only hope Westminster keeps its promise not to agree a fiscal union!

Labels: , ,



Scots voting no to independence would be an astonishing act of self-harm

George Monbiot writes stirring stuff on indy. Well-reasoned and well-documented.
Imagine the question posed the other way round. An independent nation is asked to decide whether to surrender its sovereignty to a larger union. It would be allowed a measure of autonomy, but key aspects of its governance would be handed to another nation. It would be used as a military base by the dominant power and yoked to an economy over which it had no control. ... Most nations faced even with such catastrophes choose to retain their independence – in fact, will fight to preserve it – rather than surrender to a dominant foreign power....The fears the no campaigners have worked so hard to stoke are – by comparison with what the Scots are being asked to lose – mere shadows. As Adam Ramsay points out in his treatise Forty-Two Reasons to Support Scottish Independence, there are plenty of nations smaller than Scotland that possess their own currencies and thrive. Most of the world’s prosperous nations are small: there are no inherent disadvantages to downsizing.
Remaining in the UK carries as much risk and uncertainty as leaving. England’s housing bubble could blow at any time. We might leave the European Union.
How is the argument altered by the fact that Scotland is considering whether to gain independence rather than whether to lose it? It’s not. Those who would vote no – now, a new poll suggests, a rapidly diminishing majority – could be suffering from system justification.System justification is defined as the “process by which existing social arrangements are legitimised, even at the expense of personal and group interest”. It consists of a desire to defend the status quo, regardless of its impacts. It has been demonstrated in a large body of experimental work, which has produced the following surprising results.
System justification becomes stronger when social and economic inequality is more extreme. This is because people try to rationalise their disadvantage by seeking legitimate reasons for their position. In some cases disadvantaged people are more likely than the privileged to support the status quo. One study found that US citizens on low incomes were more likely than those on high incomes to believe that economic inequality is legitimate and necessary.
It explains why women in experimental studies pay themselves less than men, why people in low-status jobs believe their work is worth less than those in high-status jobs, even when they’re performing the same task, and why people accept domination by another group. It might help to explain why so many people in Scotland are inclined to vote no.
To deny this to yourself, to remain subject to the whims of a distant and uncaring elite, to succumb to the bleak, deferential negativity of the no campaign, to accept other people’s myths in place of your own story: that would be an astonishing act of self-repudiation and self-harm. Consider yourselves independent and work backwards from there; then ask why you would sacrifice that freedom.
Scots voting no to independence would be an astonishing act of self-harm

A yes vote in Scotland would unleash the most dangerous thing of all - hope

(Monbiot is also the author of Heat, my favorite book on climate change.)

Labels: , ,



Independent information on independence

A few sources of information that those interested may find helpful.


Thanks to my colleague James Cheney for spotting these. (I previously circulated a pointer to the second but not to the first or third.) The sources appear reputable, but---as with everything on the net---caveat emptor.

Labels: , , ,



Howard on Curry-Howard

When writing Propositions as Types, I realised I was unclear on parts of the history. Below is a letter I wrote to William Howard and his response (with corrections he provided after I asked to publish it). I believe it is a useful historical document, and am grateful to Howard for his permission to publish.

Update. References to Figures 5 and 6 in the following are to Propositions as Types. Thanks to Ezra Cooper for pointing out this was unclear.

Here is my original request.

Subject: The Formulae-as-Types Notion of Construction

Dear Prof Howard,

My research has been greatly influenced by your own, particularly the paper cited in my subject. I am now writing a paper on the field of work that grew out of that paper, which was solicited for publications by the Communications of the ACM (the flagship of the professional organisation for computer scientists). A draft of the paper is attached.

I would like to portray the history of the subject accurately. I have read your interview with Shell-Gallasch, but a few questions remain, which I hope you will be kind enough to answer.

Your paper breaks into two halves. The first describes the correspondence between propositional logic and simple types, the second introduces the correspondence between predicate logic and dependent types. Did you consider the first half to be new material or merely a reprise of what was known? To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability? To what extent did your work influence the subsequent work of de Bruijn and Martin Lof? What was the history of your mimeograph on the subject, and why was it not published until the Curry Festschrift in 1980?

Many thanks for your consideration, not to mention for founding my field! Yours, -- P

And here is his response: 

Dear Prof. Wadler,

As mentioned in the interview with Shell-Gellasch, my work on propositions as types (p-a-t) originated from my correspondence with Kreisel, who was very interested in getting a mathematical notion (i.e., in ordinary mathematics) for Brouwer's idea of a construction (as explained by Heyting). I was not familiar with the work of Brouwer or Heyting, let alone Kolmogorov, but, from what Kreisel had to say, the idea was clear enough: a construction of  alpha - > beta was to be a construction F which, acting on a construction A of alpha, gives a construction B of beta. So we have constructions acting on constructions, rather like functionals acting on functionals. So, as an approximation,

(1)   let's take "construction" to mean "functional".

But what kind of functionals? In constructive mathematics, a functional is not given as a set of ordered pairs. Rather,

(2)   to give a functional is to give not only the action or process it performs but also to give its type (domain and counterdomain).

Clearly, the type structure is going to be complicated. I set myself the project of finding a suitable notation for the type symbols. So one needs a suitable type symbol for the functional F, above. Well, just take it to be alpha itself (at this point, I was thinking of propositional logic). Suddenly I remembered something that Curry had talked about in the logic seminar during my time at Penn State. If we consider typed combinators, and look at the structure of the type symbols of the basic combinators (e.g., S, K, I), we see that each of the type symbols corresponds to (is isomorphic to) one of the axioms of pure implicative logic. Well! This was just what I needed!

How do we formulate the following notion?

(3)   F is a construction of phi.

Consider the case in which phi has the form alpha - > beta. The temptation is to define "F is a construction of alpha - > beta" to mean "for all A: if A is a construction of alpha, then FA is a construction of beta". Well, that is circular, because we have used if ... then ... to define implication. This is what you call "Zeno’s paradox of logic". I avoided this circularity by taking (3) to mean:

(4)   F is assigned the type phi according to the way F is built up; i.e., the way in which F is constructed.

Thus F is a construction of phi {\em by construction}. Your figure 6 illustrates precisely what I meant by this. (I did not have that beautiful notation at the time but it conveys what I meant.)

To summarize: My basic insight consisted simultaneously of the thoughts (2) and (4) plus the thought that Curry's observation provided the means to implement (2), (4). Let me say this in a different way. The thought (2) was not new. I had had the thought (2) for many years, ever since I had begun to study primitive recursive functionals of finite type. What was new was the thought (4) plus the recognition that Curry's idea provided the way to implement (4). I got this basic insight in the summer of 1966. Once I saw how to do it with combinators, I wondered what it would look like from the vewpoint of the lambda calculus, and saw, to my delight, that this corresponded to the intuitionistic version of Gentzen's sequent calculus.

Incidentally, Curry's observation concerning the types of the basic combinators is presented in his book with Feys (Curry-Feys), but I was unaware of this, though I had owned a copy for several years (since 1959, when I was hired at Penn State). After working out the details of p-a-t over a period of several months, I began to think about writing it up, so I thought I had better see if it is in the book. Well, it is easy enough to find if you know what you are looking for. On looking at it, I got a shock: not only had they extended the ideas to Gentzen's sequent calculus, but they had the connection between elimination of cuts from a derivation and normalization of the corresponding lambda term. But, on a closer look, I concluded that they had {\em a} connection but not {\em the} connection. It turns out that I was not quite right about that either. See my remark about their Theorem 5, below. Not that it would have mattered much for anything I might have published: even if they had the connection between Gentzen's sequent calculus and the lambda calculus, I had a far-reaching generalization (i.e., to Heyting arithmetic).

The above is more detailed than would be required to answer your questions, but I needed to write this out to clarify my thoughts about the matter; so I may as well include the above, since I think it will interest you. It answers one of your questions, "To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability?" Namely, my work draws on the work of Heyting and Brouwer, via Kreisel's explanation of that work to me. None of it was anticipated by the work of Heyting, Kolmogorov or Kleene: they were not thinking of functionals of finite type. Though I was familiar with Kleene's recursive realizability, I was not thinking about it at the time. Admittedly, it touches on ideas about Brouwer's constructions but is far from capturing the notion of a construction (actually, Kleene once made remarks to this effect, I forget where). Because of the relation between constructions and Kleene's recursive realizability, there could have been some unconscious influence; but, in any case, not a significant influence.

"did your work influence the subsequent work of de Bruijn and Martin Lof? " As far as I know, my work had no influence on the work of de Bruijn. His work appears to be completely independent of mine. I do recall that he once sent me a package of Automath material. The project of a computer program for checking existing proofs did not appear very interesting and I did not reply. What I would have been interested in is a program for finding proofs of results that had not yet been proved! Even a proof-assistant would have been fine. Why did he send me the Automath material? I don't recall what year it was. Sometime in the 1970s. Whatever the accompanying letter, it was not informative; merely something like: "Dear Professor Howard, you may be interested in the following material ...". Since that time, I have seen two or three articles by him, and I have a more favorable impression. It is good, solid work. Obviously original. He discovered the idea of derivations as terms, and the accompanying idea of formulae-as-types, on his own. He uses lambda terms but, I think, only for purposes of description. In other words, I don't think that he has the connection between normalization and cut-elimination, but I have not made an extensive examination of his work. In fact, does he use a Gentzen system at all? I just don't know. The latter two questions would easily be answered by anyone familiar with his work. In any case, give him credit where credit is due. There are enough goodies for everyone!

My influence on Martin-Löf? No problem there. I met him at the Buffalo 1968 conference and I told him my ideas. His instant reaction was: "Now, why didn't I think of that?" He had a visiting appointment at UIC for the academic year 1968-1969, so we had lot's of opportunity to talk, and he started developing his own approach to the ideas. In Jan. 1969, mainly to make sure that we were both clear on who had discovered what, I wrote up my own ideas in the form of handwritten notes. By then, Xerox machines were prevalent, so I sent a copy to Kreisel, and he gave copies to various people, including Girard. At least, I think that is how Girard got a copy, or maybe Martin-Löf gave him one. I like Martin-Löf's work. I could say more about this, but the short answer to your question is: Martin-Löf's work originated from mine. He has always given me credit and we are good friends.

On further thought, I need to mention that, in that first conversation, Martin-Löf suggested that the derivations-as-terms idea would work particularly well in connection with Prawitz's theory of natural deduction. I thought: okay, but no big deal. Actually, at that time, I was not familiar with Prawitz's results (or, if at all, then only vaguely). But it was a bigger deal than I had thought, because Prawitz's reductions steps for a deduction correspond direcly to reduction steps for the associated lambda term! Actually, for most purposes, I like the sequent formulation of natural deduction as given in pages 33 and 88 of Sorensen and Urzyczyn (2006). In fact, if we add left-implication-introduction to this (let's confine ourselves to pure implicative logic), the resulting system P# is pretty interesting. All occurrences of modus ponens can be eliminated, not just those which are preceded by left-implication-introduction. This is what I am up to in my JSL 1980 paper, "Ordinal analysis of terms of finite type." Also, the cut rule is easy to derive in P# (just consider, for typed lambda terms: a well-formed term substituted into a well-formed term results in a well-formed term); hence P# is is a conservative extension of the system P* in Part I of my little paper in the Curry Festschrift.

The phrase formulae-as-types was coined by Kreisel in order that we would have a name for the subject matter in our correspondence back and forth. I would assume that the phrase "propositions as types" was coined by Martin-Löf; at least, during our first conversation at the Buffalo 1968 meeting, he suggested that one could think of a type as a proposition, according to the idea that, in intuitionistic mathematics, the meaning of a proposition phi is given by the species of "all" proofs of phi. I use quotes here because we are not talking about a set-theoretic, completed infinity.

"the second [part] intrudes the correspondence between predicate logic and dependent types." I was not thinking about it in that way at all. I wanted to provided an interpretation of the notion of construction to some nontrivial part of intuitionistic mathematics (Heyting arithmetic). Part I of the paper was just the preliminaries for this. Actually, what you say in the pdf is consistent with this. No need for change here.

"Did you consider the first half to be new material or merely a reprise of what was known?" New. But in January of last year I had occasion to take a really hard look at the material in Curry-Feys, pp. 313-314; and I now see that there is a much closer relationship between my Theorem 2 in Part I and their Theorem 5, page 326, than I had thought. The issues here are quite interesting. I can provide a discussion if you want.

In the introduction to my little paper, I mention that Tait had influenced me. Let me say a few words about that. In the summer of 1963 we had conversations in which he explained to me that he had developed a theory of infinite terms in analogy to Schütte's theory of infinite proofs, where normalization (via lambda reductions) of an infinite terms corresponds to cut elimination of the corresponding proof. He did not know what to make of it. He thought of his theory of infinite terms as a sort of pun on Schütte's theory of infinite proofs. But we both agreed that  there must be a deep connection between normalization of lambda terms and Gentzen's cut elimination. We puzzled over this during two or three of our conversations but could not come up with an answer.

As explained in the first paragraph of this e-mail, my work originated with a problem posed by Kreisel; so, at the start of this work, certainly I was not thinking of those conversations with Tait. But, as mentioned above, as soon as I got the basic insight about the relevance of Curry's combinators, I considered how it would work for lambda terms. At that point, I remembered my conversations with Tait. In other words, when I verified that

(5)   cut elimination for a derivation corresponds to normalization for the term,

the conversations with Tait were very much on my mind. Most likely I would have noticed (5) without having had the conversations with Tait. But who knows? In any case, he deserves credit for having noticed the correspondence between derivations and terms. What he did not have was the associated correspondence between propositions and types. In fact, he was not using a general enough notion of type for this. By hindsight we can see that in his system there is a homomorphism, not an isomorphism, from propositions to types.

I need to say a bit more about Tait and types. Since Schütte had extended his system of proofs to transfinite orders, Tait extended his system of terms to transfinite type levels. I already had my own system of primitive recursive functionals of transfinite type. In our very first conversation, we compared out ideas on this topic. This topic requires that one think very hard about the notion of type. Certainly, I had already thought extensively about the notion of type (because of (2), above) before I ever met Tait, but my conversations with him reinforced this tendency. Thoughts about types were very much on my mind when I began to consider (1), (2), above.

As already mentioned, the notes were handwritten and xeroxed; no mimeographs. "why [were they] not published until the Curry Festschrift in 1980?" First let me mention why they got published in the Curry Festschrift. Selden was bringing out the Festschrift for Curry's 80th birthday. He asked me to contribute the notes. I said: "Sure. I'll write up an improved version. I can now do much better." He replied: "No, I want the original notes. It is a historical document." In other words, by that time various copies had been passed around and there were a number of references to them in the literature. So I had them typed up and I sent them in.

Why didn't I publish them before that? Simply because they did not solve the original problem. That was Kreisel's and Gödel’s verdict (Kreisel had shown or described the work to Gödel). In fact, even before communicating the work to Kreisel, I knew that I had gotten only an approximation to the notion of construction, and that more work had to be done. Essentially, the criticism is as follows. In my little paper, I do not provide axioms and rules of inference for proving statements of the form

(3)   F is a construction of phi.

Remember, we have to avoid "Zeno’s paradox of logic"! The answer is that the proofs will look like what you have in Figure 6. In other words, Figure 6 is not only a program; it is also a proof (or: it can be reinterpreted as a proof). But Figure 6 can also be interpreted as an explanation of how a construction (blue) is to be built up in order to have a given type (red). In other words, figures such as Figure 6 implements the idea (4) mentioned near the beginning of this e-mail; i.e., F is assigned the type phi according to the way F is built up.

I hope this tickles you; it certainly tickles me. Of course, the rules of inference are as in Figure 5. So these simple ideas provide the missing theory of constructions; or, at the very least, provide a significant step in that direction.

In Jan. 2013, I exchanged a few e-mails with Tait and Constable on the history of p-a-t. This caused me to take a really careful look at the Curry-Feys book. Here is something I found that really made me laugh: the required theory, whose inferences are of the form given in Figure 5 is already in Curry-Feys. Admittedly, to see this you first have to erase all the turnstyles ( |-- ); Curry seems to have some kind of obsession with them. In particular, erase the turnstiles from the proof tree on page 281. The result is exactly a proof tree of the general form given in your Figure 6. (Hint: (...)X is to be read "X has type (...)". In other words, rewrite (...)X as X : (...).) What does Fbc mean, where F is boldface? Just rewrite Fbc as b -> c. You see? I am an expert. I could probably make money writing a translation manual. In summary, the required theory is essentially just Curry's theory of functionality (more precisely, the appropriate variant of Curry's theory). So, did I miss the boat here? Might I have seen all this in 1969 if only I had had the determination to take a hard look at Curry-Feys? I don't know. It may require the clarity of mind represented by the notation of Figure 5. Do you have any idea when and where this notation came into use?

One more remark concerning my reason for not publishing. Didn't I feel that I had made an important breakthrough, in spite of Kreisel's and Gödel’s criticisms? On the one hand, yes. On the other hand, I had reservations. Except for Martin-Löf, Prawitz, Tait and Girard, very few people showed an interest in the ideas. But maybe Martin-Löf, Prawitz, Tait and Girard should have been enough. You say: "Certainly Howard was proud of the connection he drew, citing it as one of the two great achievements of his career [43]." Should we let that passage stand? Sure. The interview occurred in the spring of 2000. By that time, I was getting lots of praise from the computer science community. So, pride is a peculiar thing. Let me end this on a positive note. In 1969 Prawitz was in the US and came to UIC to give a talk. When he entered the room, he made a beeline for me, looked me in the eye and shook my hand. The message was: Well done! THAT made me proud.

There is more to say; but this answers your questions, I think; so I'll send it to avoid further delay. 

Your pdf, Propositions as Types, is very readable.


Labels: ,



Informatics Independence Referendum Debate - the result

Here is the outcome of the debate announced earlier:

Yes 19
No 25
Undecided 28

Yes 28
No 31
Undecided 26

(Either some people entered after the debate began, or some people began the debate unsure even whether they were undecided.)

Thank you to Alan, Mike, and the audience for a fantastic debate. The audience asked amazing questions on both sides, clearly much involved with the process.

Video of debate here.
Alan's slides here.
My slides here.



Informatics Independence Referendum Debate

School of Informatics, University of Edinburgh
Independence Referendum Debate
4.00--5.30pm Monday 25 August
Appleton Tower Lecture Room 2

For the NAYs: Prof. Alan Bundy
For the AYEs: Prof. Philip Wadler
Moderator: Prof. Mike Fourman

All members of the School of Informatics
and the wider university community welcome

(This is a debate among colleagues and not a formal University event.
All views expressed are those of the individuals who express them,
and not the University of Edinburgh.)


Research funding in an independent Scotland

A useful summary, written by a colleague.
In Summary:
  •  the difference between the Scottish tax contribution and RCUK spending in Scotland is small compared to savings that will be made in other areas such as defence
  • Funding levels per institution are actually similar in Scotland to those in the rest of the UK, it’s just that there are more institutions here
  • Because of its relative importance any independent Scottish government would prioritise research
  • If rUK rejects a common research area it would lose the benefits of its previous investments, and the Scottish research capacity, which is supported by the Scottish government and the excellence of our universities
  • There are significant disadvantages with a No vote, resulting from UK immigration policy and the possibility of exiting the EU

Labels: , ,



Scotland can't save England

Salmond concluded his debate with Darling by observing that for half his lifetime Scotland had been ruled by governments that Scotland had not elected. Many take this the other way, and fret that if Scotland leaves the UK, then Labour would never win an election. Wings Over Scotland reviews the figures. While Scotland has an effect on the size of the majority, elections would yield the same ruling party with or without Scotland in 65 of the last 67 years. To a first approximation, Scotland's impact over the rest of the UK is nil, while the rest of the UK overwhelms Scotland's choice half the time.

1945 Labour govt (Attlee)

Labour majority: 146
Labour majority without any Scottish MPs in Parliament: 143

1950 Labour govt (Attlee)

Labour majority: 5
Without Scottish MPs: 2

1951 Conservative govt (Churchill/Eden)

Conservative majority: 17
Without Scottish MPs: 16

1955 Conservative govt (Eden/Macmillan)

Conservative majority: 60
Without Scottish MPs: 61

1959 Conservative govt (Macmillan/Douglas-Home)

Conservative majority: 100
Without Scottish MPs: 109

1964 Labour govt (Wilson)

Labour majority: 4
Without Scottish MPs: -11

1966 Labour govt (Wilson)

Labour majority: 98
Without Scottish MPs: 77

1970 Conservative govt (Heath)

Conservative majority: 30
Without Scottish MPs: 55

1974 Minority Labour govt (Wilson)

Labour majority: -33
Without Scottish MPs: -42

1974b Labour govt (Wilson/Callaghan)

Labour majority: 3
Without Scottish MPs: -8

1979 Conservative govt (Thatcher)

Conservative majority: 43
Without Scottish MPs: 70

1983 Conservative govt (Thatcher)

Conservative majority: 144
Without Scottish MPs: 174

1987 Conservative govt (Thatcher/Major)

Conservative majority: 102
Without Scottish MPs: 154

1992 Conservative govt (Major)

Conservative majority: 21
Without Scottish MPs: 71

1997 Labour govt (Blair)

Labour majority: 179
Without Scottish MPs: 139

2001 Labour govt (Blair)

Labour majority: 167
Without Scottish MPs: 129

2005 Labour govt (Blair/Brown)

Labour majority: 66
Without Scottish MPs:  43

2010 Coalition govt (Cameron)

Conservative majority: -38
Without Scottish MPs: 19

Labels: , ,


How Scotland will be robbed

Thanks to the Barnett Formula, the UK government provides more funding per head in Scotland than in the rest of the UK. Better Together touts this as an extra £1400 in each person's pocket that will be lost if Scotland votes 'Aye' (famously illustrated with Lego). Put to one side the argument as to whether the extra £1400 is a fair reflection of the extra Scotland contributes to the UK economy, through oil and other means. The Barnett Formula is up for renegotiation. Will it be maintained if Scotland votes 'Nay'?

Wings over Scotland lays out the argument that if Scotland opts to stick with Westminster then Westminster will stick it to Scotland.
The Barnett Formula is the system used to decide the size of the “block grant” sent every year from London to the Scottish Government to run devolved services. ...
Until now, however, it’s been politically impossible to abolish the Formula, as such a manifestly unfair move would lead to an upsurge in support for independence. In the wake of a No vote in the referendum, that obstacle would be removed – Scots will have nothing left with which to threaten Westminster.
It would still be an unwise move for the UK governing party to be seen to simply obviously “punish” Scotland after a No vote. But the pledge of all three Unionist parties to give Holyrood “more powers” provides the smokescreen under which the abolition of Barnett can be executed and the English electorate placated.
The block grant is a distribution of tax revenue. The “increased devolution” plans of the UK parties will instead make the Scottish Government responsible for collecting its own income taxes. The Office of Budget Responsibility has explained in detail how the block grant from the UK government to Scotland will then be reduced to reflect the fiscal impact of the devolution of these tax-raising powers.” (page 4).But if Holyrood sets Scottish income tax at the same level as the UK, that’ll mean the per-person receipts are also the same, which means that there won’t be the money to pay for the “extra” £1400 of spending currently returned as part-compensation for Scottish oil revenues, because the oil revenues will be staying at Westminster. ...
We’ve explained the political motivations behind the move at length before. The above is simply the mechanical explanation of how it will happen if Scotland votes No. The“if” is not in question – all the UK parties are united behind the plan.
A gigantic act of theft will be disguised as a gift. The victories of devolution will be lost, because there’ll no longer be the money to pay for them. Tuition fees and prescription charges will return. Labour’s “One Nation” will manifest itself, with the ideologically troublesome differences between Scotland and the rest of the UK eliminated.
And what’s more, it’ll all have been done fairly and above-board, because the Unionist parties have all laid out their intentions in black and white. They’ll be able to say, with justification, “Look, you can’t complain, this is exactly what we TOLD you we’d do”.
This analysis looks persuasive to me, and I've not seen it put so clearly elsewhere. Please comment below if you know sources for similar arguments.

Labels: , ,



An Open Letter to Alex Salmond

Dear Alex,

It's not working.

There may be reasons to stick to the story that all will be smooth sailing in the event that Scotland becomes independent, but everyone knows it is not true.

Last night's debate makes it clear that refusal to discuss Plan B for currency hurts more than it helps. The same could be said for how negotiations will proceed over Trident, the EU, Nato, pensions, education, and the economy.

You took too long pressing Darling to admit that Scotland could succeed as an independent country, which you did to show that he too has issues with the truth. Last night's audience failed to get a straight answer from either side, and that led to their verdict: the debate was a disappointment.

It's time for an about face. Tell the truth. Independence will be stormy.  The transition will not be easy. We cannot be certain of the outcome, save that it will put Scotland in a position to make its own decisions.

The future is indefinite, whether we opt for independence or no. The probable outcome if Scotland remains in the UK is growing social injustice, austerity for the poor and more for the 1%, bedroom tax, referenda on whether to stay in the EU. You made these points last night, but they were overshadowed by your inability to admit that independence has risks too.

Truth will be refreshing. It will knock all loose and reinvigorate the debate. It may restore part of Scottish people's faith in the political process, something we sorely need regardless of which side wins in September.

If you stick to your current strategy, polls make it clear that No will win. It's time for Plan B.

Yours aye, -- P

Labels: , ,



Pictures taken at the right moment

33 pictures taken at the right moment.
36 more perfectly timed photos.
33 perfectly timed photos.




How do we satisfy our need to keep informed about results that might influence our work ? We (still) read papers and go to conferences. And how does the ACM help ? Well not very well.

  • Aggregating the deluge of information: anyone will tell you that the amount of research material to track and read has grown exponentially. But we still, to this day, have nothing like PUBMED/MEDLINE as a central clearinghouse for publications in CS-disciplines. The ACM DL is one step towards this, but it's a very poor imitation of what a 21st century repository of information should look like. It's not comprehensive, its bibliographic data is more erroneous than one expects, and the search mechanisms are just plain depressing (it's much easier to use Google).
  • Dealing with the changing nature of peer review and publication: Sadly, ACM, rather than acting like a society with its members' interests at heart, has been acting as a for-profit publisher with a some window dressing to make it look less execrable. Many people have documented this far more effectively than I ever could. 
  • Conference services: One of the services a national organization supposedly provides are the conference services that help keep communities running. But what exactly does the ACM do ? It sits back and nitpicks conference budgets, but provides little in the way of real institutional support. There's no infrastructure to help with conference review processes, no support for at-conference-time services like social networking, fostering online discussion and communities, and even modern web support. I only bring this up because all of these services exist, but piecemeal, and outside the ACM umbrella.
Underneath all of this is a slow but clear change in the overall CS research experience. The CRA has been doing yeoman service here: taking the temperature of the community every year with the Taulbee surveys, putting out a best practices document for postdocs after extensive community discussion, and even forming action groups to help gain more support for CS research from the government. Does the ACM do any of this ?

Labels: , ,



Meditations on Using Haskell

Bitemyapp - Meditations on Using Haskell explains why and how those in the trenches use Haskell, by quoting from conversations on an IRC channel.


So when i found haskell i slingshotted off through dependent and substructural types. Assuming that if a little was good a lot was better. Made it half way through TaPL and found pure type systems, coq, etc.
I think the power to weight ratio isn’t there. I find that Haskell gives amazingly expressive types that have amazingpower for the amount of code you tie up in them and that are very resistant to refactoring.
If i write agda and refactor I scrap and rewrite everything. If i write haskell, and get my tricky logic bits right?
I can refactor it, split things up into classes, play all the squishy software engineering games to get a nice API I want. And in the end if it still compiles I can trust I didn’t screw up the refactoring with a very high degree of assurance.


Admittedly I’m not playing at the level E is, but this was my experience. I can make sweeping changes to my API, get all the bugs caught by the type system, and still have minimal code impact.


That is what I was getting at with the tweet about not using dynamically typed langs because I need to be able to prototype quickly and get rapid feedback.
I think a lot of my friends thought i was just being trollish. Even just being able to see what would have to change if you changed your design slightly and being able to back it out quickly…

Labels: , , , ,



Propositions as Types, updated

Propositions as Types has been updated. Thanks to all the readers and reviewers who helped me improve the paper.

Propositions as Types
Philip Wadler
Draft, 26 June 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.
Comments still solicited!

Labels: , , ,



The Implicit Calculus: A New Foundation for Generic Programming

The Implicit Calculus: A New Foundation for Generic Programming

Bruno C. D. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, Kwangkeun Yi, Philip Wadler. Draft paper, 2014.

Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces.

Scala implicits are a GP language mechanism, inspired by type classes, that break with the tradition of coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit instantiation, which is generalized to work for any types. Scala implicits turn out to be quite powerful and useful to address many limitations that show up in other GP mechanisms.

This paper synthesizes the key ideas of implicits formally in a minimal and general core calculus called the implicit calculus (\lambda_?), and it shows how to build source languages supporting implicit instantiation on top of it. A novelty of the calculus is its support for partial resolution and higher-order rules (a feature that has been proposed before, but was never formalized or implemented). Ultimately, the implicit calculus provides a formal model of implicits, which can be used by language designers to study and inform implementations of similar mechanisms in their own languages.
 Share and enjoy!

Labels: , , , ,



Research Funding in an Independent Scotland with Michael Russel, MSP and Cabinet Secretary

MICHAEL RUSSELL MSP, CABINET SECRETARY FOR EDUCATION AND LIFE LONG LEARNING is coming 7-9pm Wednesday 25 June to the University of Edinburgh to speak on the issue of Research Funding in an Independent Scotland.

Much scaremongering has gone on around this subject and with this event we are hoping to meet the discussion head on to dispel fears and myths.

Also speaking will be Dr Stephen J Watson of the University of Glasgow and Chair of Academics For Yes who had an open letter on the subject printed in the Herald.
Anyone interested in the subject, Yes, Better Together, or Don't Know, is very welcome to attend. Questions from the audience on all topics related to the referendum will be invited in the Q&A. Please pass this on to anyone you think may be interested! This is a one-off opportunity from the Cabinet Secretary that we will not have again in the campaign.

7-9pm Wednesday 25 June 2014
University of Edinburgh, JCMB Lecture Theatre B, Kings Campus
Mayfield Road
Edinburgh EH9 3JN
Google map and directions

Dr Stephen J Watson · scienceforscotland@gmail.com · 07874233137

Labels: , , , ,


Congratulations to Shayan Najd on his 2014 Google PhD Fellowship!

I'm pleased to be working with Shayan on ABCD. List of recipients, Google's announcement.

Labels: ,



Mairi McFadyen's Open Letter to J. K. Rowling

Mairi McFadyen wrote a heartfelt response to J. K. Rowling, at National Collective.
To be asked, ‘what kind of country do you want to live in?’ is the most wonderful gift. Many people have taken this opportunity to empower themselves with knowledge. They are actively engaged in the world, not passively accepting of the status quo. They could have chosen to remain, in your own words, ‘comfortably within the bounds of their own experience, never troubling to wonder how things might be improved.’ They could remain switched off. Now we frequently overhear the #indyref discussed passionately at the taxi rank at 3 o’clock in the morning on a Friday night; in the chippy queue; at the hairdressers. It is being discussed by high school leavers: full of hope, full of promise for life and all the joy and wonders and pain it brings. ... 
I do not believe that independence will be easy or will somehow magically cure society’s problems. What this historical moment provides us with is an unmatched opportunity to participate in the writing of our own future. We have a chance to liberate ourselves from the stranglehold of austere Westminster politics and lead by example. We must ask ourselves, what really matters? ...
We need a new story to live by. In your own words: “We do not need magic to change the world, we carry all the power we need inside ourselves already: we have the power to imagine better.”

Labels: , , ,

This page is powered by Blogger. Isn't yours?