Consider

(a->a) -> [a] -> Bool

这个签名有什么有意义的定义吗？也就是说，定义不是简单地忽略论证？

x -> [a] -> Bool

看来这样的签名还有很多，可以立即排除。

Carsten König 在评论中建议使用自由定理。让我们试试吧。

装好大炮

我们从生成自由定理 http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi对应类型(a->a) -> [a] -> Bool。这是该类型的每个函数都必须满足的属性，正如著名的 Wadler 论文所确立的那样免费定理！ http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf.

forall t1,t2 in TYPES, R in REL(t1,t2).
 forall p :: t1 -> t1.
  forall q :: t2 -> t2.
   (forall (x, y) in R. (p x, q y) in R)
   ==> (forall (z, v) in lift{[]}(R). f_{t1} p z = f_{t2} q v)

lift{[]}(R)
  = {([], [])}
  u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))}

一个例子

为了更好地理解上面的定理，让我们看一个具体的例子。要使用该定理，我们需要采用任意两种类型t1,t2，所以我们可以选择t1=Bool and t2=Int.

然后我们需要选择一个函数p :: Bool -> Bool (say p=not) 和一个函数q :: Int -> Int (say q = \x -> 1-x).

现在，我们需要定义一个关系R之间Bools and Ints。让我们采用标准布尔值 整数对应关系，即：

R = {(False,0),(True,1)}

（以上是一一对应的，但一般情况下不一定如此）。

现在我们需要检查一下(forall (x, y) in R. (p x, q y) in R)。我们只有两个案例需要检查(x,y) in R:

Case (x,y) = (False,0): we verify that (not False, 1-0) = (True, 1) in R   (ok!)
Case (x,y) = (True ,1): we verify that (not True , 1-1) = (False,0) in R   (ok!)

到目前为止，一切都很好。现在我们需要“提升”关系以便处理列表：例如

[True,False,False,False] is in relation with [1,0,0,0]

这个扩展关系被命名为lift{[]}(R) above.

最后，定理指出，对于any功能f :: (a->a) -> [a] -> Bool我们必须有

f_Bool not [True,False,False,False] = f_Int (\x->1-x) [1,0,0,0]

上面哪里f_Bool只是明确表示f用于特殊情况，其中a=Bool.

这样做的力量在于我们不知道代码是什么f实际上是。我们正在推论什么f必须仅通过查看其多态类型来满足。

由于我们从类型推断中获得类型，并且我们可以将类型转化为定理，因此我们真正获得了“免费定理！”。

回到最初的目标

我们想证明这一点f不使用它的第一个参数，并且它也不关心它的第二个列表参数，除了它的长度。

为此，采取R是普遍正确的关系。然后，lift{[]}(R)是一种关系，如果两个列表具有相同的长度，则将它们关联起来。

该定理意味着：

forall t1,t2 in TYPES.
 forall p :: t1 -> t1.
  forall q :: t2 -> t2.
   forall z :: [t1].
    forall v :: [t2].
     length z = length v ==> f_{t1} p z = f_{t2} q v

Hence, f忽略第一个参数，只关心第二个参数的长度。

QED