Propositions as Types
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!
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.Share and enjoy!
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.
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.
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.
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.”
Full story on the BBC.
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.”