<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
You might have a look at an example I have written some time ago,
namely<br>
a drawing program written in Agda.<br>
The way to overcome the problem with termination is to use
coalgebras <br>
(at some point called codata, currently implemented using Nisse's #
and b).<br>
<br>
<a class="moz-txt-link-freetext" href="http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/">http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/</a><br>
<br>
Anton<br>
<br>
<br>
On 26/07/11 05:58, Jeremy Shaw wrote:
<blockquote
cite="mid:CFA30019-5390-444E-A9CA-646ACD5DDFF6@n-heptane.com"
type="cite">Hello,
<div><br>
</div>
<div>I am ashamed to admit that I have done something horrible ...
I have written an irc bot in Agda.</div>
<div><br>
</div>
<div>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!</div>
<div><br>
</div>
<div>I have forever tarnished the good name of Agda.</div>
<div><br>
</div>
<div>You can attempt to browse the source here:</div>
<div><br>
</div>
<div><a moz-do-not-send="true"
href="http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty">http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty</a></div>
<div><br>
</div>
<div>But unicode support is apparently busted -- so it is a bit
tough to read. </div>
<div><br>
</div>
<div>darcs get should be fine though:</div>
<div><br>
</div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;">darcs
get <a moz-do-not-send="true"
href="http://patch-tag.com/r/stepcut/agdabot">http://patch-tag.com/r/stepcut/agdabot</a></span></div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;"><br>
</span></div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;">Current
it only supports one command: hi</span></div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;"><br>
</span></div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;">Here
is a sample session:</span></div>
<div><span class="Apple-style-span" style="color: rgb(34, 34, 34);
font-family: courier; font-size: 12px; line-height: 18px;"><br>
</span></div>
<div>
<div style="margin: 0px 0px 0px 119px; text-indent: -119px;
font: 12px Courier; color: rgb(58, 58, 58);"><span
style="color: rgb(132, 132, 132);"><stepcut> </span>agdabot:
hi</div>
<div style="margin: 0px 0px 0px 119px; text-indent: -119px;
font: 12px Courier;"><font class="Apple-style-span"
color="#222222"><</font><span style="color: rgb(105, 30,
108);">agdabot></span> <font class="Apple-style-span"
color="#222222">hello!</font></div>
<div style="font-family: courier; font-size: 12px; line-height:
18px; color: rgb(34, 34, 34);"><br>
</div>
<div style="font-family: courier; font-size: 12px; line-height:
18px; color: rgb(34, 34, 34);">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:</div>
<div style="font-family: courier; font-size: 12px; line-height:
18px; color: rgb(34, 34, 34);"><br>
</div>
<div>
<div><font class="Apple-style-span" color="#222222"
face="courier"><span class="Apple-style-span"
style="line-height: 18px;">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..." ∷ [] })</span></font></div>
<div><font class="Apple-style-span" color="#222222"
face="courier"><span class="Apple-style-span"
style="line-height: 18px;">test-decode-1 = refl</span></font></div>
</div>
</div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;">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 :)</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;">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.</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;">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.</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;">patches
and flames welcome!</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;">- jeremy</span></font></div>
<div><font class="Apple-style-span" color="#222222" face="courier"><span
class="Apple-style-span" style="line-height: 18px;"><br>
</span></font></div>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
<br>
<pre class="moz-signature" cols="72">--
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK
Telephone:
(national) (01792) 513368
(international) +44 1792 513368
Fax:
(national) (01792) 295708
(international) +44 1792 295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: <a class="moz-txt-link-abbreviated" href="mailto:a.g.setzer@swan.ac.uk">a.g.setzer@swan.ac.uk</a>
WWW:
<a class="moz-txt-link-freetext" href="http://www.cs.swan.ac.uk/~csetzer/">http://www.cs.swan.ac.uk/~csetzer/</a>
---------------------------------------
</pre>
</body>
</html>