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.
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.”
"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.”
One question one might ask is which government shows stronger appreciation of the value of science? The coalition planned to slash science funding as part of its austerity programme, with a reprieve at the last moment leading to only a mild cut. The UK as a whole tends to elect governments that cut education and maintain science funding only when pressed."The Campaign for Science and Engineering (CaSE) has noted 'the cumulative erosion' of the science budget of 'over £1.1billion' and CaSE director, Dr Sarah Main, has commented that 'the last four years of a flat cash science budget is biting scientists and engineers and squeezing universities'.
Scottish Enterprise Edinburgh and Lothian has secured an additional £14 million from the Scottish Executive towards the £42 million construction costs of the University of Edinburgh's Informatics Forum. ...
A further £5 million has been awarded by Scottish Enterprise Edinburgh and Lothian towards a strategy which will maximise engagement with local and international industry, ensuring Scotland reaps the economic benefits the Forum will generate. ...
Tim O’Shea, Principal of the University of Edinburgh, says: ‘Scotland is already a world-leader in a number of areas of Informatics and with the vision and support of the Scottish Executive and Scottish Enterprise Edinburgh and Lothian it will become even stronger.’
To maintain the international quality of our research base, Professor Paterson added, we must maintain our access to international funding and maintain our international standards. To do so, it has been calculated that an independent Scotland would need to find an extra £300 million in funds per annum – double the amount currently distributed by the Scottish Funding Council.Lindsay Paterson is my colleague at the University of Edinburgh, so I wrote to him asking the source of his figures. He referred me to his detailed notes, where he explains (footnote 35) that
Public expenditure on research in Scotland is about 0.95% of GDP, whereas the average in the comparison developed countries noted in that footnote is 0.7%. The difference, 0.25%, is £325 million in a GDP of £130 billion.So the RSEs summary above is inaccurate: £300 million is not the difference between what Scotland spends now and what it would need to spend to fund science at the same level as currently, it is the difference between what Scotland spends now and what it would spend if it spent the same amount as a typical developed country.
