pozorvlak: (polar bear)
2011-09-15 02:11 pm

Teaching our kids to code: a clarification

[This is a followup to Teaching our kids to code.]

When I say that I yearn for a mass-algorate society, I don't mean a society in which everyone has the level of knowledge of today's professional programmers. We live in a mass-literate society, but we don't expect everyone to be able to write novels or sonnets or in-depth analyses of the politics of the Middle East; we live in a mass-numerate society, but we don't expect everyone to be able to prove Stokes' Theorem or calculate cohomology groups. We do expect (almost) everyone to be able to read a newspaper, write a note for the babysitter, and write an SMS to tell their other half that they're staying in the pub for another round unavoidably delayed due to badgers on the line; we do expect (almost) everyone to be able to do simple arithmetic and make sense of graphs. Similarly, a mass-algorate society probably wouldn't expect everyone to be able to write an operating system kernel, a compiler or a game engine, but it probably would expect everyone to be able to write simple scripts to automate repetitive computational tasks, to do basic data-mining, or to control machinery.

I think that this is within the capabilities of almost everyone, given a sufficiently supportive infrastructure (which we don't have at the moment, but which we'd inevitably develop as more and more people become algorate). I'd love to live in that world.
pozorvlak: (polar bear)
2011-09-15 12:11 am
Entry tags:

Why we should teach our kids to code

There's a petition up on the British Government's e-petitions website, called "teach our kids to code". Despite being plugged by geek luminaries like Ben Goldacre, it's received barely a thousand signatures at the time of writing. I think this issue is much more important than that.

Goldacre says "heaven knows where our successive governments think the next generation of nerds is going to come from". But that's not the point. Call us nerds, geeks, hackers or Morlocks, the technological priesthood of humanity isn't going anywhere: this stuff is so goddamn fascinating that enough people will teach it to themselves for the wheels to keep turning. I don't know any programmers who weren't at least partly self-taught. Today's proto-hackers don't have the easily-programmable 8-bit micros that programmers of my generation cut their teeth on, but they've got something much better: a full open-source software stack whose source they can read, resources like Project Euler and Hackety Hack to help them take their first steps, and a huge community of open-source hackers to learn from. The petition talks about narrowing the appalling gender gap in IT, and that's a genuinely important issue, but it's not the main reason we should be teaching coding in schools.

John Graham-Cumming very nearly nails it:
I fully support that idea because I think that 'programming thinking' is an important skill that needs to be taught. Children first need to learn to be literate, then they need to learn to be numerate and finally they need to learn to be 'algorithmate' (yes, I just made that word up)... It's obvious to most people that illiteracy and innumeracy are problems to be tackled at school, but it's not obvious that we are now living in a world where logical and algorithmic thinking are very, very important.
Yes, we need some people who know how to instruct the machines if we want to have a viable economy. But the real point is that we currently live in a pre-algorate society¹. People who object that "Kids no more need to know how to code than they need to know car maintenance or how to build a table - useful for some, pointless for the majority" (a quote from one of JGC's commenters) are missing this point entirely. Computers are not like cars. Cars have a well-defined purpose, for which they have been ruthlessly optimised. Computers are more like writing. Writing is a means for expressing and conveying ideas (and here's the key bit: any ideas); computers are machines for executing instructions (and here's the key bit: any instructions). Saying that only a few people need to code today is like saying that only a few people needed to read and write in the 1500s². Their whole society was set up with the assumption that very few people could read: pub signs were carved representations of the pub's name, for instance. Everyone got by, but our society is incomparably richer since the advent of mass literacy. We're in the same situation with regards to algorithms today: a technological priesthood tries to do the algorithmic thinking for everyone, but the shiny toys they produce for non-algorists are often more hindrance than help. And unsurprisingly they miss a lot of opportunities for algorithmic assistance: ever see someone repetitively copying-and-pasting something over and over in Word? Do you feel the same almost physical pain that I get when I see someone doing drudge-work on a computer? In a mass-algorate society, that Word user would realise immediately that they were doing work that the computer could be doing for them, and the software would be set up to make it easy for them to automate their drudgework.


A very, very old description of an algorithm for calculating volumes. From the British Museum's Babylonian collection.


I want to live in a mass-algorate society. I want to use the software that a mass-algorate society would develop: sane and hackable, because everyone would know what computers fundamentally do and how to make them do what they want. I also expect that a mass-algorate society's software would have discoverable, predictable APIs, because 99% of coders would not be specialist programmers and would have better things to do than read endless documentation. But again, that's not really the point; the point is that I expect mass algoracy to have knock-on effects at least as dramatic as those of mass literacy.

Where do you want to go today?

Edit: followup post; Reddit discussion.




¹ "Algorithmate" strikes me as rather a mouthful. I propose "algorate", because it's shorter, easier to say, and a backhanded compliment to the man who, after all, was the first political leader to recognize the importance of the Internet and to promote and support its development. Poor Muhammad ibn Musa al-Khwārizmī al-Majousi al-Katarbali has already lost 14 of his name's 18 syllables by the time we've got to "algorithmate", two more seems like a relatively minor loss.

"Algorist", by the way, isn't a neologism: it's a long-established term meaning "one who invents algorithms".

² Car maintenance isn't analogous to coding; car maintenance is analogous to system administration, which I agree most users shouldn't have to bother with.
pozorvlak: (Default)
2011-08-15 05:35 pm

This one time, in Galilee...

In a world where Smile, Chinese Democracy, Duke Nukem Forever and Perl 6 have all actually been released, what archetype are we meant to use for an over-ambitious, never-to-be-completed project? And what did people use before those projects started? What do people who don't know about computers or rock music use?

The obvious answer, at least in the West, is "the Tower of Babel", but that doesn't quite work: firstly, because an essential aspect of the ToB story (and a more common use of the simile) is that the project failed because of communication breakdown; and secondly, because the ToB project failed not through its inherent overambition, but because said ambition led to one of the stakeholders¹ actively working to sabotage the project. DNF had many, many things working against it, but AFAIK intentional sabotage wasn't one of them.

Which leads me to two related questions:

1) What did people call a Yoko Ono figure before the Beatles? The idea of two close collaborators being driven apart by a woman who captivates Collaborator A and distracts him from his work with Collaborator B seems like it should be as old as Humanity; but the closest I can think of is the Biblical story of David, Uriah and Bathsheba. And again, the parallel doesn't quite work: it's important to that story that the woman was also desired by (indeed, married to) Collaborator B.

