如何证明一个函数在其类型中是唯一的？

Question

id是唯一的类型为a -> a的函数，fst是唯一的类型为(a，b) -> a的函数。在这些简单的情况下，这是相当直接的。但是通常情况下，你要如何证明这一点呢？如果有多个相同类型的可能函数怎么办？

或者，给定一个函数的类型，如何推导出该类型的唯一函数（如果真的存在的话）？

编辑：我特别关注的是当我们开始将约束条件添加到类型中时会发生什么。

- Mike Izbicki

---

严谨来说，我认为人们通常会说 id 是类型 a->a 中唯一“有趣”或“完备”的函数。在Haskell中，undefined 可以是任何类型，但它不是一个有用的函数。你可能还对Djinn感兴趣，这是一个可以根据类型生成函数的程序，网址是http://lambda-the-ultimate.org/node/1178。 - John L

@JohnL Djinn并没有真正证明唯一性，对吧？它只是在存在的情况下找到了某些类型的函数。 - Mike Izbicki

这个问题可能更适合发布在http://cs.stackexchange.com。 - Heatsink

@MikeIzbicki 这是一个很好的观点。然而，Djinn会找到多个解决方案（例如f ? (a,a,b) -> a将找到两个答案）。如果列表是详尽的（我不知道是否如此），那么确定唯一性就很容易了。 - John L

@amindfv： Djinn 不知道 Float，甚至连 Int 都不知道，所以如果你尝试的话会出错。但是关于穷尽性的问题并不在于我们需要找到所有的解决方案，而只是我们需要知道我们要找多少个。我不知道底层的 PL 框架是否有能力做到这一点。无论如何，我想测试一下 Church 编码数字和 f？Church a -> Church a -> Church a 会发生什么。Djinn 找到了相当多的解，受到截止设置的限制。如果资源没有限制且编码正确，也许它会产生所需的无限解决方案？ - John L

Answer 1

你所寻找的结果源于雷诺参数性，最著名的证明是由Wadler在theorems for free中展示。

证明基本参数性结果最优雅的方式是使用“单例类型”的概念。基本上，给定任何抽象数据类型

data Nat = Zero | Succ Nat

存在一个索引族（也被称为GADT）

data SNat n where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)

我们可以通过将所有类型消除为无类型语言，从而给我们的语言赋予语义，使得Nat和SNat擦除为相同的东西。 然后，通过语言的类型规则

id (x :: SNat n) :: SNat n

SNat n 只有一个成员（它的单例），因为语义是通过擦除给出的，函数不能使用它们的参数类型，所以 id 在任何 Nat 上返回的唯一可返回值是你给它的数字。这个基本的论证可以推广到证明大多数参数性结果，并被 Karl Crary 用于 A Simple Proof Technique for Parametricity Results，尽管我在这里的展示受到了 Stone 和 Harper 的启发。

- Philip JF