<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Briefly, the main difference is that MAlonzo covers the entirety of
Agda, while agda2hs does not really care about that, we instead want
to cover as many Haskell features as possible, i.e. writing Haskell
within Agda if you will.<br>
<p>Also see the 'Related Work: Program Extraction' section of the
paper for more details and comparisons.<br>
<br>
Cheers,<br>
--OM<br>
</p>
<br>
<div class="moz-cite-prefix">On 07/04/2023 16:31, Jason Hu wrote:<br>
</div>
<blockquote type="cite"
cite="mid:PH0PR14MB53821FF739F923A3CEAE6253AF969@PH0PR14MB5382.namprd14.prod.outlook.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<style>@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}.MsoChpDefault
{mso-style-type:export-only;}div.WordSection1
{page:WordSection1;}</style>
<div class="WordSection1">
<p class="MsoNormal">That’s great Jesper. But I don’t quite
understand the difference between the built-in extraction and
agda2hs. I understand that code from agda2hs is more readable,
but why can’t we make the built-in extracted code more
readable?</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div
style="mso-element:para-border-div;border:none;border-top:solid
#E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From:
</b><a href="mailto:jesper@sikanda.be"
moz-do-not-send="true">Jesper Cockx</a><br>
<b>Sent: </b>Friday, April 7, 2023 6:17 AM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se"
moz-do-not-send="true">Agda list</a><br>
<b>Subject: </b>[Agda] Announcement: agda2hs release v1.0</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif">Dear
all,<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif">I
am very pleased to announce the first official release of
agda2hs, a tool for producing verified and readable
Haskell code by extracting it from a (lightly annotated)
Agda program. You can find it at <a
href="https://hackage.haskell.org/package/agda2hs-1.0"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">
https://hackage.haskell.org/package/agda2hs-1.0</a> or
on a cabal package manager near you. The official
documentation can be found at
<a href="https://agda.github.io/agda2hs/" target="_blank"
moz-do-not-send="true" class="moz-txt-link-freetext">https://agda.github.io/agda2hs/</a>,
and more details about the motivation and design are
available in our paper at the Haskell Symposium:
<a href="https://dl.acm.org/doi/10.1145/3546189.3549920"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">https://dl.acm.org/doi/10.1145/3546189.3549920</a>.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif">This
release is just a first step for agda2hs into the wider
world and we have many exciting features that will be
added in the future. If you want to report a bug or a
feature request, you can do so at <a
href="https://github.com/agda/agda2hs/issues"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">
https://github.com/agda/agda2hs/issues</a>. We are also
open to contributions by new developers, feel free to
contact me via email or on Zulip if you have any questions
about this.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif">Best
regards,<o:p></o:p></span></p>
</div>
<p class="MsoNormal"><span
style="font-size:10.5pt;font-family:"Arial",sans-serif">Jesper
Cockx<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
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>
</body>
</html>