<!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);">&lt;stepcut&gt; </span>agdabot:
          hi</div>
        <div style="margin: 0px 0px 0px 119px; text-indent: -119px;
          font: 12px Courier;"><font class="Apple-style-span"
            color="#222222">&lt;</font><span style="color: rgb(105, 30,
            108);">agdabot&gt;</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>