id
是唯一的类型为a -> a
的函数,fst
是唯一的类型为(a,b) -> a
的函数。在这些简单的情况下,这是相当直接的。但是通常情况下,你要如何证明这一点呢?如果有多个相同类型的可能函数怎么办?
或者,给定一个函数的类型,如何推导出该类型的唯一函数(如果真的存在的话)?
编辑:我特别关注的是当我们开始将约束条件添加到类型中时会发生什么。
你所寻找的结果源于雷诺参数性,最著名的证明是由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 的启发。
id
是类型a->a
中唯一“有趣”或“完备”的函数。在Haskell中,undefined
可以是任何类型,但它不是一个有用的函数。你可能还对Djinn感兴趣,这是一个可以根据类型生成函数的程序,网址是http://lambda-the-ultimate.org/node/1178。 - John Lf ? (a,a,b) -> a
将找到两个答案)。如果列表是详尽的(我不知道是否如此),那么确定唯一性就很容易了。 - John LFloat
,甚至连Int
都不知道,所以如果你尝试的话会出错。但是关于穷尽性的问题并不在于我们需要找到所有的解决方案,而只是我们需要知道我们要找多少个。我不知道底层的 PL 框架是否有能力做到这一点。无论如何,我想测试一下 Church 编码数字和f?Church a -> Church a -> Church a
会发生什么。Djinn 找到了相当多的解,受到截止设置的限制。如果资源没有限制且编码正确,也许它会产生所需的无限解决方案? - John L