[Agda] Compiler works ahead

[Alan Jeffrey]

Yay!  Shinier compiler!  Can I make a couple of feature requests:

a) Support for FFI bindings for dependent types (in particular 
level-polymorphic types) -- I submitted a patch for this.

b) Some support for views, e.g. a COMPILED_VIEW similar to COMPILED_DATA 
except that it inserts a conversion function before pattern-matching and 
after constructor application.  This would allow, for example, binding 
Agda Nat to a Haskell Natural type.

c) Replace unsafeCoerce by our own coercion function, which inlines to 
unsafeCoerce in a late optimization phase.  This would make coercion 
rewrite-friendly, for example the rule (forall (x :: a) . coerce x = x) 
would remove unnecessary coercions.

If we had (c) then I'm not sure we'd need typed compilation to remove 
coercions.

A.

On 10/26/2010 12:21 PM, Andreas Abel 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