[Agda] Compiler internals for projection functions

[Andreas Abel]

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
>

-- 
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/