How to recursively define a generalized projection function?

Question

Projection functions such as id (¹P₁) and const (²P₁) are very useful in functional programming. However, sometimes you need more complex projection functions such as ⁵P₄. You could write it manually in pointful style as a => b => c => d => e => d but this is tedious and not very readable. Hence, it would be nicer to be able to write proj(5)(4) instead. Here's how I currently defined this generalized projection function in JavaScript:

const proj = n => m => curry(n, (...args) => args[m - 1]);

const curry = (n, f, args = []) => n > 0 ?
    x => curry(n - 1, f, args.concat([x])) :
    f(...args);

console.log(proj(5)(4)("a")("b")("c")("d")("e")); // prints "d"

As you can see, this implementation of proj is a hack because it makes use of variadic arguments. Hence, it can't be directly translated into languages like Agda or Idris (where the generalized projection function is actually typeable due to dependent types). So, how to recursively define a generalized projection function in such a way that it can be directly translated it into Agda?

Answer 1

All projection functions can be decomposed into the following three combinators:

I :: a -> a
I x = x

K :: a -> b -> a
K x y = x

C :: (a -> c) -> a -> b -> c
C f x y = f x

Using these three combinators we can define the various projection functions as follows:

┌─────┬──────────┬──────────┬──────────┬──────────┬─────────────┐
│ n\m │     1    │     2    │     3    │     4    │      5      │
├─────┼──────────┼──────────┼──────────┼──────────┼─────────────┤
│  1  │      I   │          │          │          │             │
│  2  │      K   │     KI   │          │          │             │
│  3  │     CK   │     KK   │   K(KI)  │          │             │
│  4  │   C(CK)  │   K(CK)  │   K(KK)  │ K(K(KI)) │             │
│  5  │ C(C(CK)) │ K(C(CK)) │ K(K(CK)) │ K(K(KK)) │ K(K(K(KI))) │
└─────┴──────────┴──────────┴──────────┴──────────┴─────────────┘

As you can see, there's a recursive pattern here:

proj 1 1 = I
proj n 1 = C (proj (n - 1) 1)
proj n m = K (proj (n - 1) (m - 1))

Note that K = CI which is why proj 2 1 works. Converting this directly to JavaScript:

const I = x => x;
const K = x => y => x;
const C = f => x => y => f(x);

const raise = (Error, msg) => { throw new Error(msg); };

const proj = n => n === 1 ?
    m => m === 1 ? I : raise(RangeError, "index out of range") :
    m => m === 1 ? C(proj(n - 1)(1)) : K(proj(n - 1)(m - 1));

console.log(proj(5)(4)("a")("b")("c")("d")("e")); // prints "d"

I'll leave it as an exercise for you to figure out the dependent type of this function.