[Agda] Compiler internals for projection functions

[Vincent Siles]

Is this related to the performance issue  you were talking about a few week ago
(related to using Sigma instead of build-in records) ?

Cheers,
Vincent

2011/9/23 Ulf Norell <ulf.norell at gmail.com>:
>
> On Fri, Sep 23, 2011 at 3:15 AM, Alan Jeffrey <ajeffrey at bell-labs.com>
> wrote:
>>
>> Thanks for the pointer.
>>
>> Is there any way to recreate the dropped arguments? I don't fancy having
>> to document in the FFI interface that the compliler may sometimes drop
>> arguments based on projection analysis.
>
> The reason why they are dropped is that (a) they're not used and (b) that
> they can be recovered from the type of the first proper argument. An
> optimised js implementation of the function shouldn't really look at these
> arguments so it should be safe to just insert dummy values for the dropped
> arguments.
> / Ulf
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>