30.6.09
Pictures created from food
26.6.09
QML: Explicit first-class polymorphism for ML
Claudio Russo and Dimitris Vytiniotis, QML: Explicit first-class polymorphism for ML, ML Workshop, Edinburgh, August 2009.
This simple solution is along different lines than ML^F, FPH, and HML. I like the idea of allowing both explicit and implicit quantification, which was explored years ago by O'Toole and Gifford. I'm surprised that to make it work they needed to avoid permitting bound variables to be in scope, so their explicit constructs look (alas) quite different than the type abstraction and application of System F. I'd always thought that having 'rigid' type variables in explicit types was a good idea, but this paper makes an intriguing case otherwise.
This simple solution is along different lines than ML^F, FPH, and HML. I like the idea of allowing both explicit and implicit quantification, which was explored years ago by O'Toole and Gifford. I'm surprised that to make it work they needed to avoid permitting bound variables to be in scope, so their explicit constructs look (alas) quite different than the type abstraction and application of System F. I'd always thought that having 'rigid' type variables in explicit types was a good idea, but this paper makes an intriguing case otherwise.
The SIGSOFT Impact Project
As incoming Chair of SIGPLAN, one of my objectives is to explain to governments and the public why programming languages are important. Shiram Krishnamurthi points out to me that SIGSOFT has an Impact project with similar goals, and has produced several journal papers, including The impact of software engineering research on modern progamming languages.
9.6.09
Subtext
A visual programming language based on decision tables. This video describes unifying conditionals, switch statements, and polymorphism. Although the author, Jonathan Edwards, never mentions it, the language appears to be functional (although he compiles into Java).
1.6.09
George Monbiot: Captive Knowledge
Monbiot's Heat is my favorite book on climate change. Here is a column of his, pointing out to the general public the unwelcome, and potentially disastrous, government shift toward emphasizing 'economic impact' in research funding. Many academics make the same case, but it is good to someone outside the academic community backing this position.
Picture Charles Darwin trying to fill out his application form before embarking on the Beagle. "Explain how the research has the potential to impact on the nation's health, wealth or culture. For example: fostering global economic performance, and specifically the economic competitiveness of the United Kingdom ... What are the realistic timescales for the benefits to be realised?" If Darwin had been dependent on a grant from a British research council, he would never have set sail.Spotted by Maurice Naftalin. Thanks, Maurice!
26.5.09
Frank Lloyd Wright Lego
Two more for the wish list. The Guggenheim and Falling Water. Spotted on Boing Boing.
Lambda Chair
Slashdot: 'functional programming languages can beat C.'
Spotted on Slashdot by Greg Michaelson's brother.
John Fremlin has released what he believes to be the worlds fastest webserver for small dynamic content, teepeedee2. It is written entirely in LISP, the world's second oldest high-level programming language. He gave a talk at the Tokyo Linux Users Group last year, with benchmarks, which he says demonstrate that 'functional programming languages can beat C.' Imagine a small alternative to Ruby on rails, supporting the development of any web application, but much faster.
14.5.09
Robin Milner back in Edinburgh
Robin Milner has returned to Edinburgh as a visiting professor, and he just completed an enlightening series of lectures on bigraphs. This is how he began:
I always get nostalgic when I return to Edinburgh. On this visit, when I got off the train, a woman rushed up to me and asked "Are you Earnest?" I have a feeling that if I had said yes, I would be having a very good time right now.(Audience rolls on the floor.)
Jan Wielemaker, Doxygen
Jan Wielemaker is speaking at ICLP on "Enabling serendipitous search on the Web of Data using Prolog". I wonder about whether there is some way to get web pages to publish logic formulas which could be used for inference during a search, and this looks like it might be close. RDF is aimed at this, of course, but I'm unclear on what sort of inference its triples enable; using Prolog sounds plausible for more serious inference.
Two Wielemaker papers of interest: Using Prolog as the fundament for applications on the semantic web and PlDoc: Wiki style Literate Programming for Prolog. The second mentions a popular non-Prolog documentation tool called Doxygen.
Two Wielemaker papers of interest: Using Prolog as the fundament for applications on the semantic web and PlDoc: Wiki style Literate Programming for Prolog. The second mentions a popular non-Prolog documentation tool called Doxygen.
12.5.09
Hackers can sidejack cookies
A collage-homage to Guy L. Steele and Eric S. Raymond. Poetry in the 11 May 2009 New Yorker by Heather McHugh. Spotted by Ezra Cooper--thanks, Ezra!
11.5.09
A Brief, Incomplete, and Mostly Wrong History of Programming Languages
Several folk have pointed me at this, since Haskell and myself get a mention. I'm delighted to learn that "a monad is a monoid in the category of endofunctors"---anyone know where I can find a good tutorial?
6.001 RIP
Jerry Sussman has taught the last class ever of 6.001, Structure and Interpretation of Computer Programs, the introductory computing course at MIT. Here's a summary of the reasoning, taken from Dan Weinreb.
My own take on this is that you need both. Yes, one of the great advances of modern times is that we have large systems with large libraries, and students must learn to work with that. But, no, that doesn't mean that fundamental skills taught in SICP are any less relevant.
As Joel Splosky points out in The Perils of JavaSchools, it is vital that schools of computing continue to explode the minds of incoming undergraduates by exposing them to Scheme (or Haskell or Erlang or Prolog or anything else far from the mainstream).
In 1980, computer engineering was based on starting with clearly-defined things (primitives or small programs) and using them to build larger things that ended up being clearly-defined. Composition of these fragments was the name of the game.
However, nowadays, a real engineer is given a big software library, with a 300-page manual that’s full of errors. He’s also given a robot, whose exact behavior is extremely hard to characterize (what happens when a wheel slips?). The engineer must learn to perform scientific experiments to find out how the software and hardware actually work, at least enough to accomplish the job at hand. Gerry pointed out that we may not like it this way (”because we’re old fogies”), but that’s the way it is, and M.I.T. has to take that into account.
My own take on this is that you need both. Yes, one of the great advances of modern times is that we have large systems with large libraries, and students must learn to work with that. But, no, that doesn't mean that fundamental skills taught in SICP are any less relevant.
As Joel Splosky points out in The Perils of JavaSchools, it is vital that schools of computing continue to explode the minds of incoming undergraduates by exposing them to Scheme (or Haskell or Erlang or Prolog or anything else far from the mainstream).
21.4.09
Save Bletchley Park---your help needed
Sue Black writes:
Dear all,
Thank you so much for your support in the campaign to save Bletchley Park (BP) which I started last July. BP is not yet saved, but there have been several successes recently which are making the future seem much brighter. £900k has recently been pledged from English Heritage and Milton Keynes council towards the £10 million that BP need to ensure a secure future. This has meant that urgent repairs are now being undertaken :)
There has been a substantial amount of media coverage and award winning, and even celebrity endorsement: the wonderful Stephen Fry sent a tweet out via Twitter in February resulting in 8k hits on my blog in one day(!):
#bpark You might want to sign the Save Bletchley Park petition. Read @Dr_Black 's reasons why on http://is.gd/ikEh - BP won us the war! 2:11 AM Feb 4th from web
stephenfry
Stephen Fry
This is all really good news, and a good sign that the fortunes of BP are turning, but more help and support is still needed. The petition on the No. 10 Downing Street website is sitting at no. 5 with 20 099 votes and is not going to get any higher unless several thousand people sign it in the next month. This may be a tall order, but I am really hoping you can help.
Please sign the petition (it takes less than 1 minute) here:
http://petitions.number10.gov.uk/BletchleyPark/
and send this email to your colleagues, students, friends, relations and anyone else that you think might want to help save BP asking them to sign it too. If the petition gets to no. 1 it will show that there is a large amount of popular support and will ensure a response from government :)
Details of my campaign and achievements so far are on my blog:
http://www.savingbletchleypark.org/
Can we save Bletchley Park? Yes we can :)
Thanks very much for your time
Best regards
Sue
Dr Sue Black, Head of Department, University of Westminster, UK.
Famelab: What does logic have to do with Java?
12.3.09
Nonreferential this
This month's CACM contains articles by Jeffrey Ullman and Dave Patterson on how to advise PhD students. I particularly enjoyed the following aside from Ullman on a key writing skill:
While it sounds pedantic at first, you get a huge increase in clarity by chasing the "nonreferential this" from students' writing. Many students (and others) use "this" to refer to a whole concept rather than a noun. For example: "If you turn the sproggle left, it will jam, and the glorp will not be able to move. This is why we foo the bar." Now the writer of this prose fully understands about sproggles and glorps, so they know whether we foo the bar because glorps do not move, or because the sproggle jammed. It is important for students to put themselves in the place of their readers, who may be a little shaky on how sproggles and glorps work, and need a more carefully written paragraph. Today, it is not that hard to find a "this" that is nonreferential. Almost all begin sentences, so grepping for 'This' will find them.
Cafe Scientifique
I've been invited to give a talk for Cafe Scientifique, 8.30pm Mon 16 March at the Edinburgh Filmhouse. Title and abstract below. I've been asked to speak without using overheads or visuals, which should be an interesting challenge! The link above takes you to the Facebook page for the event.
Proofs are Programs: 19th Century Logic and 21st Century Computing
As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a principle for designing programming languages that will guide computers into the 21st century.
Similar material is covered in this article.
Proofs are Programs: 19th Century Logic and 21st Century Computing
As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a principle for designing programming languages that will guide computers into the 21st century.
Similar material is covered in this article.
23.2.09
Conal Elliott on Type class morphisms
Just read Conal Elliott's draft paper Denotational design with type class morphisms. I thought the same point was made more succinctly and with more substance in his earlier paper Simply efficient functional reactivity. Many of us already know what is in the new paper, but it still makes a valuable point. However, I think it should be a Functional Pearl, and it might work twice as well if it were half as long.
Conal is right to put forward type class morphisms as a design principle. However, I think he oversells their utility. In Section 6, he states that the fact the laws of an applicative functor are satisfied for TMap come 'for free', but they are 'free' only because he assumes you have already verified the same laws for (->), which is isomorphic to TMap.
The principle of type class morphisms is closely related to a design principle elucidated by John Reynolds in his paper Using Category Theory to Design Implicit Conversions and Generic Operators: implicit conversions between types should be homomorphisms on generic operators (that is, on overloaded operations defined by both types).
Conal is right to put forward type class morphisms as a design principle. However, I think he oversells their utility. In Section 6, he states that the fact the laws of an applicative functor are satisfied for TMap come 'for free', but they are 'free' only because he assumes you have already verified the same laws for (->), which is isomorphic to TMap.
The principle of type class morphisms is closely related to a design principle elucidated by John Reynolds in his paper Using Category Theory to Design Implicit Conversions and Generic Operators: implicit conversions between types should be homomorphisms on generic operators (that is, on overloaded operations defined by both types).
12.2.09
What do you believe is true even though you cannot prove it?
The World Question Center asks a different question every year, and the title links to one of my favorites.
11.2.09
Clay Shirky: Gin, Television, and Social Surplus
Clay Shirky on what we can accomplish if we stop watching tv.
So how big is that surplus? So if you take Wikipedia as a kind of unit, all of Wikipedia, the whole project--every page, every edit, every talk page, every line of code, in every language that Wikipedia exists in--that represents something like the cumulation of 100 million hours of human thought. I worked this out with Martin Wattenberg at IBM; it's a back-of-the-envelope calculation, but it's the right order of magnitude, about 100 million hours of thought.And television watching? Two hundred billion hours, in the U.S. alone, every year. Put another way, now that we have a unit, that's 2,000 Wikipedia projects a year spent watching television. Or put still another way, in the U.S., we spend 100 million hours every weekend, just watching the ads. This is a pretty big surplus.
30.1.09
Wordle
Wordle lets you generate word clouds from arbitrary sources. The picture shows a cloud built from this blog.IMU on Citation Statistics
A report from the International Mathematical Union on the use and misuse of citation statistics. Highly relevant with the proposed move toward citations counts as a basis for the new Research Evaluation Framework (REF, the successor to the Research Assessment Exercise, or RAE).
- Relying on statistics is not more accurate when the statistics are improperly used. Indeed, statistics can mislead when they are misapplied or misunderstood. Much of modern bibliometrics seems to rely on experience and intuition about the interpretation and validity of citation statistics.
- While numbers appear to be "objective", their objectivity can be illusory. The meaning of a citation can be even more subjective than peer review. Because this subjectivity is less obvious for citations, those who use citation data are less likely to understand their limitations.
- The sole reliance on citation data provides at best an incomplete and often shallow understanding of research—an understanding that is valid only when reinforced by other judgments. Numbers are not inherently superior to sound judgments.
23.1.09
An off-by-one error heard round the world
At the inauguration of the 44th President of the United States, during the invocation Dr. Rick Warren stated 'Now, today, we rejoice not only in America’s peaceful transfer of power for the 44th time.' But of course, it was the 43rd.
9.1.09
JfJfP and SJJP
Today I became a signatory of Jews for Justice for Palestinians and Scottish Jews for a Just Peace. I should have done this years ago, but given the events of the past week I could not put it off any longer. If not now, when?
7.1.09
Well-typed programs can't be blamed
Philip Wadler and Robert Bruce Findler, ESOP 2009, LNCS to appear.
We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.
We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.
24.12.08
If the Matrix ran on Windows
Brilliant and hilarious amateur production.
23.12.08
If programming languages were X
Lambda the Ultimate has a collection of analogies of the form 'If programming languages were X' for X varying over religions, cars, and so on. My favorite is girlfriends.
Unsafe
Via Iain Parris.
A person ran$ grep -w -o '\(unsafe[A-Z][a-zA-Z]*\)' haskell.log | sort -u.
A handful of highlights from the list:unsafeAtAnySpeedIO
unsafeShutUpAndActLikeACompiler
unsafeAttemptMiracles
unsafeBuyBackLoans
unsafeCallCthulhu
unsafeCollideHadrons
unsafeEatBabiesAndMaybePerformIO
unsafeExecuteArbitraryMachineCode
unsafePerformTheMightyFistOfTheDesertGodWithNoVowelsInHisName
18.12.08
Type Safe Pattern Combinators, by Morten Rhiger
An ingenious set of combinators for expressing pattern matching in a type-safe way. No ADTs required. Opens up the possibility of programming languages where we can declare new binding forms just as we declare new functions. Revolutionary, but may have been hard to publish before Programming Pearls were created---it shows why they are a good idea.
RAE 2008
Every few years, the UK Government conducts the Research Assessment Exercise, to determine the quality of research of every department in every university. The results for the most recent exercise are out, and by any measure Informatics at the University of Edinburgh did very well.
The Price of Forgoing Basic Research
An article by Bill Buxton in Business Week, making the case that too much emphasis on applications is counterproductive. My favorite line:
To be blunt, I believe that when academic research starts demonstrating industry relevance is when funding should be cut off, not augmented.
12.12.08
Informatics Christmas Meal
Facebook tells me the photo at left was shown at the Informatics Chrismas Meal. Caption: '"Some believed we lacked the programming language to describe your perfect world." says Agent Smith. Well, they should've used Lamda Calculus!'Informatics 1 - Fancy Dress and Competition
Every year I enjoy teaching Haskell to Informatics 1, but this year was spectacular. The students decided to attend the last day of lectures in fancy dress, and brought cupcakes decorated with lambdas. This year's programming competition was also exceptional. Every year there are one or two stunning entries, but this year we felt we had to award prizes to no less than seven!21.11.08
Scooping the Loop Snooper
A proof in verse of the undecidability of the halting problem, in the style of Dr Seuss, by my colleage Geoffrey Pullum.
No general procedure for bug checks succeeds.
Now, I won’t just assert that, I’ll show where it leads:
I will prove that although you might work till you drop,
you cannot tell if computation will stop.
19.11.08
Proofweb
Looks interesting, but I was unable to figure out how to get it to complete even a simple proof.
7.11.08
A bizarre function over streams
Alex Simpson showed me this bizarre function. Given a total predicate p over streams, the function (exists p) returns true if there is some stream for which the predicate returns true. This works because if the predicate is total, then there must be some bound on the initial segment of the stream that it examines.
The auxiliary function (epsilon p) returns a stream for which p holds, if one exists, and an arbitrary stream otherwise. The auxiliary function (prefix b p) is like (epsilon p), but only considers streams beginning with b.
Here are some test predicates and a testing function.
And here are some test runs.
The auxiliary function (epsilon p) returns a stream for which p holds, if one exists, and an arbitrary stream otherwise. The auxiliary function (prefix b p) is like (epsilon p), but only considers streams beginning with b.
exists :: ([Bool] -> Bool) -> Bool
epsilon :: ([Bool] -> Bool) -> [Bool]
prefix :: Bool -> ([Bool] -> Bool) -> [Bool]
exists p = p (epsilon p)
epsilon p = prefix (p (prefix True p)) p
prefix b p = b : epsilon (\x -> p (b : x))
Here are some test predicates and a testing function.
pos i x = not (x !! i)
run i x = and (map not (take i x))
alt i x = take i x == take i (cycle [False,True])
fal i x = not (take i x == take i x)
test f i = (exists (f i), take (i+1) (epsilon (f i)))
And here are some test runs.
*Main> test pos 5
(True,[True,True,True,True,True,False,True,True])
*Main> test run 5
(True,[False,False,False,False,False,True,True,True])
*Main> test alt 5
(True,[False,True,False,True,False,True,True,True])
*Main> test fal 5
(False,[False,False,False,False,False,False,False,False])
30.10.08
Atypical Typing
Mark Jason Dominus' talk at OOPSLA 2008. This covers similar ground to my OOPSLA talk, but in many ways Dominus makes a better job of it than I did. And it sounds better coming from someone outside the Haskell community.
27.10.08
From computers to ubiquitous computing, by 2020
I haven't had the time to read this yet, but it seems worth a look. Includes articles by Andy Hopper, Jeanette Wing, Thomas Henziger, Ronald Rivest, and Robin Milner, among others.
26.10.08
DabbleDB and Widgenie
21.10.08
Brokers with Hands on their Faces Blog
20.10.08
Learn You a Haskell
A rather nicely illustrated Haskell tutorial. Thanks to Jeremy for the tip.
16.10.08
Method and Apparatus for Automatic Notification and Response Based on Communication Flow Expressions
I've always envied those that list patents on their cv. Now I can too!
Joanne J. Ordille, Thomas A. Petsche, and Philip L. Wadler. Method
and Apparatus for Automatic Notification and Response Based on
Communication Flow Expressions. US Patent no.: 7,436,947 B2. Date of
Patent: October 14, 2008.
Joanne J. Ordille, Thomas A. Petsche, and Philip L. Wadler. Method
and Apparatus for Automatic Notification and Response Based on
Communication Flow Expressions. US Patent no.: 7,436,947 B2. Date of
Patent: October 14, 2008.
