[Agda] hello, I've done something terrible...

[Jeremy Shaw]

Hello,

I am ashamed to admit that I have done something horrible ... I have  
written an irc bot in Agda.

That's right! A program that you can not only type-check -- but even  
run! And it is a pretty big hack job too... probably even buggy!

I have forever tarnished the good name of Agda.

You can attempt to browse the source here:

http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty

But unicode support is apparently busted -- so it is a bit tough to  
read.

darcs get should be fine though:

darcs get http://patch-tag.com/r/stepcut/agdabot

Current it only supports one command: hi

Here is a sample session:

<stepcut> agdabot: hi
<agdabot> hello!

The most 'interesting' part of the code is perhaps the unit tests. For  
example, here is a unit test that checks that messages are decoded  
properly:

test-decode-1 : decode ":adams.freenode.net NOTICE * :*** Looking up  
your hostname..." ≡ just (record { prefix = just (server  
"adams.freenode.net") ; command = "NOTICE" ; params = "*" ∷ "***  
Looking up your hostname..." ∷ [] })
test-decode-1 = refl

There the unit test is in the type signature and checked at compile  
time. Obviously that is old hat to a seasoned Agda programmer, but  
crazy talk to a Haskell user :)

The thing that makes the code especially ugly is that I have not  
figured out how to handle the equivalent of nested case statements  
yet. So, I have a bunch of helper functions that use 'with f x' to  
work around that. That is probably the first thing I will fix.

The biggest known flaw is that the many1 parser does not prove  
termination, so I had to enable --no-termination-check. That is  
probably the second thing I will look at.

patches and flames welcome!

- jeremy

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110725/7a40ae9a/attachment.html