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


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.

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!

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.

Proofweb

Looks interesting, but I was unable to figure out how to get it to complete even a simple proof.

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.

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])