javascript - 如何实现 f(g) == g(f)

Question

我answered a question yesterday这让我想起了一个(对我来说)有趣的谜题

限制使用lambda、数字和+(没有if, ?:,或其他语言特性)，目标是实现一些 f 和一些 g 这样

// contract
f(x) => f'
g(y) => g'
f'(g') == g'(f')

// or more simply:
m(n) == n(m)

Here's what I came up with so far - this code is in JavaScript for the purpose of being able to demonstrate the code in the browser but answers in any functional language are acceptable (racket, clojure, ocaml, lambda calc, etc)

// f
const f = x => k =>
  k(y => y + x)

// g
const g = y => k =>
  k(x => x + y)
  
// make instance of each
const a = f(1)
const b = g(2)

console.log(a(b))
// x => x + y1
// should be 3

console.log(b(a))
// y => y + x2
// should be 3

我能够修复一个关系的一半，但由于f和g现在不对称

// f
const f = x => k =>
  k(y => y(x))

// g
const g = y => k =>
  k(x => x + y)
  
// make instance of each
const a = f(1)
const b = g(2)

console.log(a(b))
// 3
// should be 3 (OK)

console.log(b(a))
// y => y + x2
// should be 3

我知道为什么它不起作用，但我在尝试修复它时遇到了问题。最重要的是，如果这不可能，我很想知道为什么。

如果你想出一个打破限制的方案，我还是有兴趣看看的^_^

Answer 1

这个答案假设一个强大的非单位类型系统(例如 Haskell，但我在这里尝试坚持使用类似 JS 的语法)。

如果我们停留在参数化领域，我们就不需要(甚至不能使用)数字或条件。常量函数不会改变任何东西，所以我将它们省略并直接处理 f 和 g。

首先，观察方程

f(g) == g(f)

暗示f 和g 都有函数类型。假设两者都有不同的输入，我们得到 f: A -> X 和 g: B -> X == (A -> X) -> X == ((B -> X ) -> X) -> X == ...，即，你得到一个无限类型。我记得读过一篇关于这种确切构造的论文(可以将其表示为一对类型，我认为它构成了一个类别)，但不幸的是忘记了它的名字——也许这里还有更多要说的。

一个更简单的解决方案是要求 A == B。然后 f, g: A -> X，但是由于 X == A 根据对称方程，它遵循 f, g: A -> A——对于任意的A，也就是说。实现这一点的一种可能性是身份函数:

id(id) == id(id)

当我们将 A 专门化为 A -> A 时，就会出现其他解决方案；然后我们搜索 (A -> A) -> (A -> A) 类型的函数。这些是，一方面，已经找到的(专门的)恒等函数，还有形状 h => h o ... o h 的所有函数 -- 组合 ((o ) = h => x => h(h(x))) 多个类型的函数。这些在应用程序中“添加重复”，例如

(h => h o h)(h => h o h) == (h => h o h) o (h => h o h)
                         == h => h o h o h o h.

由此可见我们可以选择

f == g == h => h,
f == g == h => h o h,
f == g == h => h o h o h,
f == g == ...

我认为，所有类型的函数都是 forall A. (A -> A) -> (A -> A)(不包括非终止)。

这种结构的极限(无限组合)似乎也与上​​面提到的无限情况(现在在真正的 Haskell 中)有关系:

Prelude> let g = \h -> h . g

<interactive>:11:19:
    Occurs check: cannot construct the infinite type: b ~ (b -> c) -> c