CODEWITHSUNDEEP
javascriptrecursionfunctional-programmingcombinatory-logic
Aadit M Shah
Aadit M Shah

Reputation: 74204

How to recursively define a generalized projection function?

Projection functions such as id (1P1) and const (2P1) are very useful in functional programming. However, sometimes you need more complex projection functions such as 5P4. 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?

Upvotes: 1

Views: 119

Answers (1)

Aadit M Shah
Aadit M Shah

Reputation: 74204

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.

Upvotes: 1

Related Questions