2) The Bible, as indicated above, provides a rich store of widely-applicable shared metaphors and allusions. As Western society becomes less Judaeo-Christian (and in particular, more secular), increasingly many people will not understand Biblical allusions. How shall we replace them?

¹ God.
pozorvlak: (Default)
2011-07-26 10:31 am

The most evil code I've ever written?

Back in 2003 when I was working for $hateful_defence_contractor, we were dealing with a lot of quantities expressed in dB. Occasionally there was a need to add these things - no, I can't remember why. Total power output from multiple sources, or something. Everyone cursed about this. So I wrote a desk calculator script, along these lines:
#!/usr/bin/perl

print "> ";
while (<>) {
   s|-?\d+(\.\d+)?([eE][-+]?\d+)?|10**($&/10)|oeg;
   print 10*log(eval $_)/log(10)."\n> ";
}
I've always thought of this as The Most Evil Code I've Ever Written. For those of you who don't speak fluent regex, it reads a line of input from the user, interprets everything that looks like a number as a number of decibels, replaces each decibel-number with the non-decibel equivalent, evaluates the resulting string as Perl code, and then converts the result back into decibels. Here's an example session:
> 1 + 1
4.01029995663982
> 10 * 10 
20
> cos(1)
-5.13088257108395
Some of you are no doubt thinking "Well of course that code's evil, it's written in Perl!" But no. Here's the same algorithm written in Python:
#!/usr/bin/python -u
import re, math, sys

def repl(match):
        num = float(match.group(0))
        return str(10**(num/10))

number = re.compile(r'-?\d+(\.\d+)?([eE][-+]?\d+)?')
while 1:
        line = sys.stdin.readline()
        if len(line) == 0:
                break
        line = re.sub(number, repl, line)
        print 10*math.log10(eval(line))
If anything, the Perl version is simpler and has lower accidental complexity. If Perl's not the best imaginable language for expressing that algorithm, it's damn close.

