This is great news! Have you considered any optimizations along the lines of "Inductive Families Need Not Store Their Indices" too? It seems like compilation to Haskell/GHC would be a problem there, as there's no real way of avoiding a tag check on constructors. Or maybe we can convince the GHC folks to provide a backdoor of sorts there for it?<div>
<br></div><div>Anyway, I'm really excited about this development. Do you plan on keeping development "open" (with a public repository) and possibly accepting small contributions from external developers?</div>
<div><br></div><div>Thanks,</div><div>Dan<br><br><div class="gmail_quote">On Tue, Oct 26, 2010 at 1:21 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">To my fellow Agda developers I'd like to announce that I plan to work on the compilation to Haskell. This is to avoid the duplication of efforts. I have two students who are interested to implement an improved compiler for Agda, probably they will start working beginning of next year.<br>
<br>
My plans are:<br>
- typed compilation (that will remove the bulk of unsafeCoerce applications)<br>
- useless code analyses (that will hopefully remove the bulk of static code)<br>
<br>
The useless code analyses have been described by Edwin Brady and colleagues:<br>
<br>
- "forcing" analysis: removing redundant constructor arguments<br>
- "collapsing" analysis (aka token type analysis): detecting unit types<br>
- identity analysis: eliminating applications of traversal functions that amount to the identity<br>
<br>
The output will be Haskell source, unless someone integrates external core into GHC in the meantime.<br>
I am tending towards a "pretty" Haskell output that is callable from other Haskell modules. That may encourage Haskell programmers to write parts of their projects in Agda even when they want to stick to Haskell as the main platform.<br>
<br>
Comments welcome.<br>
<br>
Cheers,<br>
Andreas<br>
<br>
<br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>