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.
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.
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 (email@example.com).
I'm building a type checker for a small dependently typed language, but I don't really like the various derivatives of De Bruijn indices, so I decided to try to implement an alpha equivalence system instead. I've put the code for capture-avoiding substitution and alpha equivalence portion on github here: https://github.com/psygnisfive/AlphaConversion/blob/master/Version1.hs
I think this can possibly generalize quite a bit (abstracting over the Exp structure at least), instead using something likeclass Exp a where var :: Name -> a subst :: [Name] -> a -> Name -> a -> a alpha :: [Name] -> a -> a -> Bool
but I'd be open to further suggestions on what seems like a sensible generalization.submitted by psygnisfive
[link] [10 comments]
In a recent post I asked whether there is any such thing as a declarative language. The main point was to argue that the standard “definitions” are, at best, not very precise, and to see whether anyone might offer a better definition. What I’m after is an explanation of why people seem to think that the phrase has meaning, even though they can’t say very clearly what they mean by it. (One commenter analogized with “love” and “happiness”, but I would counter by saying that we’re trying to do science here, and we ought to be able to define our terms with some precision.)
As I mentioned, perhaps the best “definition” that is usually offered is to say that “declarative” is synonymous with “functional-and-logic-programming”. This is pretty unsatisfactory, since it is not so easy to define these terms either, and because, contrary to conventional classifications, the two concepts have pretty much nothing in common with each other (but for one thing to be mentioned shortly). The propositions-as-types principle helps set them clearly apart: whereas functional programming is about executing proofs, logic programming is about the search for proofs. Functional programming is based on the dynamics of proof given by Gentzen’s inversion principle. Logic programming is based on the dynamics of provability given by cut elimination and focusing. The two concepts of computation could not be further apart.
Yet they do have one thing in common that is usefully isolated as fundamental to what we mean by “declarative”, namely the concept of a variable. Introduced by the ancient Hindu and Muslim mathematicians, Brahmagupta and al Kwharizmi, the variable is one of the most remarkable achievements of the human intellect. In my previous post I had secretly hoped that someone would propose variables as being central to what we mean by “declarative”, but no one did, at least not in the comments section. My unstated motive for writing that post was not so much to argue that the term “declarative” is empty, but to test the hypothesis that few seem to have grasp the importance of this concept for designing a civilized, and broadly applicable, programming language.
My contention is that variables, properly so-called, are what distinguish “declarative” languages from “imperative” languages. Although the imperative languages, including all popular object-oriented languages, are based on a concept that is called a variable, they lack anything that actually is a variable. And this is where the trouble begins, and the need for the problematic distinction arises. The declarative concept of a variable is the mathematical concept of an unknown that is given meaning by substitution. The imperative concept of a variable, arising from low-level machine models, is instead given meaning by assignment (mutation), and, by a kind of a notational pun, allowed to appear in expressions in a way that resembles that of a proper variable. But the concepts are so fundamentally different, that I argue in PFPL that the imperative concept be called an “assignable”, which is more descriptive, rather than “variable”, whose privileged status should be emphasized, not obscured.
The problem with purely imperative programming languages is that they have only the concept of an assignable, and attempt to make it serve also as a concept of variable. The results are a miserable mess of semantic and practical complications. Decades of work has gone into rescuing us from the colossal mistake of identifying variables with assignables. And what is the outcome? If you want to reason about assignables, what you do is (a) write a mathematical formulation of your algorithm (using variables, of course) and (b) show that the imperative code simulates the functional behavior so specified. Under this methodology the mathematical formulation is taken as self-evidently correct, the standard against which the imperative program is judged, and is not itself in need of further verification, whereas the imperative formulation is, invariably, in need of verification.
What an odd state of affairs! The functional “specification” is itself a perfectly good, and apparently self-evidently correct, program. So why not just write the functional (i.e., mathematical) formulation, and call it a day? Why indeed! Declarative languages, being grounded in the language of mathematics, allow for the identification of the “desired behavior” with the “executable code”. Indeed, the propositions-as-types principle elevates this identification to a fundamental organizing principle: propositions are types, and proofs are programs. Who needs verification? Once you have a mathematical specification of the behavior of a queue, say, you already have a running program; there is no need to relegate it to a stepping stone towards writing an awkward, and invariably intricate, imperative formulation that then requires verification to ensure that it works properly.
Functional programming languages are written in the universally applicable language of mathematics as expressed by the theory of types. Such languages are therefore an integral part of science itself, inseparable from our efforts to understand and master the workings of the world. Imperative programming has no role to play in this effort, and is, in my view, doomed in the long run to obsolescence, an artifact of engineering, rather than a fundamental discovery on a par with those of mathematics and science.
This brings me to my main point, the popular concept of a domain-specific language. Very much in vogue, DSL’s are offered as the solution to many of our programming woes. And yet, to borrow a phrase from my colleague Guy Blelloch, the elephant in the room is the question “what is a domain?”. I’ve yet to hear anyone explain how you decide what are the boundaries of a “domain-specific” language. Isn’t the “domain” mathematics and science itself? And does it not follow that the right language must be the language of mathematics and science? How can one rule out anything as being irrelevant to a “domain”? I think it is impossible, or at any rate inadvisable, to make such restrictions a priori. Indeed, full-spectrum functional languages are already the world’s best DSL’s, precisely because they are (or come closest to being) the very language of science, the ultimate “domain”.
Filed under: Research Tagged: assignables, declarative language, domain-specific language, variables
Hi r/haskell! I've been using Haskell for a lot of low-thoroughput scientific computing and it involves a lot of matrix algebra. I've been using HMatrix mainly, but honestly I mostly use very simple functions—none of it is HMatrix specific.
So what I'd like to do is rewrite all of my functions in terms of some more generic Matrix typeclass. I thought that I had mostly accomplished the feat but ran into a lot of difficultly keeping track of the underlying field properly. Can anyone recommend good tutorials or source code examples where I can see a backend like this in practice?
In a perfect world I'd like to be able to write various instances to swap between HMatrix, Repa, or (god forbid) even Accelerate. Is there maybe something already like that out there?submitted by danielsmw
[link] [5 comments]
[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.
It’s been a while since my last blog post (early last December, in fact), and I’ve even neglected to process comments during the same period. Why the interruption? Have I finally run out of things to complain about? Not a chance! Actually, what’s happened is that on December 18 I underwent a kidney transplant from a kind living donor who I scarcely even knew before the surgery occurred. (If you are interested in the back story, you might like to read the newspaper article about it that appeared in the Pittsburgh Post-Gazette last Christmas.) My condition, primary FSGS, is idiopathic, and has been worsening for about 20 years (an unusually long time before transplant is indicated). Things finally became acute last year when I was reduced to approximately 10% kidney function, close to the lower bound for survival without renal replacement therapy. I was deeply humbled by the generosity of numerous people who stepped forward to volunteer to donate an organ to me, some of whom are readers of this blog and are in any case well-known to all of you. To them I am unable to adequately express my gratitude, but I can try to pay it forward over time. The donor selection process is largely opaque to the donee (so as to ensure that the donor not being is coerced or bribed), but as it turned out Tony Balko, the fiancé of my “niece”, Marina Pfenning, daughter of my colleague Frank Pfenning, became my donor, and thereby saved my life.
I have spent the last couple of months recovering from the surgery itself, which involved a substantial incision, monitoring my progress and the health of the organ, and adjusting the immune suppressants to achieve a balance between avoiding rejection and inviting infection. As a pay-it-forward gesture I volunteered to be a subject in a study of a new immune suppressant, ASKP1240, that is being developed specifically for kidney transplant patients. All this means frequent visits to the transplant center and frequent blood draws to measure my kidney function and medication levels. The recovery and monitoring has kept me operating at a reduced level, including neglecting my blog.
The good news is that Tony and I have fully recovered from surgery, and I am happy to say that I am enjoying an optimal outcome so far. The transplanted organ began working immediately (this is not always the case), and within two days I had gotten back ten years of kidney function. By now I am at completely normal blood levels, with no signs of kidney disease, and no signs of rejection or other complications. Tony gave me a really good organ, and my body seems to be accepting it so far. I’m told that the first six months are determinative, so I expect to have a pretty solid sense of things by the summer.
I would like to say that among the many things I’ve learned and experienced these last few months, one is an appreciation for the importance of organ donation. Every year hundreds of people die from kidney disease for lack of a suitable organ. If someone is limited to the national cadaverous donors list, it can take more than two years to find an acceptable organ, during which time people often die waiting. Another complication is that someone may have a willing donor, perhaps a family member, with whom they are incompatible. There are now several living donor exchange networks that arrange chains of organ swaps (as many as 55 simultaneously, I’m told!) so that everyone gets a compatible organ. But to be part of such an exchange, you must have a living donor.
Living donation is a daunting prospect for many. It does, after all, involve major surgery, and therefore presents a health risk to the donor. On the other hand nature has provided that we can survive perfectly well on one kidney, and a donation is literally the difference between life and death for the recipient. The trade-off is, in objective terms, clearly in favor of donation, but the scarcity of organs makes clear that not everyone, subjectively, reaches the same conclusion. As an organ recipient, allow me to plead with you to consider becoming an organ donor, at least upon your death, and perhaps even as a living donor for those cases, such as kidney donation, where it is feasible. Should you donate, and find yourself in need of an organ later in life, you will receive top priority among all recipients for a donated organ. The donation process is entirely cost-free to the donor in monetary terms, but pays off big-time in terms of one’s personal satisfaction at having saved someone’s life.
Filed under: Uncategorized Tagged: kidney transplant, organ donation