你如何证明一个函数对于它的类型是唯一的？

Question

id是类型的唯一功能a -> a,和 fst类型的唯一功能(a,b) -> a.在这些简单的情况下,这是非常简单的.但总的来说,你会如何证明这一点？如果有多个相同类型的可能功能怎么办？

或者,给定函数的类型,如何导出该类型的唯一(如果这是真的)函数？

编辑:我特别感兴趣的是当我们开始在类型中添加约束时会发生什么.

Answer 1

您正在寻找的结果来自雷诺兹的参数化,并且是Wadler在免费定理中最为着名的.

证明基本参数化结果的最优雅的方法我已经看到使用"单一类型"的概念.基本上,给定任何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只有一个居民(其单),因为语义被擦除给出,功能不能使用的参数的类型,所以从可回收的唯一的价值id上的任何Nat是你给它的数量.这个基本论证可以扩展到证明大多数参数性结果,并被Karl Crary用于参数化结果的简单证明技术中,尽管我在这里的演示灵感来自Stone和Harper