1

id( 1 P 1 ) 和const( 2 P 1 )等投影函数在函数式编程中非常有用。但是，有时您需要更复杂的投影函数，例如5 P 4。您可以用点式的方式手动编写它，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 呢？

4

1 回答 1

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"

我将把它作为练习留给你，让你弄清楚这个函数的依赖类型。

于 2018-07-29T09:11:53.403 回答