[Agda] Compiler works ahead
pumpkingod at gmail.com
Tue Oct 26 20:12:36 CEST 2010
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?
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
> - useless code analyses (that will hopefully remove the bulk of static
> The useless code analyses have been described by Edwin Brady and
> - "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
> Comments welcome.
> 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
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda