id是 type 的唯一函数，也是 typea -> a的
fst唯一函数(a,b) -> a。在这些简单的情况下，这很容易看出。但总的来说，您将如何证明这一点？如果同一类型有多个可能的函数怎么办？
或者，给定一个函数的类型，你如何推导出该类型的唯一（如果这是真的）函数？
编辑：我对当我们开始向类型添加约束时会发生什么特别感兴趣。
问问题
1863 次
1 回答
15
您正在寻找的结果来自 Reynolds 的参数性，并且最著名的是 Wadler 在定理中的 free。
我见过的证明基本参数结果的最优雅的方法是使用“单例类型”的概念。本质上，给定任何 ADT
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只有一个居民（它的单身人士），因为语义是通过擦除给出的，所以函数不能使用它们的参数的类型，所以唯一可以从idanyNat上返回的值是你给它的数字。这个基本论证可以扩展来证明大多数参数化结果，并且被 Karl Crary 在参数化结果的简单证明技术中使用，尽管我在这里的演示文稿受到了Stone 和 Harper的启发
于 2012-11-27T06:05:50.467 回答