Wadler's Blog

Christine Bell has written an article on the currency debate that, for once, sheds more light than heat. She sets out home truths I've not seen stated elsewhere.

People ask the 'Yes' and 'No' camps to set out clearly what will happen, but this is not possible. A vote for 'Yes' is, and can only be, a vote to open negotiations.

It is not really in either side’s interest to tell voters that everything is up for negotiation. It is certainly not in the No campaign’s interests to tell people that Scotland has significant cards in its hand in any further negotiation over currency union. It is not in the Scottish government’s interests to point out how little it can lock down and promise about the economic future – or indeed many issues – in advance.

While both campaigns assert that this is about ‘Yes’ or ‘No’, Scotland becoming an independent country or not, in fact the situation is more complicated in our interdependent world.

An odd legal fiction decrees that if Scotland secedes from the UK, the identity of the former entity will reside with the remainder (abbreviated rUK, and sometime's pronounced "rump UK"). I have heard this applied to assert that Scotland will lose its EU membership, but I had not realised that it plays both ways.

Legally under international law the position is clear: if the remainder UK keeps the name and status of the UK under international law, it keeps its liabilities for the debt. The UK took out the debt, and legally it owes the money. Scotland cannot therefore ‘default’. It can be argued that international law does, however, contemplate that on dividing, the two resulting states share out assets and liabilities equitably. However, it has no hard and fast formula for what constitutes equitable division. Tangible natural assets such as oil go with the territory they are in. But other matters – in particular debt – must be negotiated. What is equitable will depend on the overall result and context of the negotiation.

Bell concludes with an intriguing possibility:

And instead of voting no, the people might simply decide to vote for ‘maybe’. For on most of the issues the people care about, the secret no campaign dare tell is: maybe is what a yes vote could be if that was what the people wanted.

Labels: Independence, Scotland, Yes!

Chris Grayling has banned sending of books to prisoners, a counter-productive act if ever there was one. It is hard to think of a nastier act from a government responsible for numerous nasties, from the bedroom tax to cutting legal aid. Thank goodness the Scottish justice system is devolved!

Yet another reason to vote for independence. Who would want to be part of a country that could do such a thing?

Spotted via Boing Boing.

Labels: Independence, Politics, Scotland, UK, Yes!

Julian Verlauget and Alok Menghrajani of Facebook have announced Hack, a gradually-typed variant of PHP. Hack is released open-source, features support for generic types and higher-order functions, and and compiles to HHVM. The core team for Hack features a number of the usual suspects, including Bryan O'Sullivan and Erik Meijer. Meanwhile, Simon Marlow and others at Facebook are pressing ahead with Haxl, a Haskell-based project.

However, Hack adds additional features beyond static type checking, including Collections, lambda expressions, and run-time enforcement of return types and parameter types.
Collections provide a clean, type-safe alternative to PHP arrays. We designed them specifically to work well with static typing and generics. The Collections API offers many classic higher-order functions such as map() and filter() to facilitate functional programming styles.
Lambda expressions give a concise syntax for creating closures. While PHP has closures, it requires the programmer to explicitly name the variables they need to use from enclosing scopes. With Hack's lambda expressions, we automatically infer these uses, saving you needless work. Lambda expressions make it more convenient to take full advantage of the Collections API.
Run-time enforcement of return types and parameter types (including scalar types like int and string) provides safety beyond what can be checked statically while type annotations are being gradually added to a codebase. Run-time enforcement helps programmers detect and diagnose certain kinds of problems more easily, and it helps HHVM's JIT produce more efficient code by making it safe to trust type annotations for optimization purposes.

Spotted by Shayan Najd.

Labels: Dynamic and Static Typing, Functional Programming, Programming Languages

Edward Snowden speaks via Google Hangouts at SxSW in Austin, Texas. Photograph: Jim Bennett/Corbis, Guardian

Cory Doctorow for the Guardian covers Edward Snowden's first public appearance. Snowden has been nominated for the Noble Peace Prize. His closing remarks show why he deserves it:

“Governments have stopped talking about the ‘public interest’ and started talking about the ‘national interest’. When these diverge, something is wrong.
“Would I do this again? Absolutely yes. No matter what happens to me. I took an oath to support and defend the constitution and I saw it was being violated on a mass scale. The interpretation of the constitution has been changed in secret from ‘no unreasonable search and seizure’ to ‘any seizure is fine, just don’t search it.’ That’s something the public has the right to know.”

Labels: Politics, Security

We are recruiting one PhD student to work on design and implementation of programming languages. The post is on the project TypeScript, The Next Generation, and is funded by a Microsoft Research PhD Scholarship.

There is increasing interest in integrating dynamically and statically typed programming languages, as witnessed in industry by the development of the languages TypeScript and Dart, and in academia by the development of the theories of gradual types, hybrid types, and the blame calculus. The purpose of our project is to bring the academic and industrial developments together, applying theory to improve practice.

Our project focusses on JavaScript, an ECMA standard, and its typed variant TypeScript, an open-source project sponsored by Microsoft. JavaScript plays a central role in web-based applications and the new Windows 8 framework, and TypeScript is seeing rapid takeup, with over 150 JavaScript libraries now provided with TypeScript declarations. Our project has two parts, one aimed at immediate short-term application, and one aimed at fundamental long-term research.

• TypeScript TNG The short-term goal is to build a tool, TypeScript: The Next Generation (or TypeScript TNG for short), that generates wrapper code from TypeScript import declarations to detect and pinpoint type errors. A wrapper will accept any JavaScript value as input, and either raise an error or return a value guaranteed to satisfy the invariant associated with the corresponding type. In particular, wrappers for generic types will assure surprisingly strong guarantees, known as “theorems for free”. Our hypothesis is that TypeScript TNG will aid debugging and increase reliablility of TypeScript and JavaScript code.
  
• A wide-spectrum type system. The long-term goal is to extend the foundations of the blame calculus to support a wide-spectrum of type systems, ranging from dynamic types (as in JavaScript or Racket) through generic types (as in F# or Haskell) to dependent types (as in F* or Coq). Our hypothesis is that a wide-spectrum type system will increase the utility of dependent types, by allowing dynamic checks to be used as a fallback when static validation is problematic.
  

The workplan is likely to be too ambitious for a single PhD studentship. Which aspects are carried out will depend on which seem the most promising as our work develops, and on the abilities and desires of the student.

The successful candidate will join the ABCD team, carrying out a research programme investigating sesion types and web programming. The project is jointly supervised by Andrew Gordon of Microsoft Research Cambridge and the University of Edinburgh.

You should possess an undergraduate degree in a relevant area, or being nearing completion of same, or have comparable experience. You should have evidence of ability to undertake research and communicate well. You should have a background in programming languages, including type systems, and programming and software engineering skills.

It is desirable for candidates to also have one or more of the following: a combination of theoretical and practical skills; experience of JavaScript or web programming; knowledge of dependent type theory; or training in empirical measurement of programming tasks. We especially welcome applications from women and minorities.

We seek applicants at an international level of excellence. The School of Informatics at Edinburgh is among the strongest in the world, and Edinburgh is known as a cultural centre providing a high quality of life.

The successful candidate will receive a studentship covering tuition and subsistence. Students from the UK or EU are preferred. Consult the University of Edinburgh website for details of how to apply.

If you are interested, please send an outline of your qualifications to: Prof. Philip Wadler (wadler@inf.ed.ac.uk).

Labels: Dynamic and Static Typing, Edinburgh, Functional Programming, JavaScript, Programming Languages, Types

I have a colleague who opposes independence, on the grounds that though it might be good for Scotland, it would be bad for the UK as a whole. Tariq Ali disagrees, as reported in Herald Scotland.

[Ali] believes the referendum could trigger the process of dismantling the British state. "At present UK politics are dominated by the extreme centre." A vote for Scottish independence would amount to a rejection of the extreme centre, and would open up the path for a "new politics" throughout the UK.
"England has been politically petrified since the Thatcher era." Although the Tories were soundly beaten by New Labour in 1997, Blair was the heir to Thatcher, he says. "An independent Scotland could also lead to something quite new in England; but not something nutty like UKIP."
He will tell his Scottish audiences that a vote for independence would " enable the rediscovery of hope of a better future, provide a much greater say for people over what their country looks like, and would finish off the decrepit, corrupt, tribal Labourist stranglehold on some parts of Scotland forever".
Ali is not much exercised by suggestions by businesses that would leave Scotland after a yes vote. "Large corporations are trying to frighten people,'' he said. ''But there are opportunities for investment from Scandinavia and the far east."
Ali's visit will not be welcomed by the SNP leadership. He will argue that an independent Scotland would need its own currency, and would require a state Bank of Scotland to be established. He says the new currency could be informally tied to sterling, but that all economic decisions would be taken in Scotland by a sovereign Scottish parliament.

Ali will be speaking in Appleton Tower, opposite my office, 3:30 Fri 14 March. Alas, I'll be in London that day, speaking at Functional Programming eXchange.

 

Labels: Edinburgh, Independence, Scotland, Yes!

Dead on and hilarious.

Labels: Independence, Scotland, Yes!

Propositions as Types
Philip Wadler
Draft, March 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 solicited!

Labels: Logic, Programming Languages, Types

Blame, coercions, and threesomes, precisely
Jeremy Siek, Peter Thiemann, and Philip Wadler
Draft, March 2014

We systematically present four calculi for gradual typing: the blame calculus of Wadler and Findler (2009); a novel calculus that pinpoints blame precisely; the coercion calculus of Henglein (1994); and the threesome calculus of Siek and Wadler (2010). Threesomes are given a syntax that directly exposes their origin as coercions in normal form, a more transparent presentation than that found in Siek and Wadler (2010) or Garcia (2013).

Comments welcome!

Labels: Functional Programming, Programming Languages, Types