Wadler's Blog

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: Functional Programming, Logic, Programming Languages, Types

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: Computing, Functional Programming, Haskell, Programming Languages, Scala

Labels: Edinburgh, Independence, Science, Scotland, Yes!

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

Labels: Functional Programming, Session Types

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: Independence, Politics, Scotland, Yes!

You couldn't make it up. The Treasury announces the cost of setting up an independent Scotland will be £2.7 billion, citing a study by Prof Patrick Dunleavy of the LSE. Dunleavy denounces the claim at 'ludicrous' and estimates the cost at £150—200 million. The Treasury then issues a new figure of £1.5 billion, citing work of Prof Robert Young of Western University in Canada. Young remarks the government has cherry-picked the largest figure, with other estimates in the paper at one half or one third as much, going on to say "It is worth pointing out that there is a lot of politics in most of these estimates and the way they are deployed. ... these costs are just money — there are other possible costs and benefits from independence that may be less easily measured ... like a secure position in the European Union or the capacity to redistribute being able to achieve higher growth rates." Full story on the BBC.

Labels: Independence, Politics, Scotland, Yes!

My daughter introduced me to slam poet Taylor Mali.

Labels: Education

Today is the day we Reset the Net. Here is Edward Snowden's announcement:

"One year ago, we learned that the internet is under surveillance, and our activities are being monitored to create permanent records of our private lives — no matter how innocent or ordinary those lives might be.

Today, we can begin the work of effectively shutting down the collection of our online communications, even if the US Congress fails to do the same. That’s why I’m asking you to join me on June 5th for Reset the Net, when people and companies all over the world will come together to implement the technological solutions that can put an end to the mass surveillance programs of any government. This is the beginning of a moment where we the people begin to protect our universal human rights with the laws of nature rather than the laws of nations.

We have the technology, and adopting encryption is the first effective step that everyone can take to end mass surveillance. That’s why I am excited for Reset the Net — it will mark the moment when we turn political expression into practical action, and protect ourselves on a large scale.

Join us on June 5th, and don’t ask for your privacy. Take it back.”

Labels: Distributed Computing, Internet, Politics, Security