Как рекурсивно определить обобщенную функцию проекции?

Question

Функции проекции, такие как id (¹ P ₁) и const (² P ₁) очень полезны в функциональном программировании. Однако иногда вам нужны более сложные проекционные функции, такие как ⁵ P ₄. Вы можете написать это вручную в точечном стиле, как a => b => c => d => e => d но это утомительно и не очень читабельно. Следовательно, было бы лучше иметь возможность писать proj(5)(4) вместо. Вот как я сейчас определил эту обобщенную функцию проекции в 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"

Как вы можете видеть, эта реализация proj это взлом, потому что он использует переменные аргументы. Следовательно, он не может быть напрямую переведен на такие языки, как Agda или Idris (где обобщенная проекционная функция фактически может быть набрана благодаря зависимым типам). Итак, как рекурсивно определить обобщенную проекционную функцию таким образом, чтобы ее можно было напрямую перевести в Agda?

Answer 1

Все проекционные функции можно разложить на следующие три комбинатора:

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

Используя эти три комбинатора, мы можем определить различные функции проекции следующим образом:

┌─────┬──────────┬──────────┬──────────┬──────────┬─────────────┐
│ 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))) │
└─────┴──────────┴──────────┴──────────┴──────────┴─────────────┘

Как видите, здесь есть рекурсивный шаблон:

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

Обратите внимание, что K = CI вот почему proj 2 1 работает. Преобразование этого непосредственно в 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"

Я оставлю это в качестве упражнения для вас, чтобы выяснить зависимый тип этой функции.