I wrote and host lsc-todaybot, a bot that moves the [TODAY] flair around on reddit.com/r/LondonSocialClub, a subreddit dedicated to social activities in London. I wrote it in Haskell, and over the last year or so have used it as a simple application for experimenting with different Haskell libraries and techniques. For example, I used it to learn about extensible effects (and gave a talk about it at the London Haskell meetup).
I've been interested in the dependently typed programming language Idris and someone claimed it was pacman-complete - that is, you can write Pacman in it. So rather than playing round with proofs and all that dependent-type gubbins, I set out to rewrite todaybot in Idris.
It's here: https://github.com/benclifford/idris-todaybot
It's not beautiful. But it works well enough to be running alongside the Haskell implementation.
I've littered the source with QUESTION/DISCUSSION blocks, but basically I had to patch up an existing JSON library, interface an HTTP library (I chose libcurl), and struggle with a whole new style of error message (possibly the hardest bit as I'm used to error messages really leading you to the right answer).
There's almost no use of dependent types, but I did find a straightforward place to make use of them, in the parameters to this libcurl function:
CURLcode curl_easy_setopt(CURL *handle, CURLoption option, parameter);
where the type of the supplied parameter depends on the particular option chosen: for example a pointer to a callback function, or a boolean verbosity level.
No comments:
Post a Comment