如何递归定义广义投影函数？

Question

Projection functions such as id (¹P₁) and 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 的这种实现是一种 hack，因为它使用了可变参数。因此，它不能直接翻译成像 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"

我将把它留作练习，供您找出此函数的依赖类型。

如何递归定义广义投影函数？

How to recursively define a generalized projection function?

javascript

recursion

functional-programming

combinatory-logic