[Agda] Compiler works ahead

[Daniel Peebles]

Nominolo on IRC pointed out that in some cases, GHC does already optimize
this, if you can convince it that only one constructor is possible even at
the core level: http://hpaste.org/40909/impossible_constructor_cases_o

You can see that the generated core only has one pattern match and that the
cmm from it doesn't check the tag.

However, in a quick sized vector example I tried, with a zip over it, it
wasn't so smart and the core did contain matches between Cons and Nil, with
the associated pattern match error generation code and double tag check.
This was on GHC 7 RC1.

But maybe GHC could be made smarter about these things, or the Haskell
codegen could craft GADTs that GHC is able to optimize suitably.

Anyway, not a big deal I guess :)

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

> 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/
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101026/b881a334/attachment-0001.html