haskell - 输入没有意义的签名

Question

考虑

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

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

x -> [a] -> Bool

似乎有很多这样的签名可以立即排除。

Answer 1

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

准备大炮

我们从 generating the free theorem 开始对应类型(a->a) -> [a] -> Bool .正如著名的 Wadler 的论文 Theorems for free! 所确立的，这是该类型的每个函数都必须满足的属性。 .

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和 t2=Int .

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

现在，我们需要定义一个关系 R Bool之间s 和 Int s。让我们采用标准 bool 值
<->整数对应，即:

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)以上。

最后，定理指出，对于 任意 功能 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

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

量子点