证明具有某些签名的函数唯一性的陈述的形式主义是什么

Question

假设我想要一个像这样的函数

f: ((A, B) -> C) -> A -> B -> C

我经常看到的一种说法是 f 只有一种实现，即“柯里函数”，即 g => a => b => g(a, b)

从表面上看，这似乎并不正确，我总是可以将 f 定义为在特殊情况下表现与此不同，例如我可以说是 g => a => b => g(a, b) 除非 A = B 然后我将其定义为 g => a => b => g(b, a).

尽管如此，“只有一种实现”的含义非常直观。

我想知道可以证明上述陈述的正确形式主义。

我猜测我会怀疑这是范畴论？上面感觉有点像自然变换的概念，但我并没有真正看到细节。

Answer 1

我确信与范畴论有联系，但你实际上可以使用（我认为是）一个更简单的工具来做到这一点：参数化。

他们的基本思想是，当一种语言具有多态类型对它们实例化到的每种类型执行完全相同的操作时（即，多态类型）的属性。没有 typecase 构造），我们可以以逻辑关系的形式证明该语言非常强大的属性。

这完全阻止了您在问题中描述的“特殊情况”实现。还值得一提的是，这些实现都是 外延地 平等的：它们可能看起来不同，但相同的输入会产生相同的结果。例如您可以替换任何术语 $t$ 和 $(\lambda x \ldotp x) t $ 并得到一个等价的函数。

仅从其类型来描述函数的语句通常称为 自由定理, ，以介绍该想法的论文命名： 免费定理 作者：菲尔·瓦德勒。如果您对这个领域感兴趣，我强烈推荐这篇论文，因为它是对该主题的很好的介绍。

这个想法背后的想法实际上比那篇论文要追溯到约翰·雷诺兹对系统 F 和“抽象定理”的研究，但这个想法花了一段时间才流行起来。

您实际上可以在以下位置生成免费定理 http://free-theorems.nomeata.de/, ，尽管可能需要一些按摩才能从他们给出的定理中获取有用的信息。

如果您对用于证明自由定理以外的事物（例如类型安全）的参数性感兴趣，那么 阿迈勒·艾哈迈德的论文 是我见过的最好的介绍。她在描述语义类型方面确实做得很好：程序的类型实际上是它如何运行和产生什么的属性，我们所说的“类型”是这些更一般的语义类型的语法近似。