[Agda] Compiler works ahead

[Daniel Peebles]

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?

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?

Thanks,
Dan

On Tue, Oct 26, 2010 at 1:21 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> 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.
>
> My plans are:
> - typed compilation (that will remove the bulk of unsafeCoerce
> applications)
> - useless code analyses (that will hopefully remove the bulk of static
> code)
>
> The useless code analyses have been described by Edwin Brady and
> colleagues:
>
> - "forcing" analysis: removing redundant constructor arguments
> - "collapsing" analysis (aka token type analysis): detecting unit types
> - identity analysis: eliminating applications of traversal functions that
> amount to the identity
>
> The output will be Haskell source, unless someone integrates external core
> into GHC in the meantime.
> 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.
>
> Comments welcome.
>
> Cheers,
> Andreas
>
>
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101026/d4541bcd/attachment.html