I was at a Burns Supper last night (and my hangover is only beginning to subside as I write), for which I was asked to give the Immortal Memory. I was only asked to do it last week, so it was a bit of a rush job (the tone and humour is uneven), but I learned a lot about Rabbie Burns.

For posterity, here is the text, not precisely as delivered of course. In fact it probably reads better than how I delivered it, since I did not have time to commit it to memory or work on the presentation. Continue reading →

I’m working on a spreadsheet application at the moment. (Very exciting.) Part of the implementation obviously includes an expression language (so you can write things like total = sum(numbers) or vat = price × 17.5%).

Part of the design is to disallow things like "text" ÷ 11 or apples + oranges, and for that I need a type system.

So I’m investigating type systems, and rules for inferring types, and I’m looking at the algorithm they call Hindley-Milner type inference. I found an implementation of the algorithm in Perl by Nikita Borisov. This was in turn based on a Modula-2 implementation described in a paper by Luca Cardelli, Basic Polymorphic Typechecking (1987/’88). Given that I read maths only very painfully and slowly, it’s a very clear and readable paper.

I have reimplemented the algorithm in Scala (the language I’m using for my application).

Because Scala is itself a statically-typed language, some of the logic becomes clearer than the Perl version (for example, it is obvious where type variables are expected as opposed to type terms). Scala is also somewhat syntactically lighter than Perl, and a lot lighter and more expressive than Modula-2, so you may find it easier to read too.

The essential algorithm is elegant: given an expression in the form of an abstract syntax tree (AST), it recursively creates a tree of types in the expression, inserting placeholder ‘type variables’ for all the unknowns. It then ‘unifies’ sub-types, for example, ensuring that a function call’s result type is the same as the function definition’s result type. The final unification creates the most general type tree possible which accurately captures the expression type. The final unification may include still-unbound type variables, which would indicate that the expression is polymorphic in these type variables.

My code is available for download in the hope that others find it as useful as I found Luca Cardelli’s paper and Nikita Borisov’s Perl implementation:

http://dysphoria.net/code/hindley-milner/HindleyMilner.scala

You can run it as a script to see it analyse some example expressions: scala HindleyMilner.scala

Note: I believe that there was a mistake in the original Perl code; when unifying two variables, it tried to ensure that generic type variables were always bound to non-generic ones, not the other way about. This was in order to satisfy the requirement “In unifying a non-generic variable to a term, all the type variables contained in that term become non-generic.” However, it does not matter the order in which they are bound. Once the ‘bindee’ is further bound to a term, they both become bound to the same term. The original code omitted a call to prune in the method occursintype which (I believe) lead to a fault, for which the mistaken ‘fix’ was added.

I just watched The Stolen Earth (first episode of the two-parter Doctor Who season 4 finalé).

Fuck.

What a stinking cheese platter of overripe dramatic stilton.

Personally I lay full blame at the feet of series godfather and cheesemonger in residence, Russell T. Davies. Gaping plot-holes, magical mobile phones which work across the Universe, a key plot-point straight out of Lawnmower Man, pretentious, overblown orchestration, and seemingly an attempt to jam every single character and monster from the last 4 seasons, into a bloated 45 minutes of Whovian fanboy masturbation.

I liked one bit: the bit near the end, when Rose and The Doctor see each other for the first time in ages. That was lovely. However almost immediately afterwards the spell was broken, when they ran toward each other in a comically overextended ‘lovers’ cinematic run’ sequence which seemed to go on for about 5 minutes, (before a clichéd fucking Dalek clichédly shoots The Doctor, then a just-in-the-nick-of-clichéd-time Captain Clichéd Jack appears and clichédly shoots the Dalek).

And the Daleks… Basically they keep coming back from the dead in increasingly creative ways, just in time to threaten the Earth at the end of each season of Doctor Who. They’ve turned from a sinister surprise into an expected, end of season Very Special Guest Star.

Ugh. There’s only one way to save the Universe: quick, everybody dial The Doctor’s mobile phone number (07700 900461*—you may want to take a note of it in case your planet is ever in danger), thus boosting the subspace frequencies, routing it through every telephone exchange in the UK (which has the effect of, erm, not completely clogging the network, apparently), and causing big RKO-style circles to propagate out through space, thus alerting The Doctor that The Earth has been ‘hidden’ 1 second back in time. (Oddly, given that the TARDIS routinely pops back and forth in time by millennia, going back in time by 1 second causes the camera to shake and things to go on fire in a very dramatic manner.)

I can understand that Russell T. wanted to go out with a bang (he’s retiring as head writer), but he really should have smoked less crack while knocking off this piece of trite, disjointed, nonsensical, overblown, masturbatory, illogical, incoherent bollocks.

* Actually, I just tried phoning it. “This number is not recognised.” Thanks Doctor. (He must have changed his provider and not bothered moving his number over. Bloody disorganised Timelord.)

Gary Gygax, inventor of the role playing game, yesterday failed to recover from an Abdominal Aneurysm spell cast by higher-level mage. Finished off by giant spiders:

http://www.signonsandiego.com/uniontrib/20080322/news_1m22gygax.html

He is survived by a wife, six children, and 8 million teenagers with funny-shaped dice.