[Agda] Compiler works ahead

[Andreas Abel]

On Oct 26, 2010, at 8:12 PM, Daniel Peebles wrote:
> 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?

Some of these optimizations can be carried out without having the  
possibility to "jump over" a tag.  For the others, one would have to  
encode data types constructorless, like in PiSigma, but this does not  
give nice Haskell code.

   data VecTag = VNil | VCons

   type Vec a = (VecTag, a)

   vnil :: Vec a
   vnil = (VNil, unsafeCoerce ())

   vcons :: a -> Vec a -> Vec a
   vcons a v = (VCons, unsafeCoerce (a,v))

   vhead :: Vec a -> a
   vhead (tag, t) = fst (unsafeCoerce t)  -- jumps over VCons tag

There is a lot of unsafeCoerce, seems like a high price to pay.

> 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?

Sure, the plan is that this takes place in the Agda repository.   
Probably, the initial development won't be open, to get started, and  
because it is a student final project, but then it is public an open  
to all kinds of contributions.  Was this what you were thinking?

Cheers,
Andreas

> 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/