[Agda] Compiler internals for projection functions

[Alan Jeffrey]

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.

A.

On 09/22/2011 11:09 AM, Andreas Abel wrote:
> Hi Jeffrey,
>
> indeed, your analysis of the situation is correct.  The epic backend
> team had a similar question, here is Ulf's answer:
>
>     http://code.google.com/p/agda/issues/detail?id=465
>
> Cheers,
> Andreas
>
> On 22.09.11 4:25 PM, Jeffrey, Alan S A (Alan) wrote:
>> A question about the internals of the compiler...
>>
>> Agda does some static analysis to determine whether or not a function is a projection, for example:
>>
>>     data Pair(A B :Set) : Set
>>       _,_ : A ->   B ->   Pair A B
>>
>>     fst : {A B : Set} ->   Pair A B ->   A
>>     fst (a , b) = a
>>
>>     swap : {A B : Set} ->   Pair A B ->   Pair B A
>>     swap (a , b) = (b , a)
>>
>> Static analysis determines that fst is a projection and swap isn't. Good for it.
>>
>> Now the weird bit... Internally, swap takes 3 parameters (A, B and the pair) as you'd expect, but fst only takes one (just the pair). The compiler is consistent about this: when swap is applied it is given three arguments, and when fst is applied it is only give one. It looks like what's going on is that the internal representation of projection functions strips off any indexes of the projected type.
>>
>> This is causing me headaches in the JS back end, especially in the case where the user is providing FFI bindings (e.g. they might decide to bind Pair to native arrays, and provide optimized code for fst and swap).
>>
>> Before embarking on lots of hacky workarounds I thought I'd double-check to make sure my analysis is right, and that the internal representation of a function changes depending on whether or not it is flagged as a projection.
>>
>> A._______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>