PeCoWriMo day 4

[pozorvlak]

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