[Agda] Compiler works ahead

[Daniel Peebles]

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.


Yeah, that makes sense, and probably isn't worth it in most cases. I just
asked the people in #ghc on IRC and they said there wasn't an easy way to do
this in GHC (especially if you have unboxed fields in your constructors),
and it wouldn't be a simple change either. It probably isn't even a big win
in most cases, but it'd be nice to do. Maybe someday Haskell itself will
implement that optimization for multiple GADT matches, but people don't seem
terribly interested.


 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?


Yeah, that makes sense, and sounds good.

Thanks,
Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101026/3184b0e0/attachment.html