[Agda] Compiler works ahead

[Andreas Abel]

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/