[I also tried to write a Haskell version using System.Eval.Haskell, but I got undefined reference to `__stginit_pluginszm1zi5zi1zi4_SystemziEvalziHaskell_' errors, suggesting my installation of cabal is b0rked. Anyone know what I need to do to fix it? Also, I'm sure my Python style can be greatly improved - suggestions most welcome.]

No, I thought of it as evil because it's doing an ugly thing: superficially altering code with regexes and then using string eval? And who the hell adds decibels, anyway?

Needless to say, it was the most successful piece of code I wrote in the year I spent in that job.

I was talking about string eval to Aaron Crane the other day, and I mentioned this program. His response surprised me:
I disagree; I think it’s a lovely piece of code. It may not be a beautiful jewel of elegant abstractions for a complex data model, true. But it’s small, simple, trivial to write, works on anything with a Perl interpreter (of pretty much any vintage, and with no additional dependencies), and clearly correct once you’ve thought about the nature of the arithmetic you’re doing. While it’s not something you’d ship as part of a safety-critical system, for example, I can’t see any way it could be realistically improved as an internal tool, aimed at users who are aware of its potential limitations.
[Full disclosure: the Perl version above didn't work first time. But the bug was quickly found, and it did work the second time :-)]

The lack of external dependencies (also a virtue of the Python version, which depends only on core modules) was very much intentional: I wrote my program so it could be trivially distributed (by samizdat, if necessary). Most of my colleagues weren't Perl programmers, and if I'd said "First, install Regexp::Common from CPAN...", I'd have lost half my potential audience. As it was, the tool was enthusiastically adopted.

So, what do you all think? Is it evil or lovely? Or both? And what's the most evil piece of code that you've written?

Edit: Aaron also pointed me at this program, which is both lovely and evil in a similar way. If you don't understand what's going on, type
perl -e 'print join q[{,-,+}], 1..9'
and
perl -e 'print glob "1{,-,+}2"'
at the command-line.
pozorvlak: (Default)
2011-07-02 06:37 pm

Fighting with make(1)

I'm currently running a lot of benchmarks in my day job, in the hope of perhaps collecting some useful data in time for an upcoming paper submission deadline - this is the "science" part of "computer science". Since getting a given benchmark suite built and running is often needlessly complex and tedious, one of my colleagues has written an abstraction layer in the form of a load of Makefiles. By issuing commands like "make build-eembc2", "make run-utdsp" or "make distclean-dspstone" you can issue the correct command (build/run/distclean) to whichever benchmark suite you care about. The lists of individual benchmarks are contained in .mk files, so you can strip out any particular benchmark you're not interested in.

I want to use benchmark runs as part of the fitness function for a genetic algorithm, so it's important that it run fast, and simulating another processor (as we're doing) is inherently a slow business. Fortunately, benchmark suites consist of lots of small programs, which can be run in parallel if you don't care about measuring wallclock seconds. And make already has support for parallel builds, using the -j option.

But it's always worth measuring these things, so I copied the benchmark code up onto our multi-core number crunching machine, and did two runs-from-clean with and without the -j flag. No speedup. Checking top, I found that only one copy of the simulator or compiler was ever running at a time. What the hell? Time to look at the code:
TARGETS=build run collect clean distclean

%-eembc2: eembc-2.0
        @for dir in $(BMARKS_EEMBC2) ; do \
          if test -d eembc-2.0/$$dir ; then \
            ${MAKE} -C eembc-2.0/$$dir $* ; \
          fi; \
        done
Oh God. Dear colleague, you appear to have taken a DSL explicitly designed to provide parallel tracking of dependencies, and then deliberately thrown that parallelism away. What were you thinking?¹ But it turns out that Dominus' Razor applies here, because getting the desired effect without sacrificing parallelism is actually remarkably hard... )

Doing it in redo instead )

Time to start teaching my colleagues about redo? I think it might be...

¹ He's also using recursive make, which means we're doing too much work if there's much code shared between different benchmarks. But since the time taken to run a benchmark is utterly dominated by simulator time, I'm not too worried about that.
pozorvlak: (Default)
2011-05-31 12:28 pm
Entry tags:

Code review gamification

Here's a daft idea I had last night, on which I'd appreciate feedback:

Suppose your project struggles to get code reviews done in a timely or thorough fashion¹. It might be possible to improve matters by making code review into a game: you score points for every bug you find, for suggesting successful solutions, or for completing your code review quickly. More points for finding subtler bugs, submitting working patches or completing reviews extra-quickly. At the end of the month award prizes (or perhaps just bragging rights) to whoever's amassed the most Code Review Points.

Has anyone tried this? Has anyone got any good ideas for (semi-)automating the system? Does anyone think it's a terrible idea? If so, why?

¹ You are doing code reviews, right? :-)
pozorvlak: (Default)
2011-05-30 06:44 pm

(no subject)

I have just written the following commit message:
"Branch over unconditional jump" hack for arbitrary-length brcc.
    
 - brcc (branch and compare) instructions can have static branch-prediction
   hints, but can only jump a limited distance.
 - Calculating the distance of a jump at expand-time is hard.
 - So instead of emitting just a brcc instruction, we emit an unconditional
   jump to the same place and a branch over it.
 - I added a simple counter to emit/state to number the labels thus introduced.
 - With this commit, I forfeit all right to criticise the hackiness of anyone
   else's code.
 - Though I doubt that will stop me.
pozorvlak: (Default)
2011-04-05 01:06 pm

Some trivial things I've released recently

Here are some bits of code I've released recently:

UK mountain weather forecast aggregator


The Mountain Weather Information Service do an excellent job, providing weather forecasts for all the mountain areas in the UK - most weather forecast sites only give forecasts for inhabited areas, and the weather at sea level often differs in interesting ways from the nearby weather at 1000m. However, their site's usability could be better. They assume that you're already in an area and want to know what the weather's going to be like for the next couple of days¹, but it's more normal for me to know what day I'm free to go hillwalking, and to want to know where I'll get the best weather.

So I decided to write a screen-scraper to gather and collate the information for me. I'd heard great things about Python's BeautifulSoup library and its ability to make sense of non-compliant, real-world HTML, so this seemed like a great excuse to try it out; unfortunately, BeautifulSoup completely failed me, only returning the head of the relevant pages. Fortunately, Afternoon and [livejournal.com profile] ciphergoth were on hand with Python advice; they told me that BeautifulSoup is now largely deprecated in favour of lxml. This proved much better: now all I needed to handle was the (lack of) structure of the pages...

There's a live copy running at mwis.assyrian.org.uk; you can download the source code from GitHub. There are a bunch of improvements that could be made to this code:
  1. The speed isn't too bad, but it could be faster. An obvious improvement is to stop doing eight HTTP GETs in series!
  2. There's no API.
  3. Your geographic options are limited: either the whole UK, or England & Wales, or Scotland. Here in the Central Belt, I'm closer to the English Lake District than I am to the North-West Highlands.
  4. The page design is fugly severely functional. Any design experts wanna suggest improvements? Readability on mobile devices is a major bonus.
  5. MWIS is dependent on sponsorship for their website-running costs, and for the English and Welsh forecasts. I don't want to take bread out of their mouths, so I should probably add yet more heuristics to the scraper to pull out the "please visit our sponsors" links.
  6. Currently all HTML is generated with raw print statements. It would be nicer to use a templating engine of some sort.
A possible solution to (1) and (2) is to move the scraper itself to ScraperWiki, and replace my existing CGI script with some JavaScript that pulls JSON from ScraperWiki and renders it. Anyway, if anyone feels like implementing any of these features for me, I'll gratefully accept your patches :-)

git-deploy


While I was developing the MWIS scraper, I found it was annoying to push to GitHub and then ssh to my host (or rather, switch to a window in which I'd already ssh'ed to my host) and pull my changes. So I wrote the World's Simplest Deployment Script. I've been finding it really useful, and you're welcome to use it yourself.

[In darcs, of course, one would just push to two different repos. Git doesn't really like you pushing to non-bare repositories, so this isn't such a great idea. If you want to know what an industrial-strength deployment setup would look like, I suggest you read this post about the continuous deployment setup at IMVU.]

bfcc - BrainF*** to C compiler


I was on the train, looking through the examples/ directory in the LLVM source tree, and noticed the example BrainF*** front-end. For some reason, it hadn't previously occurred to me quite how simple it would be to write a BF compiler. So I started coding, and had one working by the time I got back to Glasgow (which may sound a long time, but I was on my way back from an Edinburgh.pm meeting and was thus somewhat drunk). You can get it here. [livejournal.com profile] aaroncrane suggested a neat hack to provide O(1) arithmetic under certain circumstances: I should add this, so I can claim to have written an optimising BF compiler :-)



All of these programs are open source: share and enjoy. They're all pretty much trivial, but I reckon that creating and releasing something trivial is a great improvement over creating or releasing nothing.

¹ Great Britain is a small, mountainous island on the edge of the North Atlantic. Long-term weather forecasting is a lost cause here.
pozorvlak: (Default)
2011-03-31 12:11 pm

Building a queue with two stacks

Here's a data-structure I use almost every day. It's an implementation¹ of a queue. You have two stacks, an in-stack and an out-stack. To add a new item, push it onto the in-stack. To remove an item, take the top item off the out-stack; if the out-stack's empty, push all the items on the in-stack onto the out-stack in reverse order and then take the top item.

In C++ )


While Josie looks for an escape route, Haggis accepts the sudden shift in the Earth's gravity with stoic equanimity.

¹ This originally read "an unusual (AFAIK) implementation", but at least three people have now told me that it's the standard implementation used in the purely-functional world. I'm honestly astonished that people think this is a good idea in general, but hey, I guess I've learned something.
pozorvlak: (Default)
2011-03-30 10:57 pm

A Most Vexatious Merge

In The Art of Unix Programming, Eric Raymond lists among his basics of the Unix philosophy the "Rule of Generation":
14. Rule of Generation: Avoid hand-hacking; write programs to write programs when you can.
He goes into this idea in more detail in chapter 9 of the same book.

I used to believe this was a good idea, and in many situations (here's a great example) it is. But my current work project, which makes heavy use of code generators and custom minilanguages, has been a crash course (sometimes literally) in the downsides. Here's the latest example.

I've recently been merging in some code a colleague wrote about a year ago, just before I started. As you'd expect, with a year's drift this was a non-trivial exercise, but I eventually got all the diffs applied in (I thought) the right places. Protip: if forced to interact with a Subversion repository, use git as your client. It makes your life so much less unpleasant. Anyway, I finished the textual part of the merge, and compiled the code.

Screens-full of error messages. Oh well, that's not so unexpected.

I'm a big fan of Tilton's Law: "solve the first problem". The chances are good that the subsequent problems are just cascading damage from the first problem; no sense in worrying about them until you've fixed that one. Accordingly, I looked only at the first message: "The variable 'state' has not been declared at line 273".

Hang on...

Git checkout colleagues-branch. Make. No errors.

Git checkout merge-branch. Make. Screens-full of errors.

Git checkout colleagues-branch. Grep for a declaration of "state". None visible.

Clearly, there was some piece of voodoo that I'd failed to merge correctly.

I spent days looking through diffs for something, anything, that I'd failed to merge properly that might be relevant to this problem. I failed.

I then spent some serious quality time with the code-generation framework's thousand-page manual, looking for some implicit-declaration mechanism that might explain why "state" was visible in my colleague's branch, but not in mine. I failed.

Finally, I did what I probably should have done in the first place, and took a closer look at the generated code. The error messages that I was seeing referred to the DSL source code rather than the generated C code, because the code-generator emitted #line directives to reset the C compiler's idea of the current file and line; I could therefore find the relevant section of generated code by grepping for the name of the buggy source file in the gen/ directory.

The framework uses code generators for all sorts of things (my favourite generator being the shell script that interprets a DSL to build a Makefile which is used to build another Makefile), but this particular one was used to implement a form of polymorphism: the C snippet you provide is pasted into a honking great switch statement, which switches on some kind of type tag.

I found the relevant bit of generated code, and searched back to the beginning of the function. Yep, "state" was indeed undeclared in that function. And the code generator had left a helpful comment to tell me which hook I needed to use to declare variables or do other setup at the beginning of the function. So that was the thing I'd failed to merge properly!

Git checkout colleagues-branch. Grep for the hook. No results.

And then it hit me.

Like all nontrivial compilers, ours works by making several transformation passes over the code. The first pass parses your textual source-code and spits out a machine-independent tree-structured intermediate representation (IR). There then follow various optimization and analysis passes, which take in IR and return IR. Then the IR is expanded into a machine-specific low-level IR, and finally the low-level IR is emitted as assembly language.

The code that was refusing to compile was part of the expansion stage. But at the time that code was written, the expansion stage didn't exist: we went straight from the high-level IR to assembly. Adding an expansion stage had been my first task on being hired. Had we been using a language that supported polymorphism natively, that wouldn't have been a problem: the code would have been compiled anyway, and the errors would have been spotted; a smart enough compiler would have pointed out that the function was never called. But because we were using a two-stage generate-and-compile build process, we were in trouble. Because there was no expansion stage in my colleague's branch, the broken code was never pasted into a C file, and hence never compiled. My colleague's code was, in fact, full of compile-time errors, but appeared not to be, because the C compiler never got a look at it.

And then I took a closer look at the screensfull of error messages, and saw that I could have worked that out right at the beginning: subsequent error messages referred to OUTFILE, and the output file isn't even open at the expansion stage. Clearly, the code had originally been written to run in the emit phase (when both state and OUTFILE were live), and he'd got half-way through converting it to run at expansion-time before having to abandon it.

Lessons learned:
  1. In a generated-code scenario, do not assume that any particular snippet has been compiled successfully just because the whole codebase builds without errors.
  2. Prefer languages with decent native abstraction mechanisms to code generators.
  3. At least skim the subsequent error messages before dismissing them and working on the first bug: they may provide useful context.
  4. Communication: if I'd enquired more carefully about the condition of the code to be merged I could have saved myself a lot of time.
  5. Bear in mind the possibility that you might not be the guilty one.
  6. Treat ESR's pronouncements with even greater caution in future. Same goes for Kenny Tilton, or any other Great Prognosticator.
Any more?

Edit: two more:
  1. If, despite (2), you find yourself writing a snippet-pasting code generator, give serious thought to providing "this snippet is unused" warnings.
  2. Learn to spot when you're engaged in fruitless activity and need to step back and form a better plan. In my case, the time crawling through diffs was wasted, and I probably could have solved the problem much quicker if I'd rolled up my sleeves and tried to understand the actual code.
Thanks to [livejournal.com profile] gareth_rees and jerf.
pozorvlak: (Default)
2011-02-20 09:49 pm

Unit testing Agda code, redux

My post about unit-testing Agda code using elisp was posted to the dependent types subreddit (of which I was previously unaware). There, the commenter stevana pointed out that you could achieve the same effect using the following Agda code:
test1 : 2 + 1 == 3
test1 = refl

test2 : 3 + 0 == 3
test2 = refl
If your test fails, you'll get a compile-time error on that line. Aaaaaaaargh. I do wish someone had told me that before I spent a week mucking about with elisp. Well, that's not quite true - I learned a lot about Emacs, I had some fun writing the code, I learned some things about Agda that I might otherwise not have done, I got some code-review from [livejournal.com profile] aaroncrane, and I had a chance to try out using darcs and patch-tag for a collaborative project (the experience, I'm afraid, didn't measure up well against git and GitHub).

What I'd failed to realise, of course, is that the == type constructor describes computable equality: a == b is inhabited if the compiler can compute a proof that a is equal to b. "They both normalise to the same thing" is such a proof, and obviously one that the compiler's smart enough to look for on its own.

Ordinarily, a testcase is better than a compile-time assertion with the same meaning, because you can attach a debugger to a failing test and investigate exactly how your code is broken. This doesn't mean that types are stupid - types draw their power from their ability to summarise many different testcases. But in this case, I don't think there's much reason to prefer our approach to stevena's: the slight increase in concision that agda-test allows is balanced out by its inability to coerce both expressions to the same type, which often means the user has to type a lot more code. Stevena's approach does not suffer from this problem.

This also makes me more positive about dependent typing: if simple testcases can be incorporated into your type-system so easily, then maybe the "types are composable tests" slogan has some truth to it.

But seriously, guys, macros.
pozorvlak: (Default)
2011-02-04 02:11 pm

Unit testing Agda code with elisp

On Monday I went to the first day of Conor McBride's course Introduction to Dependently-Typed programming in Agda. "What's dependently-typed programming?" you ask. Well, when a compiler type-checks your program, it's actually (in a sense which can be made precise) proving theorems about your code. Assignments of types to expressions correspond to proofs of statements in a formal logical language; the precise logical language in which these statements are expressed is determined by your type system (union types correspond to "or", function types correspond to "if... then", that kind of thing). This correspondence goes by the fancy name of "the Curry-Howard isomorphism" in functional programming and type-theory circles. In traditional statically-typed languages these theorems are mostly pretty uninteresting, but by extending your type system so it corresponds to a richer logical language you can start to state and prove some more interesting theorems by expressing them as types, guaranteeing deep properties of your program statically. This is the idea behind dependent typing. A nice corollary of their approach is that types in dependently-typed languages (such as Agda, the language of the course) can be parametrised by values (and not just by other types, as in Haskell), so you can play many of the same type-level metaprogramming games as in C++ and Ada, but in a hopefully less crack-fuelled way. I spent a bit of time last year playing around with Edwin Brady's dependently-typed systems language Idris, but found the dependent-typing paradigm hard to wrap my head around. So I was very pleased when Conor's course was announced.

The course is 50% lab-based, and in these lab sessions I realised something important: fancy type-system or no, I need to test my code, particularly when I'm working in such an unfamiliar language. Dependent typing may be all about correctness by construction, but I'm not (yet?) enlightened enough to work that way - I need to see what results my code actually produces. I asked Conor if there were any way to evaluate individual Agda expressions, and he pointed me at the "Evaluate term to normal form" command in Emacs' Agda mode (which revealed that I had, indeed, managed to produce several incorrect but well-typed programs). Now, that's better than nothing, but it's clearly inadequate as a testing system - you have to type the expression to evaluate every time, and check the result by eye. I asked Conor if Agda had a more extensive unit-testing framework, and he replied "I'm not aware of such a thing. The culture is more 'correctness by construction'. Testing is still valuable."

So I wrote one.

I've written - or at least hacked on - a test framework of some sort at almost every programming job I've had (though these days I try to lean on Test::More and friends as much as possible). It gets hella tedious. This one was a bit different, though. One message that came out of Conor's lectures was that the correct way to represent equality in dependently-typed languages is somewhat controversial; as a beginner, I didn't want to dip a toe into these dangerous waters until I had a clearer idea of the issues. But the basic operation of any testing system is "running THIS should yield THAT". Fortunately, there was a way I could punt on the problem. Since Agda development seems to be closely tied to the interactive Emacs mode, I could deliver my system as a set of Emacs commands; the actual testing could be done by normalising the expression under consideration and testing the normalised form for string-equality with the expected answer.

This was less easy than I'd expected; it turns out that agda-mode commands work by sending commands to a slave GHCi process, which generates elisp to insert the results into the appropriate buffer. I'm sure that agda-mode's authors had some rationale for this rather bizarre design, but it makes agda-mode a lot harder to build on than it could be. However (in close collaboration with Aaron Crane, who both contributed code directly and guided me through the gargantuan Emacs API like a Virgil to my Dante) I eventually succeeded. There are two ways to get our code:
darcs get http://patch-tag.com/r/pozorvlak/agda-test
or
git clone git://github.com/pozorvlak/agda-test.git
Then load the file agda-test.el in your .emacs in the usual way. Having done so, you can add tests to your Agda file by adding comments of the form
{- test TESTNAME: ACTUAL is EXPECTED; -}
For instance,
{- test 2+1: (suc (suc zero)) +N (suc zero) is (suc (suc (suc zero)));
   test 3+0: (suc (suc (suc (zero)))) +N zero is (suc (suc zero)); -}
When you then invoke the function agda2-test-all (via C-u C-c C-v for "verify"), you should be presented with a new buffer called *Agda test results*, containing the text
1..2
ok 1 - 2+1
not ok 2 - 3+0
    got 3
    expected 2
[ Except, er, I get "expected _175" for that last test instead. I don't think that's a bug in my elisp code, because I get the same result when I evaluate that expression manually with C-c C-n. Halp pls?]

You should recognise the output as the Test Anything Protocol; it should be easy to plug in existing tools for aggregating and displaying TAP results.

There are a lot of things I'd like to do in the future:
  • Add commands to only run a single test, or just the tests in a given comment block, or a user-specified ad-hoc test group.
  • Highlight failing tests in the Agda buffer.
  • Allow the user to specify a TAP aggregator for the results.
  • Do something about the case where the test expressions don't compile cleanly.
If you'd like to send patches (which would be very welcome!), the darcs repository is currently considered the master one, so please submit patches there. I'm guessing that most Agda people are darcs users, and the slight additional friction of using darcs as my VCS is noise next to the friction of using Emacs as my editor :-) The git repository is currently just a mirror of the darcs one, but it would be easy to switch over to having it as the master if enough potential contributors would prefer git to darcs. Things might get confusing if I get patches submitted in both places, though :-)
pozorvlak: (Default)
2011-01-14 03:01 pm

A quick introduction to redo

[This is a cleaned-up version of the notes from my Glasgow.pm tech talk last night. The central example is lifted wholesale from apenwarr's excellent README for redo; any errors are of course my own.]
Read more... )
pozorvlak: (Default)
2011-01-14 11:16 am

NWE.pm Hackday lessons learned

Last November a few of us from Glasgow.pm went to the North-West England Perl Mongers Hackathon, kindly hosted by Shadowcat Systems at their offices in Lancaster. The following are my notes on the day; I'd intended to present them at Glasgow.pm's December meeting, but the weather meant it was put off until the January meeting last night.
  1. The night before, I met up with my friend Caroline for a drink. We hadn't seen each other for a couple of years, and it turned out that we had a lot of catching up to do, so one drink turned into two, which turned into five, which turned into a gig. Then I got up very early and got on one of these, which made me feel like this.

    So, Lesson Learned number 1: do not go out and get steaming the night before the Hackday, especially if you're travelling there by a very juddery train.

  2. Some Modern Perl modules have very long dependency lists: Task::Kensho, for instance, depends on all of these modules. CPAN is great, but installing and testing all of those modules takes a long time. So, Lesson Learned number 2: if the project you're going to be working on has some dependencies, or is planned to have some dependencies, then find out what they are and install them beforehand. Dually, if you're running a hackday project and you plan to depend on some module or other, tell people about it and encourage them to install it in advance.

  3. Lesson Learned number 3: you're going to need a version control repository sooner or later - you might as well set it up in advance and write the URL on the whiteboard for everyone to see when they come in. For a Hackday setup it's probably better to use a push model than a pull-request model; GitHub will support this, but you need to create a Hackday user and add everyone's ssh public keys to its keychain.

  4. Communication is really hard. My first commit was at 16.47 because we spent so long arguing about what exactly Oyster was meant to do and how it was meant to work. Most of the time this was because there were people still arguing about things that I'd thought were settled.

    So, Lesson Learned number 4: this is one of those cases where it's better to make a decision now than to make the best decision when it's too late and everyone's gone home. And when you've made your decision, communicate it clearly.

  5. Other lessons learned: Shadowcat (and NWE.pm more generally) are great people, Osfameron is a dude, pizza is tasty, and hackathons are great fun.
Thanks once again to the Shadowcat team for a great day.
pozorvlak: (pozorvlak)
2011-01-12 08:28 pm

Redo from scratch

I think that djb redo will turn out to be the Git of build systems.

Read more... )
pozorvlak: (Default)
2010-12-01 03:03 pm

Addendum to the git/darcs talk

After my git/darcs talk, some of the folks on darcs-users were kind enough to offer constructive criticism. In particular, Stephen Turnbull mentioned an interesting use-case which I want to discuss further.

As I tried to stress, the key insight required to translate between git-think and darcs-think is
In git, the natural thing to pull is a branch (an ordered list of commits, each of which is assumed to depend on those before it); in darcs, the natural thing to pull is a patch (a named change whose dependencies are calculated optimistically by the system).
Stephen's use-case is this: you're a release manager, and one of your hackers has written some code you want to pull in. However, you don't want all their code. Suppose the change is nicely isolated into a single commit. In darcs, you can pull in just that commit (and a minimal set of prior commits required for it to apply cleanly). This is as far as my thinking had got, but Stephen points out that the interesting part of the story is what happens next: if you subsequently pull in other changes that depend on that commit, then darcs will note that it's already in your repository and all will be well. This is true in git if the developer has helpfully isolated that change into a branch: you can pull that branch, and subsequent merges will take account of the fact that you've done so. However, if the developer hasn't been so considerate, then you're potentially in trouble: you can cherry-pick that commit (creating a new commit with the same effect), but if you subsequently pull a branch containing it then git will not take account of your having cherry-picked it earlier. If either of you have changed any of the lines affected by that diff, then you'll get conflicts.

Thinking about this further, this means that I was even righter than I realised. In the git view of the world, the fact that that commit is not in its own branch is an assertion that it only makes sense in the context of the rest of the branch. Attempting to pull it in on its own is therefore not useful. You can do it, of course - it's Unix git, you can do anything - but you're making a rod for your own back. As I tried to emphasize in the talk, git-cherry-pick is a low-level, hackish tool, only really intended for use in drastic situations or in the privacy of your own local repo. If you want something semantically meaningful, only pull branches.

Git-using release managers, therefore, have to rely on developers to package atomic features sensibly into branches. If your developers can't be trusted to do this, you may have a problem. But note that darcs has the dual problem: if you can't trust your developers to specify semantic (non-textual) dependencies with darcs commit --ask-deps, then you're potentially going to be spending a lot of time tracking down semantic dependencies by hand. Having been a release manager under neither system, I don't have any intuition for which is worse - can anyone here shed any light?

[The cynic in me suggests that any benefits to the Darcs approach would only become apparent in projects which are large enough to rule out the use of Darcs with its current performance, but I could, as ever, be completely wrong. And besides, not being very useful right now doesn't rule out its ultimately proving to be a superior solution.]

On another note: Mark Stosberg (who's written quite a lot on the differences between darcs and git himself) confirms that people actually do use spontaneous branches, with ticket numbers as the "branch" identifiers. Which got me thinking. Any git user can see that spontaneous branches are more work for the user than real branches, because you have to remember your ticket number and type it into your commit message every time. Does that sound like a trivial amount of work to complain about? That's because you have no idea how easy branching and merging is in git. But it's also work that can be automated away with some tool support. Stick a file somewhere in _darcs containing the name of the current ticket, and somehow prepend that to your commit messages. I have just written a Perl script to do that (GitHub repo, share and enjoy).

Now we just need the ability to easily back-out and restore incomplete tickets without creating a whole new repo, and they'll be as convenient as git topic branches :-)
pozorvlak: (Default)
2010-11-30 04:03 pm

Programmer competency matrix

[livejournal.com profile] fanf linked to this on Twitter: I thought I'd fill it in with my "score". Domain-specific stuff applies to my current main gig.

Read more... )
pozorvlak: (Default)
2010-11-17 09:59 am

A rule I try to live by

Here's a pattern I see a lot in imperative languages:
sub doStuff {

    # do this
    code
    code
    code
    more code

    # do that
    code
    code
    code
    code
    more code

    # do t'other
    code
    code
    code
    code
}
That is, a long subroutine with different sections separated out by vertical whitespace.

I try to live by the following rule:
If you are ever tempted to insert vertical whitespace in the middle of a subroutine to separate out different sections, just put the sections in their own freaking subroutines already.
The usual reasons to strive for short subroutines apply:
  • It's very hard to get an overview of a block of code that doesn't fit into one screen.
  • Long subroutines make it much harder to follow the dataflow: where was this variable defined? When was it last set? When will it be used again?
  • The subroutine is the basic unit of re-use; if a section of code isn't isolated into a subroutine, you can't use it again elsewhere.
  • For maximum comprehensibility, a subroutine should do one well-defined task. If your subroutine's long, it suggests that it's doing lots of things.
The hard part of splitting up large subroutines is usually finding the right subsections to extract; but if you feel a temptation to add vertical whitespace, that's a great big hint that this is one such place. Take that comment you were tempted to add, change the spaces to underscores, and you've even got the name of your new subroutine¹. If you're using a modern IDE like Eclipse or Padre, extracting the new subroutine is a matter of selecting some text and clicking "Extract Method"; but even in vim it should be pretty straightforward².

So please, take that hint. Or I shall track you down and strangle you.

¹ As any fule kno, there are only two really hard problems in computer science: cache invalidation, naming things, and off-by-one errors.
² I once had a colleague who'd not only write subroutines that consisted of commented whitespace-separated sections, but who put each section into its own lexical scope. At which point, you've done 90% of the work to extract a new subroutine, so why not go the final step?
pozorvlak: (Default)
2010-11-12 10:37 am

Darcs versus git slides

Last night was Glasgow.pm's second technical meeting, and I finally gave a version of the DVCS-comparison talk I've been thinking about doing for at least a year. I could have done with a lot more rehearsal, something that would have been helped by finishing off the slides before (checks git-log) 5.33pm - the meeting started at 6.15 - but I think it went OK.

The idea of the talk was to
  • explain a little bit of what git's doing under the hood
  • explain how the darcs model differs
  • cut through some of the tangle of conflicting terminology
  • explain why git users think branching's such a big deal, and why darcs users think that cherry-picking's such a big deal (spoilers: the answers are the same!).
I didn't try to explain the details of how you use either system, because in both cases that's fairly easy to work out once you have a decent handle on what's going on under the hood. The audience was mostly full of git users, so I spent more time explaining the darcs model; hopefully darcs users wanting to learn git will also find the slides helpful. For a more detailed introduction to how git works, I strongly recommend mjd's recent talk on the subject, and for more on the (much ameliorated) "exponential merge" problem in darcs see here. Edit: and for the details of how to use git from a darcsy perspective, try the GHC wiki's git for darcs users page.

By the way, there's a useful consequence of git's design which neither mjd's slides nor mine mention, but which I mentioned in the talk, namely the reflog. It's a list of every commit you've visited, and when you were there. This means you can say things like "Show me the state of the repository at 11.15 last Monday"; more usefully, it lets you track down and recover commits that have been orphaned by some botched attempt at history rewriting. This is not a feature that you need often, but when you do need it it's an absolute lifesaver. Git's "directed graph of snapshots" model makes this feature almost trivial to add (and because git's built on a content-addressable filesystem, jumping to those orphaned commits is fast), but darcs' "bag of patches" model makes it much harder to add such a feature (though they're thinking about possible approaches that make more sense than storing your darcs repo in git).

Thanks very much to Eric Kow and Guillaume Hoffman for answering my questions about darcs. Any errors remaining are of course my own.

Anyway, you can get the slides here (slightly cleaned-up). Please let me know if they don't make sense on their own. Or, if you really care, you can browse the history here. To build the TeX source, you'll need the prosper, xypic and graphicsx packages installed.

Edit: some of the people on darcs-users were kind enough to comment, prompting some further thought. I've written a followup post in which I respond to some of the things they said.
pozorvlak: (Default)
2010-11-05 11:17 am

PeCoWriMo day 4

Yesterday was a bit of a weird one: I was invited to attend a friend's citizenship ceremony at the last minute, and it threw my schedule off a bit. I managed to get a bit of work done on the SEKRIT WEB PROJECT (all setup stuff; didn't close any actual tickets, but I did write some bash, and did have a look through some of the existing code), and had another brief play with Idris.

Idris doesn't, as far as I can tell, have a name-overloading mechanism like Haskell's typeclasses (the keywords are proof, data, using, idiom, params, namespace, module, import, export, inline, where, partial, syntax, lazy, infix, infixl, infixr, do, refl, if, then, else, let, in, return, include, exists, and with - suggesting Edwin's added a module system and possibly even a syntax-extension mechanism since writing the tutorial...). "But so what?" I thought. "You can treat types as values, and implement Haskell's Eq as a function from a type to its equality function." So saying, I wrote this:
eqFun : {a:Set} -> a -> a -> Bool;
eqFun String = strEq;
eqFun Char = charEq;
eqFun Int = (==);
I loaded it into the interpreter, and got the response
eqs.idr:2:Can't unify Set -> Bool and String -> String -> Bool
Bah. Still, it could be worse: when working on the cat fragment on Day 3, I got the message user error (EPIC FAIL). Protip: don't give any of your programs the name io.idr (or any of the other names used by the standard library) - it looks like "." is an early part of the library search path.

Still, it looks to me like I'm misunderstanding something big: can types only be used as arguments in type declarations? Looking through the tutorial so far, that's the only use I can see. In that case, I'm not sure how you'd go about writing a polymorphic equality-tester. I'd like one of those so I can write a test framework, so I can write some more interesting code... the "prove invariants by constructing inhabitants of types which correspond to logical statements about your code" approach looks very interesting, but also like the kind of thing that will take some time to wrap my head around.

So all-in-all not a very successful day, coding-wise. But a day in which you try something and fail is more successful than a day in which you don't try.

[Meanwhile, Tom Scott's similar "produce a web thing every week of November" challenge resulted in a text-mining and data-visualisation project that claims to show that the inhabitants of the House of Lords are not, contrary to recent evidence, going senile. I must stop comparing myself to others.]