Beware of the Train

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

Today's hack is up. It's to the flashlight app again; now the UI stays in portrait orientation no matter how you rotate the phone. This prevents the pause/resume/create cycle that was killing my Activity and causing the light to go out. Most of yesterday's code is no longer needed and has been taken out again, but that's a good thing, right? :-)

Sideload the app (if you care - HTC Sense has such a thing built-in) from here.

Anyway, the way you do this is by adding the attribute android:screenOrientation="portrait" to the activity element in your manifest. This tip came from this StackOverflow post: I tried the more complicated "add a configChanges attribute and override onConfigurationChanged" approach described there, but that resulted in the LED wedging in whatever state it was in when you rotated the phone and not accepting any further changes. God knows what was going on there.

By the way, does anyone use git add -p much? I tried the "edit this hunk" feature a couple of times, but it told me that it my patch wouldn't apply cleanly, and then rejected the whole thing. Also, I'm having trouble uploading files to GitHub's "download" section.

Edit: and I've had a documentation patch accepted into Idris. Go me!