[Agda] Compiler internals for projection functions

[Jeffrey, Alan S A (Alan)]

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.